From ea7f06c23ec1645f545c7faefacc1db4809b757d Mon Sep 17 00:00:00 2001
From: Fonenantsoa Maurica <maurica.fonenantsoa@gmail.com>
Date: Thu, 3 Jan 2019 15:40:54 +0100
Subject: [PATCH] Support for user-defined logic functions and predicates
without labels
---
src/plugins/e-acsl/Makefile.in | 2 +
src/plugins/e-acsl/env.ml | 15 +
src/plugins/e-acsl/env.mli | 6 +
src/plugins/e-acsl/fixpoint.ml | 213 +++++
src/plugins/e-acsl/fixpoint.mli | 78 ++
src/plugins/e-acsl/gmpz.ml | 23 +
src/plugins/e-acsl/gmpz.mli | 2 +
src/plugins/e-acsl/interval.ml | 160 +++-
src/plugins/e-acsl/interval.mli | 1 +
src/plugins/e-acsl/lfunctions.ml | 505 +++++++++++
src/plugins/e-acsl/lfunctions.mli | 56 ++
src/plugins/e-acsl/misc.ml | 54 ++
src/plugins/e-acsl/misc.mli | 24 +-
.../tests/bts/oracle/bts1307.res.oracle | 18 +-
.../tests/format/oracle/fprintf.res.oracle | 3 +-
.../tests/format/oracle/printf.res.oracle | 21 +-
src/plugins/e-acsl/tests/gmp/functions.c | 71 ++
.../e-acsl/tests/gmp/functions_contiki.c | 28 +
src/plugins/e-acsl/tests/gmp/functions_rec.c | 30 +
.../tests/gmp/oracle/functions.0.res.oracle | 41 +
.../tests/gmp/oracle/functions.1.res.oracle | 43 +
.../gmp/oracle/functions_contiki.0.res.oracle | 25 +
.../gmp/oracle/functions_contiki.1.res.oracle | 25 +
.../gmp/oracle/functions_rec.0.res.oracle | 25 +
.../gmp/oracle/functions_rec.1.res.oracle | 47 ++
.../e-acsl/tests/gmp/oracle/gen_functions.c | 420 ++++++++++
.../e-acsl/tests/gmp/oracle/gen_functions2.c | 513 ++++++++++++
.../tests/gmp/oracle/gen_functions_contiki.c | 45 +
.../tests/gmp/oracle/gen_functions_contiki2.c | 45 +
.../tests/gmp/oracle/gen_functions_rec.c | 623 ++++++++++++++
.../tests/gmp/oracle/gen_functions_rec2.c | 782 ++++++++++++++++++
.../runtime/oracle/local_goto.res.oracle | 6 +-
.../tests/runtime/oracle/mainargs.res.oracle | 5 +-
.../tests/temporal/oracle/t_getenv.res.oracle | 4 +-
.../temporal/oracle/t_malloc-asan.res.oracle | 2 +-
.../tests/temporal/oracle/t_memcpy.res.oracle | 12 +-
src/plugins/e-acsl/translate.ml | 46 +-
src/plugins/e-acsl/typing.ml | 99 ++-
src/plugins/e-acsl/typing.mli | 13 +-
src/plugins/e-acsl/visit.ml | 2 +
40 files changed, 4063 insertions(+), 70 deletions(-)
create mode 100644 src/plugins/e-acsl/fixpoint.ml
create mode 100644 src/plugins/e-acsl/fixpoint.mli
create mode 100644 src/plugins/e-acsl/lfunctions.ml
create mode 100644 src/plugins/e-acsl/lfunctions.mli
create mode 100644 src/plugins/e-acsl/tests/gmp/functions.c
create mode 100644 src/plugins/e-acsl/tests/gmp/functions_contiki.c
create mode 100644 src/plugins/e-acsl/tests/gmp/functions_rec.c
create mode 100644 src/plugins/e-acsl/tests/gmp/oracle/functions.0.res.oracle
create mode 100644 src/plugins/e-acsl/tests/gmp/oracle/functions.1.res.oracle
create mode 100644 src/plugins/e-acsl/tests/gmp/oracle/functions_contiki.0.res.oracle
create mode 100644 src/plugins/e-acsl/tests/gmp/oracle/functions_contiki.1.res.oracle
create mode 100644 src/plugins/e-acsl/tests/gmp/oracle/functions_rec.0.res.oracle
create mode 100644 src/plugins/e-acsl/tests/gmp/oracle/functions_rec.1.res.oracle
create mode 100644 src/plugins/e-acsl/tests/gmp/oracle/gen_functions.c
create mode 100644 src/plugins/e-acsl/tests/gmp/oracle/gen_functions2.c
create mode 100644 src/plugins/e-acsl/tests/gmp/oracle/gen_functions_contiki.c
create mode 100644 src/plugins/e-acsl/tests/gmp/oracle/gen_functions_contiki2.c
create mode 100644 src/plugins/e-acsl/tests/gmp/oracle/gen_functions_rec.c
create mode 100644 src/plugins/e-acsl/tests/gmp/oracle/gen_functions_rec2.c
diff --git a/src/plugins/e-acsl/Makefile.in b/src/plugins/e-acsl/Makefile.in
index c366ab4588b..4368abf9540 100644
--- a/src/plugins/e-acsl/Makefile.in
+++ b/src/plugins/e-acsl/Makefile.in
@@ -73,12 +73,14 @@ PLUGIN_CMO:= local_config \
env \
keep_status \
dup_functions \
+ fixpoint \
interval \
typing \
loops \
quantif \
at_with_lscope \
mmodel_translate \
+ lfunctions \
translate \
temporal \
prepare_ast \
diff --git a/src/plugins/e-acsl/env.ml b/src/plugins/e-acsl/env.ml
index c571fb5333a..a1e2b5d26c4 100644
--- a/src/plugins/e-acsl/env.ml
+++ b/src/plugins/e-acsl/env.ml
@@ -314,6 +314,17 @@ module Logic_binding = struct
in
v, e, env
+ let add_existing_vi env lv vi =
+ try
+ let varinfos = Logic_var.Map.find lv env.var_mapping in
+ Stack.push vi varinfos;
+ env
+ with Not_found | Stack.Empty ->
+ let varinfos = Stack.create () in
+ Stack.push vi varinfos;
+ let var_mapping = Logic_var.Map.add lv varinfos env.var_mapping in
+ { env with var_mapping = var_mapping }
+
let get env logic_v =
try
let varinfos = Logic_var.Map.find logic_v env.var_mapping in
@@ -337,6 +348,10 @@ let current_kf env =
| None -> None
| Some kf -> Some (Cil.get_kernel_function v#behavior kf)
+let set_current_kf env kf =
+ let v = env.visitor in
+ v#set_current_kf kf
+
let get_visitor env = env.visitor
let get_behavior env = env.visitor#behavior
diff --git a/src/plugins/e-acsl/env.mli b/src/plugins/e-acsl/env.mli
index 7fe184e3d02..1339e9357f3 100644
--- a/src/plugins/e-acsl/env.mli
+++ b/src/plugins/e-acsl/env.mli
@@ -68,6 +68,9 @@ module Logic_binding: sig
val add: ?ty:typ -> t -> logic_var -> varinfo * exp * t
(* Add a new C binding to the list of bindings for the logic variable. *)
+ val add_existing_vi: t -> logic_var -> varinfo -> t
+ (* [add_existing_vi env lv vi] defines [vi] as latest C binding for [lv]. *)
+
val get: t -> logic_var -> varinfo
(* Return the latest C binding. *)
@@ -142,6 +145,9 @@ module Logic_scope: sig
reset at next call to [reset]. *)
end
+val set_current_kf: t -> kernel_function -> unit
+(* Set current kf of the environment *)
+
(* ************************************************************************** *)
(** {2 Current annotation kind} *)
(* ************************************************************************** *)
diff --git a/src/plugins/e-acsl/fixpoint.ml b/src/plugins/e-acsl/fixpoint.ml
new file mode 100644
index 00000000000..6af95b408cf
--- /dev/null
+++ b/src/plugins/e-acsl/fixpoint.ml
@@ -0,0 +1,213 @@
+(**************************************************************************)
+(* *)
+(* This file is part of Frama-C. *)
+(* *)
+(* Copyright (C) 2007-2018 *)
+(* CEA (Commissariat à l'énergie atomique et aux énergies *)
+(* alternatives) *)
+(* *)
+(* you can redistribute it and/or modify it under the terms of the GNU *)
+(* Lesser General Public License as published by the Free Software *)
+(* Foundation, version 2.1. *)
+(* *)
+(* It is distributed in the hope that it will be useful, *)
+(* but WITHOUT ANY WARRANTY; without even the implied warranty of *)
+(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the *)
+(* GNU Lesser General Public License for more details. *)
+(* *)
+(* See the GNU Lesser General Public License version 2.1 *)
+(* for more details (enclosed in the file licenses/LGPLv2.1). *)
+(* *)
+(**************************************************************************)
+
+open Cil_types
+
+type ival_binop = Ival_add | Ival_min | Ival_mul | Ival_div | Ival_union
+
+type ival_exp =
+ | Iconst of Ival.t
+ | Ivar of string * logic_type list
+ | Ibinop of ival_binop * ival_exp * ival_exp
+ | Iunsupported
+
+let equal_ivar ivar1 ivar2 = match ivar1, ivar2 with
+ | Ivar(str1, ltys1), Ivar(str2, ltys2) ->
+ str1 = str2 &&
+ List.fold_left2
+ (fun b lty1 lty2 -> b && Cil_datatype.Logic_type.equal lty1 lty2)
+ true
+ ltys1
+ ltys2
+ | _ ->
+ Options.fatal "not an ivar"
+
+module Ieqs: sig
+ type t
+ val empty: t
+ val add: ival_exp -> ival_exp -> t -> t
+ val find: ival_exp -> t -> ival_exp
+ val cardinal: t -> int
+ val fold: (ival_exp -> ival_exp -> 'a -> 'a) -> t -> 'a -> 'a
+ val map: (ival_exp -> ival_exp) -> t -> t
+end = struct
+ module H = Map.Make(struct
+ type t = ival_exp (* an Ivar to be precise *)
+ let compare ivar1 ivar2 = if equal_ivar ivar1 ivar2 then 0 else 1
+ end)
+ type t = ival_exp H.t
+ let empty = H.empty
+ let add ivar iexp ieqs = match ivar with
+ | Ivar _ -> H.add ivar iexp ieqs
+ | _ -> Options.fatal "left-hand side is NOT an ivar"
+ let find = H.find
+ let map = H.map
+ let fold = H.fold
+ let cardinal = H.cardinal
+end
+
+(* Normalize the expression.
+ An expression is said to be normalized if it is:
+ - either Iunsupported
+ - or an expression that contains no Iunsupported *)
+let normalize_iexp iexp =
+ let rec has_unsupported iexp = match iexp with
+ | Iunsupported | Ibinop(_, Iunsupported, _) | Ibinop(_, _, Iunsupported) ->
+ true
+ | Ibinop(_, (Iconst _ | Ivar _), (Iconst _ | Ivar _))
+ | Iconst _ | Ivar _ ->
+ false
+ | Ibinop(_, iexp1, iexp2) ->
+ has_unsupported iexp1 || has_unsupported iexp2
+ in
+ if has_unsupported iexp then Iunsupported else iexp
+
+let normalize_ieqs ieqs =
+ Ieqs.map (fun iexp -> normalize_iexp iexp) ieqs
+
+let ivars_contains_ivar ivars ivar =
+ List.fold_left (fun b ivar' -> b || equal_ivar ivar ivar') false ivars
+
+let get_ival_of_iconst ieqs ivar = match Ieqs.find ieqs ivar with
+ | Iconst i -> i
+ | Ivar _ | Ibinop _| Iunsupported -> Options.fatal "not an Iconst"
+
+(*************************************************************************)
+(******************************** Solver *********************************)
+(*************************************************************************)
+
+(* [iterate indexes max] increases by 1 the leftmost element of [indexes] that
+ is less or equal to [max].
+ Eg: from index=[| 0; 0; 0 |] and max=2, the successive iterates
+ until reaching index=[| max; max; max |] are as follows:
+ [| 0; 0; 0 |]
+ [| 1; 0; 0 |]
+ [| 1; 1; 0 |]
+ [| 1; 1; 1 |]
+ [| 2; 1; 1 |]
+ [| 2; 2; 1 |]
+ [| 2; 2; 2 |]
+ Note that the number [N] of iterates is linear in [max*l] where [l] is the
+ length of [index]: [N=max*l+1].
+ [int array] (instead of [int list]) is the proper data structure for storing
+ [indexes], at least because its length is known in advance: the number of
+ variables. *)
+let iterate indexes max =
+ let min_i = ref 0 in
+ for indexes_i = 1 to Array.length indexes - 1 do
+ if indexes.(indexes_i) < indexes.(!min_i) then min_i := indexes_i
+ done;
+ if indexes.(!min_i) + 1 <= max then
+ (* The if-test is because the last iterate cannot be increased *)
+ indexes.(!min_i) <- indexes.(!min_i) + 1
+
+(* Returns an assignement to each variable of [ieqs] such that:
+ - the first (resp. the second... the last) element of [indexes] is
+ associated to the first (resp. the second... the last) variable of [ieqs]
+ - a variable that is associated to an index [index] ranging in
+ [0..max-1] will be given the interval of finite bounds:
+ [-chain_of_ivalmax.(index), chain_of_ivalmax.(index)]
+ Â - a variable that is associated to an index [index] equaling [max] will
+ be given the whole interval of integers [Z]. *)
+let to_iconsts indexes ieqs chain_of_ivalmax =
+ let max = Array.length chain_of_ivalmax in
+ let indexes_i = ref 0 in
+ Ieqs.map
+ (fun _ ->
+ let ival =
+ let index = indexes.(!indexes_i) in
+ if index < max then
+ let ivalmax = chain_of_ivalmax.(index) in
+ Ival.inject_range (Some (Integer.neg ivalmax)) (Some ivalmax)
+ else if
+ index = max then Ival.inject_range None None
+ else
+ assert false
+ in
+ indexes_i := !indexes_i + 1;
+ Iconst ival)
+ ieqs
+
+(* Assumes [iexp] to be a normalized [ival_exp] and evaluates it when each of
+ its variable is replaced by the corresponding interval from [iconsts]. *)
+let rec eval_iexp iexp iconsts =
+ match iexp with
+ | Iunsupported ->
+ Iconst (Ival.inject_range None None)
+ | Iconst _ ->
+ iexp
+ | Ivar _ ->
+ Ieqs.find iexp iconsts
+ | Ibinop(_, Iunsupported, _) | Ibinop(_, _, Iunsupported) ->
+ assert false (* because [iexp] has been normalized *)
+ | Ibinop(ibinop, iexp1, iexp2) ->
+ let i1 = match eval_iexp iexp1 iconsts with
+ | Iconst i -> i
+ | Iunsupported | Ivar _ | Ibinop _ -> assert false
+ in
+ let i2 = match eval_iexp iexp2 iconsts with
+ | Iconst i -> i
+ | Iunsupported | Ivar _ | Ibinop _ -> assert false
+ in
+ match ibinop with
+ | Ival_add -> Iconst (Ival.add_int i1 i2)
+ | Ival_min -> Iconst (Ival.sub_int i1 i2)
+ | Ival_mul -> Iconst (Ival.mul i1 i2)
+ | Ival_div -> Iconst (Ival.div i1 i2)
+ | Ival_union -> Iconst (Ival.join i1 i2)
+
+let equal_iconst iconst1 iconst2 =
+ let i1 = match iconst1 with
+ | Iconst i -> i
+ | Iunsupported | Ivar _ | Ibinop _ -> assert false
+ in
+ let i2 = match iconst2 with
+ | Iconst i -> i
+ | Iunsupported | Ivar _ | Ibinop _ -> assert false
+ in
+ Ival.is_included i1 i2
+
+let is_post_fixpoint ieqs iconsts = Ieqs.fold
+ (fun ivar iexp b ->
+ let iconst1 = eval_iexp iexp iconsts in
+ let iconst2 = Ieqs.find ivar iconsts in
+ b && equal_iconst iconst1 iconst2)
+ ieqs
+ true
+
+let rec iterate_till_post_fixpoint ieqs indexes chain_of_ivalmax =
+ let iconsts = to_iconsts indexes ieqs chain_of_ivalmax in
+ if is_post_fixpoint ieqs iconsts then
+ iconsts
+ else
+ let index_max = Array.length chain_of_ivalmax in
+ iterate indexes index_max;
+ iterate_till_post_fixpoint ieqs indexes chain_of_ivalmax
+
+let solve ieqs ivar chain_of_ivalmax =
+ let ieqs = normalize_ieqs ieqs in
+ let dim = Ieqs.cardinal ieqs in
+ let bottom = Array.make dim 0 in
+ let post_fixpoint =
+ iterate_till_post_fixpoint ieqs bottom chain_of_ivalmax
+ in
+ get_ival_of_iconst ivar post_fixpoint
\ No newline at end of file
diff --git a/src/plugins/e-acsl/fixpoint.mli b/src/plugins/e-acsl/fixpoint.mli
new file mode 100644
index 00000000000..ac2f146e7e1
--- /dev/null
+++ b/src/plugins/e-acsl/fixpoint.mli
@@ -0,0 +1,78 @@
+(**************************************************************************)
+(* *)
+(* This file is part of Frama-C. *)
+(* *)
+(* Copyright (C) 2007-2018 *)
+(* CEA (Commissariat à l'énergie atomique et aux énergies *)
+(* alternatives) *)
+(* *)
+(* you can redistribute it and/or modify it under the terms of the GNU *)
+(* Lesser General Public License as published by the Free Software *)
+(* Foundation, version 2.1. *)
+(* *)
+(* It is distributed in the hope that it will be useful, *)
+(* but WITHOUT ANY WARRANTY; without even the implied warranty of *)
+(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the *)
+(* GNU Lesser General Public License for more details. *)
+(* *)
+(* See the GNU Lesser General Public License version 2.1 *)
+(* for more details (enclosed in the file licenses/LGPLv2.1). *)
+(* *)
+(**************************************************************************)
+
+open Cil_types
+
+(** Fixpoint equation solver for infering intervals of
+ recursively defined logic functions *)
+
+(**************************************************************************)
+(*************************** Constructors *********************************)
+(**************************************************************************)
+
+type ival_binop = Ival_add | Ival_min | Ival_mul | Ival_div | Ival_union
+
+type ival_exp =
+ | Iconst of Ival.t
+ | Ivar of string (* function name *) * logic_type list (* args lty *)
+ (** Example: to the function signature f(int, long) corresponds
+ the expression Ivar("f", [int; long]) *)
+ | Ibinop of ival_binop * ival_exp * ival_exp
+ | Iunsupported
+
+module Ieqs: sig
+ type t
+ (** [Ieqs.t] represents systems of equations over [ival_exp] expressions in
+ which the variables to be found are the [Ivar] constructs.
+ [Ieqs.t] can be viewed as a fixpoint equation in the sense that the left-
+ hand side of the equation MUST be an [Ivar]:
+ solving the system [(S): x1=f1(x1, ..., xn) /\ ... /\ xn=fn(x1, ..., xn)]
+ is equivalent to solving the fixpoint equation [(E): X=F(X)] where
+ X=(x1, ..., xn) and F=(f1, ..., fn). *)
+ val empty: t
+ val add:
+ ival_exp (* left-hand side, MUST be an [Ivar] *) -> ival_exp -> t -> t
+end
+
+(**************************************************************************)
+(***************************** Solver *************************************)
+(**************************************************************************)
+
+val solve: Ieqs.t -> ival_exp -> Integer.t array -> Ival.t
+(** [solve ieqs ivar chain] finds an interval for the variable [ivar]
+ that satisfies the fixpoint equation [ieqs]. The solver is parameterized
+ by the increasingly sorted array [chain] of positive integers.
+ For chain=[n1; n2; ...; nk] where n1 < ... < nk, [solve] will
+ consider the following set S of intervals as potential solution:
+ S={[-n1, n1], [-n2, n2]... [-nk; nk]}. Then [solve] will iteratively
+ affect intervals from S to the different variables of [ieqs],
+ starting from the smallest interval [-n1, n1] to the biggest one [-nk,
+ nk], until finding the smallest combination that satisfies [ieqs].
+ If no combination is found then [solve] returns Z. *)
+
+(**************************************************************************)
+(****************************** Utils *************************************)
+(**************************************************************************)
+
+val ivars_contains_ivar: ival_exp list -> ival_exp -> bool
+(** [contains ivars ivar] checks whether the list of Ivar [ivars] contains the
+ Ivar [ivar]. *)
\ No newline at end of file
diff --git a/src/plugins/e-acsl/gmpz.ml b/src/plugins/e-acsl/gmpz.ml
index ea9e81f9486..91c7c05e864 100644
--- a/src/plugins/e-acsl/gmpz.ml
+++ b/src/plugins/e-acsl/gmpz.ml
@@ -28,12 +28,32 @@ let t_torig_ref =
tname = "";
ttype = TVoid [];
treferenced = false }
+let t_struct_torig_ref =
+ ref
+ { torig_name = "";
+ tname = "";
+ ttype = TVoid [];
+ treferenced = false }
let set_t ty = t_torig_ref := ty
+let set_t_struct ty = t_struct_torig_ref := ty
let is_now_referenced () = !t_torig_ref.treferenced <- true
let t () = TNamed(!t_torig_ref, [])
+let t_ptr () = TNamed(
+ {
+ torig_name = "";
+ tname = "__e_acsl_mpz_struct *";
+ ttype = TArray(
+ TNamed(!t_struct_torig_ref, []),
+ Some (Cil.one ~loc:Cil_datatype.Location.unknown),
+ {scache = Not_Computed},
+ []);
+ treferenced = true;
+ },
+[])
+
let is_t ty = Cil_datatype.Typ.equal ty (t ())
let apply_on_var ~loc funname e = Misc.mk_call ~loc ("__gmpz_" ^ funname) [ e ]
@@ -106,6 +126,9 @@ let init_t () =
| GType({ torig_name = s } as info, _) when s = "__e_acsl_mpz_t" ->
set_t info;
Cil.SkipChildren
+ | GType({ torig_name = s } as info, _) when s = "__e_acsl_mpz_struct" ->
+ set_t_struct info;
+ Cil.SkipChildren
| _ ->
Cil.SkipChildren
end in
diff --git a/src/plugins/e-acsl/gmpz.mli b/src/plugins/e-acsl/gmpz.mli
index 503d9887391..4f1f25f47e3 100644
--- a/src/plugins/e-acsl/gmpz.mli
+++ b/src/plugins/e-acsl/gmpz.mli
@@ -31,6 +31,8 @@ val set_t: typeinfo -> unit
val t: unit -> typ
(** type "mpz_t" *)
+val t_ptr: unit -> typ
+ (** type "_mpz_struct *" *)
val is_now_referenced: unit -> unit
(** Should be called once one variable of type "mpz_t" exists *)
diff --git a/src/plugins/e-acsl/interval.ml b/src/plugins/e-acsl/interval.ml
index e2186708be5..7bd5aab9ec4 100644
--- a/src/plugins/e-acsl/interval.ml
+++ b/src/plugins/e-acsl/interval.ml
@@ -47,6 +47,16 @@ let rec interv_of_typ ty = match Cil.unrollType ty with
| _ ->
raise Not_an_integer
+(* Return the interval over which ranges the smallest typ containing [i]. *)
+let interv_of_typ_containing_interv i =
+ try
+ let itv_kind = Misc.itv_kind i in
+ (* convert the kind to [IInt] whenever smaller. *)
+ let kind = if Cil.intTypeIncluded itv_kind IInt then IInt else itv_kind in
+ interv_of_typ (TInt(kind, []))
+ with Cil.Not_representable ->
+ Ival.inject_range None None
+
let interv_of_unknown_block =
(* since we have no idea of the size of this block, we take the largest
possible one which is unfortunately quite large *)
@@ -62,6 +72,7 @@ module Env = struct
let add = Logic_var.Hashtbl.add tbl
let remove = Logic_var.Hashtbl.remove tbl
let replace = Logic_var.Hashtbl.replace tbl
+ let find_all = Logic_var.Hashtbl.find_all tbl
let find = Logic_var.Hashtbl.find tbl
end
@@ -185,7 +196,64 @@ let rec infer t =
| Tapp (li, _, _args) ->
(match li.l_type with
| None -> assert false (* [None] only possible for predicates *)
- | Some Linteger -> Error.not_yet "logic function returning an integer"
+ | Some Linteger ->
+ begin match li.l_body with
+ | LBpred _ ->
+ Ival.zero_or_one
+ | LBterm t' ->
+ let i =
+ if Misc.is_recursive li then
+ (* 1) Build a system of interval equations that
+ constrain the solution:
+ do so by returning a variable when encoutering
+ a call of a recursive function instead of
+ performing the usual interval inference
+ BEWARE: we might be tempted to memoize the
+ solution for a given function signature
+ HOWEVER: it cannot be done in a straightforward
+ manner due to the cases of functions that use
+ C (global) variables in their definition (as the values of
+ those variables can change between two function calls). *)
+ let ieqs = Fixpoint.Ieqs.empty in
+ let ivar, ieqs, _ = build_ieqs t ieqs [] in
+ (* 2) Solve it:
+ The problem is probably undecidable in the general case.
+ Thus we just look for reasonably precise approximations
+ without being too computationally expensive:
+ simply iterate over a finite set of pre-defined intervals.
+ See [Fixpoint.solve] for details. *)
+ let chain_of_ivalmax =
+ [| Integer.one; Integer.billion_one; Integer.max_int64 |]
+ (* This set can be changed based on experimental evidences,
+ but it works fine for now. *)
+ in
+ let i = Fixpoint.solve ieqs ivar chain_of_ivalmax in
+ i
+ else begin
+ List.iter2
+ (fun lv arg ->
+ try
+ let i = interv_of_typ_containing_interv (infer arg) in
+ Env.add lv i
+ with Not_an_integer -> ())
+ li.l_profile
+ _args;
+ let i =
+ try infer t'
+ with Not_an_integer -> Ival.inject_range None None
+ in
+ List.iter (fun lv -> Env.remove lv) li.l_profile;
+ i
+ end
+ in
+ i
+ | LBnone ->
+ Error.not_yet "logic functions with no definition nor reads clause"
+ | LBreads _ ->
+ Error.not_yet "logic functions performing read accesses"
+ | LBinductive _ ->
+ Error.not_yet "logic functions inductively defined"
+ end
| Some (Ctype ty) -> interv_of_typ ty
| Some _ -> raise Not_an_integer)
| Tunion _ -> Error.not_yet "tset union"
@@ -227,10 +295,21 @@ and infer_term_lval (host, offset as tlv) =
let ty = Logic_utils.logicCType (Cil.typeOfTermLval tlv) in
interv_of_typ ty
-and infer_term_host = function
+and infer_term_host h = match h with
| TVar v ->
(try Env.find v
- with Not_found -> interv_of_typ (Logic_utils.logicCType v.lv_type))
+ with Not_found ->
+ match v.lv_type with
+ | Linteger ->
+ Ival.inject_range None None
+ | Ctype (TFloat _) -> (* TODO: handle in MR !226 *)
+ raise Not_an_integer
+ | Lreal ->
+ Error.not_yet "real numbers"
+ | Ctype _ ->
+ interv_of_typ (Logic_utils.logicCType v.lv_type)
+ | Ltype _ | Lvar _ | Larrow _ ->
+ Options.fatal "unexpected logic type")
| TResult ty -> interv_of_typ ty
| TMem t ->
let ty = Logic_utils.logicCType t.term_type in
@@ -241,6 +320,81 @@ and infer_term_host = function
Printer.pp_typ ty
Printer.pp_term t
+(* Build the system of interval equations for the logic function called
+ through [t].
+ Example: the following function:
+ f(Z n) = n < 0 ? 1 : f(n - 1) * f(n - 2) / f(n - 3)
+ when called with f(37)
+ will generate the following system of equations:
+ X = [1; 1] U Y*Y/Y /\
+ Y = [1; 1] U Z*Z/Z /\
+ Z = [1; 1] U Z*Z/Z
+ where X is the interval for f(int) (since 37 \in int),
+ Y the one for f(long) (from int-1, int-2 and int-3)
+ and Z the for the f(Z) (from long-1, long-2 and long-3) *)
+and build_ieqs t ieqs ivars =
+ match t.term_node with
+ | Tapp(li, _, args) ->
+ if li.l_type = Some Linteger && Misc.is_recursive li then begin
+ let args_lty = List.map2
+ (fun lv arg ->
+ try
+ let i = interv_of_typ_containing_interv (infer arg) in
+ Env.add lv i;
+ Ctype (TInt(Misc.itv_kind i, []))
+ with
+ | Cil.Not_representable -> Linteger
+ | Not_an_integer -> lv.lv_type)
+ li.l_profile
+ args
+ in
+ (* x *)
+ let ivar = Fixpoint.Ivar(li.l_var_info.lv_name, args_lty) in
+ (* Adding x = g(x) if it is not yet in the system of equations.
+ Without this check, the algorithm would not terminate. *)
+ let ieqs, ivars =
+ if Fixpoint.ivars_contains_ivar ivars ivar then ieqs, ivars
+ else
+ let iexp, ieqs, ivars =
+ build_ieqs (Misc.term_of_li li) ieqs (ivar :: ivars)
+ in
+ let ieqs = Fixpoint.Ieqs.add ivar iexp ieqs in (* Adding x = g(x) *)
+ ieqs, ivars
+ in
+ List.iter (fun lv -> Env.remove lv) li.l_profile;
+ ivar, ieqs, ivars
+ end else
+ (try Fixpoint.Iconst(infer t), ieqs, ivars
+ with Not_an_integer -> Fixpoint.Iunsupported, ieqs, ivars)
+ | TConst _ ->
+ (try Fixpoint.Iconst(infer t), ieqs, ivars
+ with Not_an_integer -> Fixpoint.Iunsupported, ieqs, ivars)
+ | TLval(TVar _, _) ->
+ (try Fixpoint.Iconst(infer t), ieqs, ivars
+ with Not_an_integer -> Fixpoint.Iunsupported, ieqs, ivars)
+ | TBinOp (PlusA, t1, t2) ->
+ let iexp1, ieqs, ivars = build_ieqs t1 ieqs ivars in
+ let iexp2, ieqs, ivars = build_ieqs t2 ieqs ivars in
+ Fixpoint.Ibinop(Fixpoint.Ival_add, iexp1, iexp2), ieqs, ivars
+ | TBinOp (MinusA, t1, t2) ->
+ let iexp1, ieqs, ivars = build_ieqs t1 ieqs ivars in
+ let iexp2, ieqs, ivars = build_ieqs t2 ieqs ivars in
+ Fixpoint.Ibinop(Fixpoint.Ival_min, iexp1, iexp2), ieqs, ivars
+ | TBinOp (Mult, t1, t2) ->
+ let iexp1, ieqs, ivars = build_ieqs t1 ieqs ivars in
+ let iexp2, ieqs, ivars = build_ieqs t2 ieqs ivars in
+ Fixpoint.Ibinop(Fixpoint.Ival_mul, iexp1, iexp2), ieqs, ivars
+ | TBinOp (Div, t1, t2) ->
+ let iexp1, ieqs, ivars = build_ieqs t1 ieqs ivars in
+ let iexp2, ieqs, ivars = build_ieqs t2 ieqs ivars in
+ Fixpoint.Ibinop(Fixpoint.Ival_div, iexp1, iexp2), ieqs, ivars
+ | Tif(_, t1, t2) ->
+ let iexp1, ieqs, ivars = build_ieqs t1 ieqs ivars in
+ let iexp2, ieqs, ivars = build_ieqs t2 ieqs ivars in
+ Fixpoint.Ibinop(Fixpoint.Ival_union, iexp1, iexp2), ieqs, ivars
+ | _ ->
+ Fixpoint.Iunsupported, ieqs, ivars
+
(*
Local Variables:
compile-command: "make"
diff --git a/src/plugins/e-acsl/interval.mli b/src/plugins/e-acsl/interval.mli
index 0a1e07d7b78..a900728f952 100644
--- a/src/plugins/e-acsl/interval.mli
+++ b/src/plugins/e-acsl/interval.mli
@@ -67,6 +67,7 @@ module Env: sig
val add: Cil_types.logic_var -> Ival.t -> unit
val remove: Cil_types.logic_var -> unit
val replace: Cil_types.logic_var -> Ival.t -> unit
+ val find_all: Cil_types.logic_var -> Ival.t list
end
(* ************************************************************************** *)
diff --git a/src/plugins/e-acsl/lfunctions.ml b/src/plugins/e-acsl/lfunctions.ml
new file mode 100644
index 00000000000..1b549ddc500
--- /dev/null
+++ b/src/plugins/e-acsl/lfunctions.ml
@@ -0,0 +1,505 @@
+(**************************************************************************)
+(* *)
+(* This file is part of Frama-C. *)
+(* *)
+(* Copyright (C) 2007-2018 *)
+(* CEA (Commissariat à l'énergie atomique et aux énergies *)
+(* alternatives) *)
+(* *)
+(* you can redistribute it and/or modify it under the terms of the GNU *)
+(* Lesser General Public License as published by the Free Software *)
+(* Foundation, version 2.1. *)
+(* *)
+(* It is distributed in the hope that it will be useful, *)
+(* but WITHOUT ANY WARRANTY; without even the implied warranty of *)
+(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the *)
+(* GNU Lesser General Public License for more details. *)
+(* *)
+(* See the GNU Lesser General Public License version 2.1 *)
+(* for more details (enclosed in the file licenses/LGPLv2.1). *)
+(* *)
+(**************************************************************************)
+
+open Cil_types
+
+type lfsig_info = { (* Logic Function SIGnature INFOrmation *)
+ lfs_li: logic_info; (* the logic definition,
+ base template to be specialized *)
+ lfs_args_lty: logic_type list; (* types of the args for the specialization *)
+ lfs_lty: logic_type (* return type for the specialization *)
+}
+
+(**************************************************************************)
+(********************** Forward references ********************************)
+(**************************************************************************)
+
+let predicate_to_exp_ref
+ : (kernel_function -> Env.t -> predicate -> exp * Env.t) ref
+ = Extlib.mk_fun "named_predicate_to_exp_ref"
+
+let term_to_exp_ref
+ : (kernel_function -> Env.t -> term -> exp * Env.t) ref
+ = Extlib.mk_fun "term_to_exp_ref"
+
+let add_cast_ref
+ : (location -> Env.t -> typ option -> bool -> exp -> exp * Env.t) ref
+ = Extlib.mk_fun "add_cast_ref"
+
+(*****************************************************************************)
+(****************** Generation of function bodies ****************************)
+(*****************************************************************************)
+
+(* Determine the C typ corresponding to a formal argument based on its logic
+ type. In particular, [arg_typ_from_lty] MUST NOT return arrays:
+ they should be converted into pointers. *)
+let arg_typ_from_lty lty = match lty with
+ | Linteger ->
+ Gmpz.t_ptr () (* but not [Gmpz.t] as returned by [Typing.typ_of_lty] *)
+ | Lreal ->
+ Error.not_yet "[arg_typ_from_lty] reals" (* TODO: handle in MR !226 *)
+ | Ctype _ | Ltype _ | Lvar _ | Larrow _ ->
+ let typ = Typing.typ_of_lty lty in
+ if Cil.isArrayType typ then Error.not_yet "[arg_typ_from_lty] array"
+ else typ
+
+(* Creates a new [kf] with an empty body. Its body is to be filled
+ through [fill_kf] afterwards. These two operations are purposefully
+ made distinct in order to avoid non-termination in case of recursive
+ definitions. *)
+let empty_kf lfs typ =
+ let li = lfs.lfs_li in
+ let fname = Functions.RTL.mk_gen_name
+ (Env.Varname.get ~scope:Env.Global li.l_var_info.lv_name)
+ in
+ let is_not_returnable = Cil.isArrayType typ in
+ let ty_f = if is_not_returnable then Cil.voidType else typ in
+ let vi_f = Cil.makeGlobalVar
+ fname
+ (TFun
+ (ty_f,
+ None, (* Typs of the arguments. Will be updated in the following
+ through [Cil.makeFormalVar] *)
+ false,
+ li.l_var_info.lv_attr))
+ in
+ let fundec =
+ { svar = vi_f;
+ sformals = []; (* Will be updated in the following
+ through [Cil.makeFormalVar] *)
+ slocals = []; (* Will be updated by [fill_kf] *)
+ smaxid = 0;
+ sbody = Cil.mkBlock []; (* Will be updated by [fill_kf] *)
+ smaxstmtid = None;
+ sallstmts = [];
+ sspec = Cil.empty_funspec () }
+ in
+ (* Now updating information on arguments *)
+ List.iter2
+ (fun lv lty ->
+ let name = Functions.RTL.mk_gen_name lv.lv_name ^ "_arg" in
+ let typ = arg_typ_from_lty lty in
+ ignore (Cil.makeFormalVar fundec ~where:"$" name typ))
+ li.l_profile
+ lfs.lfs_args_lty;
+ if is_not_returnable then
+ (* If the result of the function cannot be returned,
+ then define it as being the (additional) first argument *)
+ ignore (Cil.makeFormalVar
+ fundec
+ ~where:"^"
+ "__retres_arg"
+ (arg_typ_from_lty (Extlib.the li.l_type)));
+ (* Creating and returning the kf *)
+ { fundec = Definition(fundec, Cil_datatype.Location.unknown);
+ spec = Cil.empty_funspec () }
+
+(* Bind arguments to the intervals corresponding to their logic type. *)
+let add_interv_bindings lfs =
+ List.iter2
+ (fun lv lty ->
+ match lty with
+ | Linteger ->
+ let i = Ival.inject_range None None in
+ Interval.Env.add lv i
+ | Ctype (TFloat _) -> (* TODO: handle in MR !226 *)
+ ()
+ | Lreal ->
+ Error.not_yet "real numbers"
+ | Ctype (TInt(ik, _)) ->
+ let i = Interval.interv_of_typ (TInt(ik, [])) in
+ Interval.Env.add lv i
+ | Ctype _ ->
+ ()
+ | Ltype _ | Lvar _ | Larrow _ ->
+ Options.fatal "unexpected logic type")
+ lfs.lfs_li.l_profile
+ lfs.lfs_args_lty
+
+let remove_interv_bindings lfs =
+ List.iter
+ (fun lv -> Interval.Env.remove lv)
+ lfs.lfs_li.l_profile
+
+let retype lfs = match lfs.lfs_li.l_body with
+ | LBpred p ->
+ Typing.clear_all_pred_or_term (Misc.PoT_pred p);
+ Typing.type_named_predicate ~must_clear:false p
+ | LBterm t ->
+ Typing.clear_all_pred_or_term (Misc.PoT_term t);
+ Typing.type_term ~use_gmp_opt:true t
+ | LBnone ->
+ Error.not_yet "logic functions with no definition nor reads clause"
+ | LBreads _ ->
+ Error.not_yet "logic functions performing read accesses"
+ | LBinductive _ ->
+ Error.not_yet "logic functions inductively defined"
+
+(* Bind lv to C variables.
+ Case A: lv can be directly binded to the formal arg fo the C function.
+ Example: the typ corresponding to lv is [int]
+ Case B: lv CANNOT be directly binded to the formal arg.
+ This is notably the case for GMP since if they were directly binded,
+ then the function would free them before returning. Thus copies are
+ required. *)
+let add_varinfo_bindings ~loc kf env lfs =
+ (* Handle typs that cannot be returned *)
+ let vi_args =
+ let fundec = Misc.fundec_of_kf kf in
+ let vi_ty = match fundec.svar.vtype with
+ | TFun(ty, _, _, _) -> ty
+ | _ -> assert false
+ in
+ if Cil_datatype.Typ.equal Cil.voidType vi_ty then
+ match fundec.sformals with
+ | [] -> assert false
+ | _ :: vi_args -> vi_args (* First arg is the result *)
+ else
+ fundec.sformals
+ in
+ let env =
+ let lvs_and_ltys =
+ List.map2 (fun lv lty -> lv, lty) lfs.lfs_li.l_profile lfs.lfs_args_lty
+ in
+ List.fold_left2
+ (fun env (lv, lty) vi_arg ->
+ match Typing.ty_of_logic_ty lty with
+ | Typing.C_type _ | Typing.Other ->
+ (* Case A *)
+ Env.Logic_binding.add_existing_vi env lv vi_arg
+ | Typing.Gmp ->
+ (* Case B *)
+ let ty = Typing.typ_of_lty lv.lv_type in
+ let vi, _, env = Env.Logic_binding.add ~ty env lv in
+ vi_arg.vtype <- Gmpz.t ();
+ let stmt = Gmpz.init_set
+ ~loc (Cil.var vi) (Cil.evar ~loc vi) (Cil.evar ~loc vi_arg)
+ in
+ vi_arg.vtype <- Gmpz.t_ptr ();
+ let env = Env.add_stmt env stmt in
+ env)
+ env
+ lvs_and_ltys
+ vi_args
+ in
+ env
+
+(* Generate the function's body. For predicates. *)
+let pred_to_block ~loc kf env p =
+ (* Translate *)
+ let named_predicate_to_exp = !predicate_to_exp_ref in
+ let e, env = named_predicate_to_exp kf env p in
+ (* Create the variable [retres] to be returned,
+ the stmt [set_retres] setting it,
+ and the stmt [return_retres] returning it. *)
+ let fundec = Misc.fundec_of_kf kf in
+ let retres = Cil.makeLocalVar fundec "__retres" Cil.intType in
+ let set_retres =
+ Cil.mkStmtOneInstr ~valid_sid:true (Set (Cil.var retres, e, loc))
+ in
+ let return_retres = Cil.mkStmt
+ ~valid_sid:true (Return (Some (Cil.evar ~loc retres), loc))
+ in
+ (* The whole block *)
+ let b, env =
+ Env.pop_and_get env set_retres ~global_clear:false Env.Middle
+ in
+ b.blocals <- retres :: b.blocals;
+ b.bstmts <- b.bstmts @ [ return_retres ];
+ b.bscoping <- true; (* Kernel details *)
+ b, env
+
+(* Generate the function's body. For terms. *)
+let term_to_block ~loc kf env t lty (* the return type *) =
+ let term_to_exp = !term_to_exp_ref in
+ let e, env = term_to_exp kf env t in
+ (* Functions that are of primitive types are not retyped
+ ==> cast needed in case the type system inferred a different type *)
+ let ctx = Typing.typ_of_lty lty in
+ let add_cast = !add_cast_ref in
+ let e, env = add_cast loc env (Some ctx) false e in
+ (* The body itself *)
+ let fundec = Misc.fundec_of_kf kf in
+ begin match Typing.ty_of_logic_ty lty with
+ | Typing.C_type _ | Typing.Other ->
+ let typ = Typing.get_typ t in
+ assert (not (Cil_datatype.Typ.equal Cil.voidType typ));
+ (* Create the variable [retres] to be returned,
+ the stmt [set_retres] setting it,
+ and the stmt [return_retres] returning it. *)
+ let retres = Cil.makeLocalVar fundec "__retres" typ in
+ let set_retres =
+ Cil.mkStmtOneInstr ~valid_sid:true (Set (Cil.var retres, e, loc))
+ in
+ let return_retres = Cil.mkStmt
+ ~valid_sid:true (Return (Some (Cil.evar ~loc retres), loc))
+ in
+ (* The whole block *)
+ let b, env =
+ Env.pop_and_get env set_retres ~global_clear:false Env.Middle
+ in
+ b.blocals <- retres :: b.blocals;
+ b.bstmts <- b.bstmts @ [ return_retres ];
+ b.bscoping <- true; (* Kernel details *)
+ b, env
+ | Typing.Gmp ->
+ (* GMPs are not returned but given as (additional) first argument
+ to the function. *)
+ let set_first_arg =
+ let first_arg = List.hd fundec.sformals in
+ Misc.mk_call
+ (* We cannot call [Gmpz.set] since it will only make an alias *)
+ ~loc "__gmpz_init_set" [ Cil.evar ~loc first_arg; e ]
+ in
+ let return_void = Cil.mkStmt ~valid_sid:true (Return (None, loc)) in
+ (* The whole block *)
+ let b, env =
+ Env.pop_and_get env set_first_arg ~global_clear:false Env.Middle
+ in
+ b.bstmts <- b.bstmts @ [ return_void ];
+ b.bscoping <- true; (* Kernel details *)
+ b, env
+ end
+
+(* Fill [kf]'s body based on [lfs]. See also: [empty_kf]. *)
+let fill_kf lfs kf =
+ (* Init env *)
+ let env = Env.push Env.dummy in
+ Env.set_current_kf env kf;
+ let loc = Cil_datatype.Location.unknown in
+ let env = add_varinfo_bindings ~loc kf env lfs in
+ (* Create kf's body (the fundec's block) *)
+ let b, env = match lfs.lfs_li.l_body with
+ | LBpred p ->
+ pred_to_block ~loc kf env p
+ | LBterm t ->
+ term_to_block ~loc kf env t lfs.lfs_lty
+ | LBnone ->
+ Error.not_yet "logic functions with no definition nor reads clause"
+ | LBreads _ ->
+ Error.not_yet "logic functions performing read accesses"
+ | LBinductive _ ->
+ Error.not_yet "logic functions inductively defined"
+ in
+ (* Fill the fundec *)
+ let fundec = Misc.fundec_of_kf kf in
+ fundec.sbody <- b;
+ let new_vars =
+ List.map (fun (vi, _) -> vi) (Env.get_generated_variables env)
+ in
+ fundec.slocals <- fundec.slocals @ new_vars
+
+(**************************************************************************)
+(***************************** Memoization ********************************)
+(**************************************************************************)
+
+module Memo = Hashtbl.Make(struct
+ type t = lfsig_info
+ let equal lfs1 lfs2 =
+ Cil_datatype.Logic_info.equal lfs1.lfs_li lfs2.lfs_li &&
+ List.fold_left2
+ (fun b lty1 lty2 -> b && Cil_datatype.Logic_type.equal lty1 lty2)
+ true
+ lfs1.lfs_args_lty
+ lfs2.lfs_args_lty
+ let hash = Hashtbl.hash
+end)
+
+let tbl = Memo.create 7
+
+let memo lfs typ =
+ try Memo.find tbl lfs
+ with Not_found ->
+ (* We need to create a new [kf]. It is done as follows:
+ Step 1: Create a [kf] with an empty body
+ Step 2: Memoize it
+ Step 3: Fill it
+ In particular, its body CANNOT be filled during its creation: it would
+ lead to non-termination for recursive definitions. *)
+ (* Step 1 *)
+ let kf = empty_kf lfs typ in
+ (* Step 2 *)
+ Memo.add tbl lfs kf;
+ (* Step 3 *)
+ fill_kf lfs kf;
+ (* Kernel details *)
+ let fundec = Misc.fundec_of_kf kf in
+ fundec.svar.vdefined <- true;
+ Globals.Functions.register kf;
+ (* Return *)
+ kf
+
+(* Returns all the [kf] that have been constructed and memoized
+ so far for the given [logic_info]. *)
+let find_kfs li =
+ Memo.fold
+ (fun lfs kf l ->
+ if Cil_datatype.Logic_info.equal lfs.lfs_li li then kf :: l
+ else l)
+ tbl
+ []
+
+(*****************************************************************************)
+(****************** Generation of function calls *****************************)
+(*****************************************************************************)
+
+let generate ~loc env t li args args_lty =
+ let name = li.l_var_info.lv_name ^ "_tapp" in
+ let mk_call vi =
+ (* Building the arguments 1/3:
+ If the result is an array (eg gmp), then it cannot be returned.
+ Thus we let it be the (additional) first argument. *)
+ let vi_f_typ = Typing.get_typ t in
+ let args, lvl_opt =
+ if Cil.isArrayType vi_f_typ then
+ (Cil.evar ~loc vi) :: args, None
+ else
+ args, Some (Cil.var vi)
+ in
+ (* Building the arguments 2/3:
+ AST sanity: arrays that are given as arguments of functions
+ must be explicitely indicated as being pointers *)
+ let args = List.map
+ (fun arg ->
+ if Cil_datatype.Typ.equal (Cil.typeOf arg) (Gmpz.t ()) then
+ (* TODO: real numbers *)
+ Cil.mkCast ~force:true ~e:arg ~newt:(Gmpz.t_ptr ())
+ else
+ arg)
+ args
+ in
+ (* Building the arguments 3/3:
+ E-ACSL typing: short and other integer types less than in
+ are cast into int *)
+ let args = List.map
+ (fun arg ->
+ match Cil.typeOf arg with
+ | TInt(kind, _) ->
+ if Cil.intTypeIncluded kind IInt then
+ Cil.mkCast ~force:false ~e:arg ~newt:Cil.intType
+ else
+ arg
+ | TVoid _ | TFloat _ | TPtr _ | TArray _ | TFun _ | TNamed _
+ | TComp _ |TEnum _ | TBuiltin_va_list _ ->
+ arg)
+ args
+ in
+ let lty = match Typing.get_integer_ty t with
+ | Typing.Gmp -> Linteger
+ | Typing.C_type ik -> Ctype (TInt (ik, []))
+ | Typing.Other -> t.term_type
+ in
+ let lfs = {
+ lfs_li = li;
+ lfs_lty = lty;
+ lfs_args_lty = args_lty;
+ }
+ in
+ (* Memoization. We MUST guarantee that interval and type bindings
+ for logic vars, terms and predicates from the logic definition of
+ the function are restored after memoization. *)
+ add_interv_bindings lfs;
+ retype lfs;
+ let kf = memo lfs vi_f_typ in
+ remove_interv_bindings lfs;
+ retype lfs;
+ (* The call stmt *)
+ let fundec = Misc.fundec_of_kf kf in
+ let vi_f = fundec.svar in
+ Cil.mkStmtOneInstr
+ (Call (
+ lvl_opt,
+ (Cil.evar vi_f),
+ args,
+ loc))
+ in
+ match Typing.get_integer_ty t with
+ | Typing.C_type _ | Typing.Other ->
+ let res = Env.new_var
+ ~loc
+ ~name
+ env
+ (Some t)
+ (Typing.get_typ t)
+ (fun vi_app _ -> [ mk_call vi_app ])
+ in
+ res
+ | Typing.Gmp ->
+ Env.new_var_and_mpz_init
+ ~loc
+ ~name
+ env
+ (Some t)
+ (fun vi_app _ -> [ mk_call vi_app ])
+
+(**************************************************************************)
+(******************************** Visitor *********************************)
+(**************************************************************************)
+
+(* TODO: Or is it better to directly use E-ACSL's main visitor in [Visit]?
+ The decision should take into account the fact that [Visit] is already
+ very big. *)
+
+let lfunctions_visitor = object (self)
+ inherit Visitor.frama_c_inplace
+ val mutable new_definitions: global list = []
+ method private insert_lfunctions l = l @ new_definitions
+ method !vglob_aux = function
+ | GAnnot(ga, _) as g ->
+ Cil.DoChildrenPost
+ (fun _ -> match ga with
+ | Dfun_or_pred(li, _) ->
+ begin match li.l_labels with
+ | [] ->
+ (* Case of logic definitions WITHOUT labels. *)
+ let kfs = find_kfs li in
+ let loc = Cil_datatype.Location.unknown in
+ let new_decls = List.map
+ (fun kf ->
+ let fundec = Misc.fundec_of_kf kf in
+ let new_g = GFun(fundec, loc) in
+ new_definitions <- new_g :: new_definitions;
+ GFunDecl(Cil.empty_funspec (), fundec.svar, loc))
+ kfs
+ in
+ g :: new_decls
+ | _ :: _ ->
+ (* Case of logic definitions WITH labels. Not yet supported for
+ the time being. Just let it go here: an exception will be raised
+ in [Translate]. *)
+ [g]
+ end
+ | Dvolatile _ | Daxiomatic _ | Dtype _ | Dlemma _ | Dinvariant _
+ | Dtype_annot _ | Dmodel_annot _ | Dcustom_annot _ | Dextended _ ->
+ [g])
+ | GType _ | GCompTag _ | GCompTagDecl _ | GEnumTag _ | GEnumTagDecl _
+ | GVarDecl _ | GFunDecl _ | GVar _ | GFun _ | GAsm _ | GPragma _
+ | GText _ ->
+ Cil.DoChildren
+ method !vfile _ =
+ Cil.DoChildrenPost
+ (fun file ->
+ file.globals <- self#insert_lfunctions file.globals;
+ file)
+end
+
+let do_visit f = Visitor.visitFramacFile lfunctions_visitor f
\ No newline at end of file
diff --git a/src/plugins/e-acsl/lfunctions.mli b/src/plugins/e-acsl/lfunctions.mli
new file mode 100644
index 00000000000..ca4c8ead2ae
--- /dev/null
+++ b/src/plugins/e-acsl/lfunctions.mli
@@ -0,0 +1,56 @@
+(**************************************************************************)
+(* *)
+(* This file is part of Frama-C. *)
+(* *)
+(* Copyright (C) 2007-2018 *)
+(* CEA (Commissariat à l'énergie atomique et aux énergies *)
+(* alternatives) *)
+(* *)
+(* you can redistribute it and/or modify it under the terms of the GNU *)
+(* Lesser General Public License as published by the Free Software *)
+(* Foundation, version 2.1. *)
+(* *)
+(* It is distributed in the hope that it will be useful, *)
+(* but WITHOUT ANY WARRANTY; without even the implied warranty of *)
+(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the *)
+(* GNU Lesser General Public License for more details. *)
+(* *)
+(* See the GNU Lesser General Public License version 2.1 *)
+(* for more details (enclosed in the file licenses/LGPLv2.1). *)
+(* *)
+(**************************************************************************)
+
+open Cil_types
+
+(** Generate C implementations of user-defined logic functions.
+ A logic function can have multiple C implementations depending on
+ the types computed for its arguments.
+ Eg: Consider the following definition: [integer g(integer x) = x]
+ with the following calls: [g(5)] and [g(10*INT_MAX)]
+ They will respectively generate the C prototypes [int g_1(int)]
+ and [long g_2(long)] *)
+
+(**************************************************************************)
+(************** Logic functions without labels ****************************)
+(**************************************************************************)
+
+val generate: loc:location -> Env.t -> term -> logic_info ->
+ exp list -> logic_type list -> varinfo * exp * Env.t
+(** [generate ~loc env t_app li args_exp args_lty] generates the C function
+ corresponding to [t_app] and returns the associated call. *)
+
+val do_visit: Cil_types.file -> unit
+(** Put declarations and definitions of the generated functions in the AST. *)
+
+(**************************************************************************)
+(********************** Forward references ********************************)
+(**************************************************************************)
+
+val predicate_to_exp_ref:
+ (kernel_function -> Env.t -> predicate -> exp * Env.t) ref
+
+val term_to_exp_ref:
+ (kernel_function -> Env.t -> term -> exp * Env.t) ref
+
+val add_cast_ref:
+ (location -> Env.t -> typ option -> bool -> exp -> exp * Env.t) ref
\ No newline at end of file
diff --git a/src/plugins/e-acsl/misc.ml b/src/plugins/e-acsl/misc.ml
index 4956b8633e3..1d3e09cc8cc 100644
--- a/src/plugins/e-acsl/misc.ml
+++ b/src/plugins/e-acsl/misc.ml
@@ -315,6 +315,60 @@ let finite_min_and_max i = match Ival.min_and_max i with
| Some min, Some max -> min, max
| None, _ | _, None -> assert false
+let fundec_of_kf kf = match kf.fundec with
+ | Definition(fundec, _) -> fundec
+ | Declaration _ -> Options.fatal "fundec_of_kf on Declaration"
+
+let is_recursive li =
+ match li.l_body with
+ | LBpred _ | LBnone | LBreads _ | LBinductive _ -> false
+ | LBterm t ->
+ let rec has_recursive_call t = match t.term_node with
+ | TConst _ | TLval _ | TSizeOf _ | TSizeOfStr _ | TAlignOf _
+ | Tnull | TAddrOf _ | TStartOf _ | Tempty_set | Ttypeof _
+ | Ttype _->
+ false
+ | Tapp(li', _, ts) ->
+ if li.l_var_info.lv_name = li'.l_var_info.lv_name then true
+ else List.fold_left (fun b t -> b || has_recursive_call t) false ts
+ | TUnOp(_, t) | TSizeOfE t | TCastE(_, t) | Tat(t, _) | Tlambda(_, t)
+ | Toffset(_, t) | Tbase_addr(_, t) | TAlignOfE t | Tblock_length(_, t)
+ | TLogic_coerce(_, t) | TCoerce(t, _) | Tcomprehension(t, _, _)
+ | Tlet(_, t) ->
+ has_recursive_call t
+ | TBinOp(_, t1, t2) | TCoerceE(t1, t2) | TUpdate(t1, _, t2) ->
+ has_recursive_call t1 || has_recursive_call t2
+ | Trange(t1_opt, t2_opt) ->
+ begin match t1_opt with
+ | None -> begin match t2_opt with
+ | None -> false
+ | Some t2 -> has_recursive_call t2
+ end
+ | Some t1 -> begin match t2_opt with
+ | None -> has_recursive_call t1
+ | Some t2 -> has_recursive_call t1 || has_recursive_call t2
+ end
+ end
+ | Tif(t0, t1, t2) ->
+ has_recursive_call t0 || has_recursive_call t1 || has_recursive_call t2
+ | TDataCons(_, ts) | Tunion ts | Tinter ts ->
+ List.fold_left (fun b t -> b || has_recursive_call t) false ts
+ in
+ has_recursive_call t
+
+let itv_kind i =
+ if Ival.is_bottom i then IInt
+ else match Ival.min_and_max i with
+ | Some l, Some u ->
+ let is_pos = Integer.ge l Integer.zero in
+ let lkind = Cil.intKindForValue l is_pos in
+ let ukind = Cil.intKindForValue u is_pos in
+ (* kind corresponding to the interval *)
+ if Cil.intTypeIncluded lkind ukind then ukind else lkind
+ | None, None -> raise Cil.Not_representable (* GMP *)
+ | None, Some _ | Some _, None ->
+ Kernel.fatal ~current:true "ival: %a" Ival.pretty i
+
(*
Local Variables:
compile-command: "make"
diff --git a/src/plugins/e-acsl/misc.mli b/src/plugins/e-acsl/misc.mli
index 8f12597aa04..e4806f0e157 100644
--- a/src/plugins/e-acsl/misc.mli
+++ b/src/plugins/e-acsl/misc.mli
@@ -93,7 +93,7 @@ val reorder_ast: unit -> unit
* the very top of the file. *)
val cty: logic_type -> typ
-(* Assume that the logic type is indeed a C type. Just return it. *)
+(** Assume that the logic type is indeed a C type. Just return it. *)
val ptr_index: ?loc:location -> ?index:exp -> exp
-> Cil_types.exp * Cil_types.exp
@@ -101,31 +101,39 @@ val ptr_index: ?loc:location -> ?index:exp -> exp
pointer and integer parts. *)
val term_of_li: logic_info -> term
-(* [term_of_li li] assumes that [li.l_body] matches [LBterm t]
+(** [term_of_li li] assumes that [li.l_body] matches [LBterm t]
and returns [t]. *)
val is_set_of_ptr_or_array: logic_type -> bool
-(* Checks whether the given logic type is a set of pointers. *)
+(** Checks whether the given logic type is a set of pointers. *)
val is_range_free: term -> bool
-(* Returns [true] iff the given term does not contain any range. *)
+(** Returns [true] iff the given term does not contain any range. *)
val is_bitfield_pointers: logic_type -> bool
-(* Returns [true] iff the given logic type is a bitfield pointer or a
+(** Returns [true] iff the given logic type is a bitfield pointer or a
set of bitfield pointers. *)
val term_has_lv_from_vi: term -> bool
-(* Return [true] iff the given term contains a variables that originates from
+(** Return [true] iff the given term contains a variables that originates from
a C varinfo, that is a non-purely logic variable. *)
type pred_or_term = PoT_pred of predicate | PoT_term of term
val mk_ptr_sizeof: typ -> location -> exp
-(* [mk_ptr_sizeof ptr_typ loc] takes the pointer typ [ptr_typ] that points
+(** [mk_ptr_sizeof ptr_typ loc] takes the pointer typ [ptr_typ] that points
to a [typ] typ and returns [sizeof(typ)]. *)
val finite_min_and_max: Ival.t -> Integer.t * Integer.t
-(* [finite_min_and_max i] takes the finite ival [i] and returns its bounds *)
+(** [finite_min_and_max i] takes the finite ival [i] and returns its bounds *)
+
+val fundec_of_kf: kernel_function -> fundec
+
+val is_recursive: logic_info -> bool
+(** [is_recursive li] returns true iff [li] is defined recursively. *)
+
+val itv_kind: Ival.t -> ikind
+(** Return the smallest iking that contains the given interval. *)
(*
Local Variables:
diff --git a/src/plugins/e-acsl/tests/bts/oracle/bts1307.res.oracle b/src/plugins/e-acsl/tests/bts/oracle/bts1307.res.oracle
index 15637955c83..827a2632149 100644
--- a/src/plugins/e-acsl/tests/bts/oracle/bts1307.res.oracle
+++ b/src/plugins/e-acsl/tests/bts/oracle/bts1307.res.oracle
@@ -4,23 +4,29 @@
[e-acsl] beginning translation.
[e-acsl] tests/bts/bts1307.i:23: Warning: approximating a real number by a float
[e-acsl] tests/bts/bts1307.i:23: Warning:
- E-ACSL construct `logic function application' is not yet supported.
+ E-ACSL construct `logic functions with no definition nor reads clause'
+ is not yet supported.
Ignoring annotation.
[e-acsl] tests/bts/bts1307.i:23: Warning: approximating a real number by a float
[e-acsl] tests/bts/bts1307.i:23: Warning:
- E-ACSL construct `logic function application' is not yet supported.
+ E-ACSL construct `logic functions with no definition nor reads clause'
+ is not yet supported.
Ignoring annotation.
[e-acsl] tests/bts/bts1307.i:11: Warning: approximating a real number by a float
[e-acsl] tests/bts/bts1307.i:11: Warning:
- E-ACSL construct `logic function application' is not yet supported.
+ E-ACSL construct `logic functions with no definition nor reads clause'
+ is not yet supported.
Ignoring annotation.
[e-acsl] tests/bts/bts1307.i:11: Warning:
- E-ACSL construct `logic function application' is not yet supported.
+ E-ACSL construct `logic functions with no definition nor reads clause'
+ is not yet supported.
Ignoring annotation.
[e-acsl] tests/bts/bts1307.i:11: Warning:
- E-ACSL construct `logic function application' is not yet supported.
+ E-ACSL construct `logic functions with no definition nor reads clause'
+ is not yet supported.
Ignoring annotation.
[e-acsl] tests/bts/bts1307.i:11: Warning:
- E-ACSL construct `logic function application' is not yet supported.
+ E-ACSL construct `logic functions with no definition nor reads clause'
+ is not yet supported.
Ignoring annotation.
[e-acsl] translation done in project "e-acsl".
diff --git a/src/plugins/e-acsl/tests/format/oracle/fprintf.res.oracle b/src/plugins/e-acsl/tests/format/oracle/fprintf.res.oracle
index bfc158802d8..79a76e5072f 100644
--- a/src/plugins/e-acsl/tests/format/oracle/fprintf.res.oracle
+++ b/src/plugins/e-acsl/tests/format/oracle/fprintf.res.oracle
@@ -28,7 +28,8 @@
E-ACSL construct `assigns clause in behavior' is not yet supported.
Ignoring annotation.
[e-acsl] FRAMAC_SHARE/libc/stdio.h:82: Warning:
- E-ACSL construct `logic function application' is not yet supported.
+ E-ACSL construct `logic functions with no definition nor reads clause'
+ is not yet supported.
Ignoring annotation.
[e-acsl] FRAMAC_SHARE/libc/stdio.h:82: Warning:
E-ACSL construct `assigns clause in behavior' is not yet supported.
diff --git a/src/plugins/e-acsl/tests/format/oracle/printf.res.oracle b/src/plugins/e-acsl/tests/format/oracle/printf.res.oracle
index 72731f940f0..61c88433a84 100644
--- a/src/plugins/e-acsl/tests/format/oracle/printf.res.oracle
+++ b/src/plugins/e-acsl/tests/format/oracle/printf.res.oracle
@@ -18,7 +18,7 @@
the generated program may miss memory instrumentation
if there are memory-related annotations.
[e-acsl] FRAMAC_SHARE/libc/string.h:327: Warning:
- E-ACSL construct `logic function application' is not yet supported.
+ E-ACSL construct `logic functions with labels' is not yet supported.
Ignoring annotation.
[e-acsl] FRAMAC_SHARE/libc/string.h:328: Warning:
E-ACSL construct `logic function returning an integer' is not yet supported.
@@ -29,31 +29,36 @@
E-ACSL construct `assigns clause in behavior' is not yet supported.
Ignoring annotation.
[e-acsl] FRAMAC_SHARE/libc/string.h:333: Warning:
- E-ACSL construct `logic function returning an integer' is not yet supported.
+ E-ACSL construct `logic functions performing read accesses'
+ is not yet supported.
Ignoring annotation.
[e-acsl] FRAMAC_SHARE/libc/string.h:143: Warning:
- E-ACSL construct `logic function application' is not yet supported.
+ E-ACSL construct `logic functions with labels' is not yet supported.
Ignoring annotation.
[e-acsl] FRAMAC_SHARE/libc/string.h:157: Warning:
E-ACSL construct `assigns clause in behavior' is not yet supported.
Ignoring annotation.
[e-acsl] FRAMAC_SHARE/libc/string.h:146: Warning:
- E-ACSL construct `user-defined logic type' is not yet supported.
+ E-ACSL construct `logic functions performing read accesses'
+ is not yet supported.
Ignoring annotation.
[e-acsl] FRAMAC_SHARE/libc/string.h:146: Warning:
- E-ACSL construct `user-defined logic type' is not yet supported.
+ E-ACSL construct `logic functions performing read accesses'
+ is not yet supported.
Ignoring annotation.
[e-acsl] FRAMAC_SHARE/libc/string.h:153: Warning:
- E-ACSL construct `user-defined logic type' is not yet supported.
+ E-ACSL construct `logic functions performing read accesses'
+ is not yet supported.
Ignoring annotation.
[e-acsl] FRAMAC_SHARE/libc/string.h:111: Warning:
- E-ACSL construct `logic function application' is not yet supported.
+ E-ACSL construct `logic functions with labels' is not yet supported.
Ignoring annotation.
[e-acsl] FRAMAC_SHARE/libc/string.h:111: Warning:
E-ACSL construct `assigns clause in behavior' is not yet supported.
Ignoring annotation.
[e-acsl] FRAMAC_SHARE/libc/string.h:113: Warning:
- E-ACSL construct `logic function returning an integer' is not yet supported.
+ E-ACSL construct `logic functions performing read accesses'
+ is not yet supported.
Ignoring annotation.
[e-acsl] FRAMAC_SHARE/libc/string.h:113: Warning:
E-ACSL construct `assigns clause in behavior' is not yet supported.
diff --git a/src/plugins/e-acsl/tests/gmp/functions.c b/src/plugins/e-acsl/tests/gmp/functions.c
new file mode 100644
index 00000000000..61bb3857359
--- /dev/null
+++ b/src/plugins/e-acsl/tests/gmp/functions.c
@@ -0,0 +1,71 @@
+/* run.config
+ COMMENT: logic functions without labels
+*/
+
+/*@ predicate p1(int x, int y) = x + y > 0; */
+/*@ predicate p2(integer x, integer y) = x + y > 0; */
+
+/*@ logic integer f1(integer x, integer y) = x + y; */
+
+// E-ACSL integer typing:
+// types less than int are considered as int
+/*@ logic char h_char(char c) = c; */
+/*@ logic short h_short(short s) = s; */
+
+/*@ logic int g_hidden(int x) = x; */
+/*@ logic int g(int x) = g_hidden(x); */
+
+struct mystruct { int k, l; };
+typedef struct mystruct mystruct;
+/*@ logic mystruct t1(mystruct m) = m; */
+/*@ logic integer t2(mystruct m) = m.k + m.l; */
+
+// To test function call in other than assert:
+/*@ predicate k_pred(integer x) = x > 0; */
+/*@ requires k_pred(x); */
+void k(int x) {}
+
+// To test non-interference with global inits:
+int glob = 5;
+
+// To test that functions that are never called are not generated:
+/*@ predicate never_called(int x) = x == x; */
+
+/*@ logic double f2(double x) = (double)(1/x); */ /* handle in MR !226 */
+
+// To test not_yet:
+/*@ predicate p_notyet{L}(integer x) = x > 0; */
+/*@ logic integer f_notyet{L}(integer x) = x; */
+
+int main (void) {
+ int x = 1, y = 2;
+ /*@ assert p1(x, y); */ ;
+ /*@ assert p2(3, 4); */ ;
+ /*@ assert p2(5, 99999999999999999999999999999); */ ;
+
+ /*@ assert f1(x, y) == 3; */ ;
+ /*@ assert p2(x, f1(3, 4)); */ ;
+ /*@ assert f1(9, 99999999999999999999999999999) > 0; */ ;
+ /*@ assert f1(99999999999999999999999999999,
+ 99999999999999999999999999999) ==
+ 199999999999999999999999999998; */ ;
+
+ /*@ assert g(x) == x; */ ;
+
+ char c = 'c';
+ /*@ assert h_char(c) == c; */ ;
+ short s = 1;
+ /*@ assert h_short(s) == s; */ ;
+
+ mystruct m;
+ m.k = 8;
+ m.l = 9;
+ /*@ assert t2(t1(m)) == 17; */ ;
+
+ k(9);
+
+ double d = 2.0;
+ /*@ assert f2(d) > 0; */ ;
+ /*@ assert p_notyet(27); */ ;
+ /*@ assert f_notyet(27) == 27; */ ;
+}
\ No newline at end of file
diff --git a/src/plugins/e-acsl/tests/gmp/functions_contiki.c b/src/plugins/e-acsl/tests/gmp/functions_contiki.c
new file mode 100644
index 00000000000..382a1a64b9e
--- /dev/null
+++ b/src/plugins/e-acsl/tests/gmp/functions_contiki.c
@@ -0,0 +1,28 @@
+/* run.config
+ COMMENT: functions used in Contiki
+*/
+
+#include <stdlib.h>
+#include <limits.h>
+
+struct list {
+ struct list *next;
+ int value;
+};
+
+/*@
+ logic integer length_aux(struct list *l, integer n) =
+ n < 0 ? -1 :
+ l == NULL ? n :
+ n < INT_MAX ? length_aux(l->next, n+1) :
+ -1;
+ logic integer length(struct list *l) = length_aux(l, 0);
+*/
+
+int main (void) {
+ struct list node1, node2, node3;
+ node1.next = &node2;
+ node2.next = &node3;
+ struct list *l = &node1;
+ /*@ assert length(l) == 3; */ ;
+}
\ No newline at end of file
diff --git a/src/plugins/e-acsl/tests/gmp/functions_rec.c b/src/plugins/e-acsl/tests/gmp/functions_rec.c
new file mode 100644
index 00000000000..990f4826c59
--- /dev/null
+++ b/src/plugins/e-acsl/tests/gmp/functions_rec.c
@@ -0,0 +1,30 @@
+/* run.config
+ COMMENT: recursive logic functions
+*/
+
+/*@ logic integer f1(integer n) =
+ n <= 0 ? 0 : f1(n - 1) + n; */
+
+/*@ logic integer f2(integer n) =
+ n < 0 ? 1 : f2(n - 1)*f2(n - 2)/f2(n - 3); */
+
+/*@ logic integer g(integer n) = 0; */
+/*@ logic integer f3(integer n) =
+ n > 0 ? g(n)*f3(n - 1) - 5 : g(n + 1); */
+
+/*@ logic integer f4(integer n) =
+ n < 100 ? f4(n + 1) :
+ n < 0x7fffffffffffffffL ? 0x7fffffffffffffffL :
+ 6; */
+
+int main (void) {
+ /*@ assert f1(0) == 0; */ ;
+ /*@ assert f1(1) == 1; */ ;
+ /*@ assert f1(100) == 5050; */ ;
+
+ /*@ assert f2(7) == 1; */ ;
+
+ /*@ assert f3(6) == -5; */ ;
+
+ /*@assert f4(9) > 0; */ ;
+}
\ No newline at end of file
diff --git a/src/plugins/e-acsl/tests/gmp/oracle/functions.0.res.oracle b/src/plugins/e-acsl/tests/gmp/oracle/functions.0.res.oracle
new file mode 100644
index 00000000000..8784a09a0db
--- /dev/null
+++ b/src/plugins/e-acsl/tests/gmp/oracle/functions.0.res.oracle
@@ -0,0 +1,41 @@
+[e-acsl] beginning translation.
+[e-acsl] tests/gmp/functions.c:34: Warning:
+ E-ACSL construct `logic functions with no definition nor reads clause'
+ is not yet supported.
+ Ignoring annotation.
+[e-acsl] tests/gmp/functions.c:69: Warning:
+ E-ACSL construct `logic functions with labels' is not yet supported.
+ Ignoring annotation.
+[e-acsl] tests/gmp/functions.c:70: Warning:
+ E-ACSL construct `logic functions with labels' is not yet supported.
+ Ignoring annotation.
+[e-acsl] translation done in project "e-acsl".
+[eva] Analyzing a complete application starting at main
+[eva] Computing initial state
+[eva] Initial state computed
+[eva:initial-state] Values of globals at initialization
+ __e_acsl_init ∈ [--..--]
+ __e_acsl_heap_allocation_size ∈ [--..--]
+ __e_acsl_math_HUGE_VAL ∈ [-1.79769313486e+308 .. 1.79769313486e+308]
+ __e_acsl_math_HUGE_VALF ∈ [-3.40282346639e+38 .. 3.40282346639e+38]
+ __e_acsl_math_INFINITY ∈ [-1.79769313486e+308 .. 1.79769313486e+308]
+ glob ∈ {5}
+[eva] using specification for function __e_acsl_memory_init
+[eva] using specification for function __e_acsl_assert
+[eva] using specification for function __gmpz_init_set_str
+[eva] using specification for function __gmpz_init_set
+[eva] using specification for function __gmpz_init_set_si
+[eva] using specification for function __gmpz_init
+[eva] using specification for function __gmpz_add
+[eva] using specification for function __gmpz_cmp
+[eva] using specification for function __gmpz_clear
+[eva:alarm] tests/gmp/functions.c:44: Warning:
+ function __e_acsl_assert: precondition got status unknown.
+[eva:alarm] tests/gmp/functions.c:47: Warning:
+ function __e_acsl_assert: precondition got status unknown.
+[eva:alarm] tests/gmp/functions.c:48: Warning:
+ accessing uninitialized left-value.
+ assert \initialized((__e_acsl_mpz_struct *)__gen_e_acsl_f1_tapp_3);
+[eva:alarm] :0: Warning:
+ function __gmpz_init_set: precondition ¬\initialized(z) got status invalid.
+[eva] done for function main
diff --git a/src/plugins/e-acsl/tests/gmp/oracle/functions.1.res.oracle b/src/plugins/e-acsl/tests/gmp/oracle/functions.1.res.oracle
new file mode 100644
index 00000000000..46f1bb7194a
--- /dev/null
+++ b/src/plugins/e-acsl/tests/gmp/oracle/functions.1.res.oracle
@@ -0,0 +1,43 @@
+[e-acsl] beginning translation.
+[e-acsl] tests/gmp/functions.c:34: Warning:
+ E-ACSL construct `logic functions with no definition nor reads clause'
+ is not yet supported.
+ Ignoring annotation.
+[e-acsl] tests/gmp/functions.c:69: Warning:
+ E-ACSL construct `logic functions with labels' is not yet supported.
+ Ignoring annotation.
+[e-acsl] tests/gmp/functions.c:70: Warning:
+ E-ACSL construct `logic functions with labels' is not yet supported.
+ Ignoring annotation.
+[e-acsl] translation done in project "e-acsl".
+[eva] Analyzing a complete application starting at main
+[eva] Computing initial state
+[eva] Initial state computed
+[eva:initial-state] Values of globals at initialization
+ __e_acsl_init ∈ [--..--]
+ __e_acsl_heap_allocation_size ∈ [--..--]
+ __e_acsl_math_HUGE_VAL ∈ [-1.79769313486e+308 .. 1.79769313486e+308]
+ __e_acsl_math_HUGE_VALF ∈ [-3.40282346639e+38 .. 3.40282346639e+38]
+ __e_acsl_math_INFINITY ∈ [-1.79769313486e+308 .. 1.79769313486e+308]
+ glob ∈ {5}
+[eva] using specification for function __e_acsl_memory_init
+[eva] using specification for function __gmpz_init_set_si
+[eva] using specification for function __gmpz_init
+[eva] using specification for function __gmpz_add
+[eva] using specification for function __gmpz_cmp
+[eva] using specification for function __gmpz_clear
+[eva] using specification for function __e_acsl_assert
+[eva:alarm] tests/gmp/functions.c:42: Warning:
+ function __e_acsl_assert: precondition got status unknown.
+[eva:alarm] tests/gmp/functions.c:43: Warning:
+ function __e_acsl_assert: precondition got status unknown.
+[eva] using specification for function __gmpz_init_set_str
+[eva] using specification for function __gmpz_init_set
+[eva:alarm] tests/gmp/functions.c:44: Warning:
+ function __e_acsl_assert: precondition got status unknown.
+[eva:alarm] tests/gmp/functions.c:46: Warning:
+ accessing uninitialized left-value.
+ assert \initialized((__e_acsl_mpz_struct *)__gen_e_acsl_f1_tapp);
+[eva:alarm] :0: Warning:
+ function __gmpz_init_set: precondition ¬\initialized(z) got status invalid.
+[eva] done for function main
diff --git a/src/plugins/e-acsl/tests/gmp/oracle/functions_contiki.0.res.oracle b/src/plugins/e-acsl/tests/gmp/oracle/functions_contiki.0.res.oracle
new file mode 100644
index 00000000000..c46fcfd437f
--- /dev/null
+++ b/src/plugins/e-acsl/tests/gmp/oracle/functions_contiki.0.res.oracle
@@ -0,0 +1,25 @@
+[e-acsl] beginning translation.
+[e-acsl] tests/gmp/functions_contiki.c:27: Warning:
+ E-ACSL construct `logic functions with labels' is not yet supported.
+ Ignoring annotation.
+[e-acsl] translation done in project "e-acsl".
+[eva] Analyzing a complete application starting at main
+[eva] Computing initial state
+[eva] Initial state computed
+[eva:initial-state] Values of globals at initialization
+ __e_acsl_init ∈ [--..--]
+ __e_acsl_heap_allocation_size ∈ [--..--]
+ __e_acsl_math_HUGE_VAL ∈ [-1.79769313486e+308 .. 1.79769313486e+308]
+ __e_acsl_math_HUGE_VALF ∈ [-3.40282346639e+38 .. 3.40282346639e+38]
+ __e_acsl_math_INFINITY ∈ [-1.79769313486e+308 .. 1.79769313486e+308]
+[eva] using specification for function __e_acsl_memory_init
+[eva] using specification for function __e_acsl_store_block
+[eva] using specification for function __e_acsl_initialize
+[eva] using specification for function __e_acsl_full_init
+[eva] tests/gmp/functions_contiki.c:27:
+ cannot evaluate ACSL term, unsupported ACSL construct: logic function length
+[eva:alarm] tests/gmp/functions_contiki.c:27: Warning:
+ assertion got status unknown.
+[eva] using specification for function __e_acsl_delete_block
+[eva] using specification for function __e_acsl_memory_clean
+[eva] done for function main
diff --git a/src/plugins/e-acsl/tests/gmp/oracle/functions_contiki.1.res.oracle b/src/plugins/e-acsl/tests/gmp/oracle/functions_contiki.1.res.oracle
new file mode 100644
index 00000000000..c46fcfd437f
--- /dev/null
+++ b/src/plugins/e-acsl/tests/gmp/oracle/functions_contiki.1.res.oracle
@@ -0,0 +1,25 @@
+[e-acsl] beginning translation.
+[e-acsl] tests/gmp/functions_contiki.c:27: Warning:
+ E-ACSL construct `logic functions with labels' is not yet supported.
+ Ignoring annotation.
+[e-acsl] translation done in project "e-acsl".
+[eva] Analyzing a complete application starting at main
+[eva] Computing initial state
+[eva] Initial state computed
+[eva:initial-state] Values of globals at initialization
+ __e_acsl_init ∈ [--..--]
+ __e_acsl_heap_allocation_size ∈ [--..--]
+ __e_acsl_math_HUGE_VAL ∈ [-1.79769313486e+308 .. 1.79769313486e+308]
+ __e_acsl_math_HUGE_VALF ∈ [-3.40282346639e+38 .. 3.40282346639e+38]
+ __e_acsl_math_INFINITY ∈ [-1.79769313486e+308 .. 1.79769313486e+308]
+[eva] using specification for function __e_acsl_memory_init
+[eva] using specification for function __e_acsl_store_block
+[eva] using specification for function __e_acsl_initialize
+[eva] using specification for function __e_acsl_full_init
+[eva] tests/gmp/functions_contiki.c:27:
+ cannot evaluate ACSL term, unsupported ACSL construct: logic function length
+[eva:alarm] tests/gmp/functions_contiki.c:27: Warning:
+ assertion got status unknown.
+[eva] using specification for function __e_acsl_delete_block
+[eva] using specification for function __e_acsl_memory_clean
+[eva] done for function main
diff --git a/src/plugins/e-acsl/tests/gmp/oracle/functions_rec.0.res.oracle b/src/plugins/e-acsl/tests/gmp/oracle/functions_rec.0.res.oracle
new file mode 100644
index 00000000000..e3a0950b8f7
--- /dev/null
+++ b/src/plugins/e-acsl/tests/gmp/oracle/functions_rec.0.res.oracle
@@ -0,0 +1,25 @@
+[e-acsl] beginning translation.
+[e-acsl] translation done in project "e-acsl".
+[eva] Analyzing a complete application starting at main
+[eva] Computing initial state
+[eva] Initial state computed
+[eva:initial-state] Values of globals at initialization
+ __e_acsl_init ∈ [--..--]
+ __e_acsl_heap_allocation_size ∈ [--..--]
+ __e_acsl_math_HUGE_VAL ∈ [-1.79769313486e+308 .. 1.79769313486e+308]
+ __e_acsl_math_HUGE_VALF ∈ [-3.40282346639e+38 .. 3.40282346639e+38]
+ __e_acsl_math_INFINITY ∈ [-1.79769313486e+308 .. 1.79769313486e+308]
+[eva] using specification for function __e_acsl_memory_init
+[eva] tests/gmp/functions_rec.c:21:
+ cannot evaluate ACSL term, unsupported ACSL construct: logic function f1
+[eva:alarm] tests/gmp/functions_rec.c:21: Warning: assertion got status unknown.
+[eva] using specification for function __gmpz_init
+[eva:alarm] tests/gmp/functions_rec.c:21: Warning:
+ accessing uninitialized left-value.
+ assert \initialized((__e_acsl_mpz_struct *)__gen_e_acsl_f1_tapp);
+[eva] using specification for function __gmpz_init_set_si
+[eva] using specification for function __gmpz_init_set
+[eva] using specification for function __gmpz_clear
+[eva:alarm] :0: Warning:
+ function __gmpz_init_set: precondition ¬\initialized(z) got status invalid.
+[eva] done for function main
diff --git a/src/plugins/e-acsl/tests/gmp/oracle/functions_rec.1.res.oracle b/src/plugins/e-acsl/tests/gmp/oracle/functions_rec.1.res.oracle
new file mode 100644
index 00000000000..899afbf364f
--- /dev/null
+++ b/src/plugins/e-acsl/tests/gmp/oracle/functions_rec.1.res.oracle
@@ -0,0 +1,47 @@
+[e-acsl] beginning translation.
+[e-acsl] translation done in project "e-acsl".
+[eva] Analyzing a complete application starting at main
+[eva] Computing initial state
+[eva] Initial state computed
+[eva:initial-state] Values of globals at initialization
+ __e_acsl_init ∈ [--..--]
+ __e_acsl_heap_allocation_size ∈ [--..--]
+ __e_acsl_math_HUGE_VAL ∈ [-1.79769313486e+308 .. 1.79769313486e+308]
+ __e_acsl_math_HUGE_VALF ∈ [-3.40282346639e+38 .. 3.40282346639e+38]
+ __e_acsl_math_INFINITY ∈ [-1.79769313486e+308 .. 1.79769313486e+308]
+[eva] using specification for function __e_acsl_memory_init
+[eva] tests/gmp/functions_rec.c:21:
+ cannot evaluate ACSL term, unsupported ACSL construct: logic function f1
+[eva:alarm] tests/gmp/functions_rec.c:21: Warning: assertion got status unknown.
+[eva] using specification for function __gmpz_init
+[eva:alarm] tests/gmp/functions_rec.c:21: Warning:
+ accessing uninitialized left-value.
+ assert \initialized((__e_acsl_mpz_struct *)__gen_e_acsl_f1_tapp);
+[eva] using specification for function __gmpz_init_set_si
+[eva] using specification for function __gmpz_cmp
+[eva] using specification for function __gmpz_init_set
+[eva] using specification for function __gmpz_clear
+[eva] using specification for function __gmpz_sub
+[eva:alarm] tests/gmp/functions_rec.c:6: Warning:
+ accessing uninitialized left-value.
+ assert \initialized((__e_acsl_mpz_struct *)__gen_e_acsl_sub);
+[eva:alarm] tests/gmp/functions_rec.c:6: Warning:
+ accessing uninitialized left-value.
+ assert \initialized((__e_acsl_mpz_struct *)__gen_e_acsl_f1_tapp_2);
+[eva] tests/gmp/functions_rec.c:6: Warning:
+ recursive call during value analysis
+ of __gen_e_acsl_f1_2 (__gen_e_acsl_f1_2 <- __gen_e_acsl_f1_2 :: tests/gmp/functions_rec.c:6 <-
+ __gen_e_acsl_f1 :: tests/gmp/functions_rec.c:21 <-
+ main).
+ Assuming the call has no effect. The analysis will be unsound.
+[eva:alarm] tests/gmp/functions_rec.c:6: Warning:
+ accessing uninitialized left-value.
+ assert \initialized((__e_acsl_mpz_struct *)__gen_e_acsl_sub_2);
+[eva:alarm] tests/gmp/functions_rec.c:6: Warning:
+ accessing uninitialized left-value.
+ assert \initialized((__e_acsl_mpz_struct *)__gen_e_acsl_f1_tapp_3);
+[eva] using specification for function __gen_e_acsl_f1_2
+[eva] using specification for function __gmpz_add
+[eva:alarm] :0: Warning:
+ function __gmpz_init_set: precondition ¬\initialized(z) got status invalid.
+[eva] done for function main
diff --git a/src/plugins/e-acsl/tests/gmp/oracle/gen_functions.c b/src/plugins/e-acsl/tests/gmp/oracle/gen_functions.c
new file mode 100644
index 00000000000..0c716f6c8bb
--- /dev/null
+++ b/src/plugins/e-acsl/tests/gmp/oracle/gen_functions.c
@@ -0,0 +1,420 @@
+/* Generated by Frama-C */
+#include "stdio.h"
+#include "stdlib.h"
+struct mystruct {
+ int k ;
+ int l ;
+};
+typedef struct mystruct mystruct;
+/*@ predicate p1(int x, int y) = x + y > 0;
+ */
+int __gen_e_acsl_p1(int __gen_e_acsl_x_arg, int __gen_e_acsl_y_arg);
+
+/*@ predicate p2(ℤ x, ℤ y) = x + y > 0;
+
+*/
+int __gen_e_acsl_p2_2(int __gen_e_acsl_x_arg,
+ __e_acsl_mpz_struct * __gen_e_acsl_y_arg);
+
+int __gen_e_acsl_p2(int __gen_e_acsl_x_arg, int __gen_e_acsl_y_arg);
+
+int __gen_e_acsl_p2_3(int __gen_e_acsl_x_arg, long __gen_e_acsl_y_arg);
+
+/*@ logic ℤ f1(ℤ x, ℤ y) = x + y;
+
+*/
+long __gen_e_acsl_f1(int __gen_e_acsl_x_arg, int __gen_e_acsl_y_arg);
+
+void __gen_e_acsl_f1_2(__e_acsl_mpz_struct * __retres_arg,
+ int __gen_e_acsl_x_arg,
+ __e_acsl_mpz_struct * __gen_e_acsl_y_arg);
+
+void __gen_e_acsl_f1_3(__e_acsl_mpz_struct * __retres_arg,
+ __e_acsl_mpz_struct * __gen_e_acsl_x_arg,
+ __e_acsl_mpz_struct * __gen_e_acsl_y_arg);
+
+/*@ logic char h_char(char c) = c;
+ */
+char __gen_e_acsl_h_char(int __gen_e_acsl_c_arg);
+
+/*@ logic short h_short(short s) = s;
+ */
+short __gen_e_acsl_h_short(int __gen_e_acsl_s_arg);
+
+/*@ logic int g_hidden(int x) = x;
+ */
+int __gen_e_acsl_g_hidden(int __gen_e_acsl_x_arg);
+
+/*@ logic int g(int x) = g_hidden(x);
+ */
+int __gen_e_acsl_g(int __gen_e_acsl_x_arg);
+
+/*@ logic mystruct t1(mystruct m) = m;
+ */
+mystruct __gen_e_acsl_t1(mystruct __gen_e_acsl_m_arg);
+
+/*@ logic ℤ t2(mystruct m) = m.k + m.l;
+ */
+long __gen_e_acsl_t2(mystruct __gen_e_acsl_m_arg);
+
+/*@ predicate k_pred(ℤ x) = x > 0;
+
+*/
+int __gen_e_acsl_k_pred(int __gen_e_acsl_x_arg);
+
+/*@ requires k_pred(x); */
+void __gen_e_acsl_k(int x);
+
+void k(int x)
+{
+ return;
+}
+
+int glob = 5;
+/*@ predicate never_called(int x) = x ≡ x;
+ */
+/*@ logic double f2(double x) = (double)(1 / x);
+ */
+double __gen_e_acsl_f2(double __gen_e_acsl_x_arg);
+
+/*@ predicate p_notyet{L}(ℤ x) = x > 0;
+ */
+/*@ logic ℤ f_notyet{L}(ℤ x) = x;
+
+*/
+int main(void)
+{
+ int __retres;
+ mystruct m;
+ __e_acsl_memory_init((int *)0,(char ***)0,(size_t)8);
+ int x = 1;
+ int y = 2;
+ /*@ assert p1(x, y); */
+ {
+ int __gen_e_acsl_p1_tapp;
+ __gen_e_acsl_p1_tapp = __gen_e_acsl_p1(x,y);
+ __e_acsl_assert(__gen_e_acsl_p1_tapp,(char *)"Assertion",(char *)"main",
+ (char *)"p1(x, y)",42);
+ }
+ /*@ assert p2(3, 4); */
+ {
+ int __gen_e_acsl_p2_tapp;
+ __gen_e_acsl_p2_tapp = __gen_e_acsl_p2(3,4);
+ __e_acsl_assert(__gen_e_acsl_p2_tapp,(char *)"Assertion",(char *)"main",
+ (char *)"p2(3, 4)",43);
+ }
+ /*@ assert p2(5, 99999999999999999999999999999); */
+ {
+ __e_acsl_mpz_t __gen_e_acsl_;
+ int __gen_e_acsl_p2_tapp_2;
+ __gmpz_init_set_str(__gen_e_acsl_,"99999999999999999999999999999",10);
+ __gen_e_acsl_p2_tapp_2 = __gen_e_acsl_p2_2(5,
+ (__e_acsl_mpz_struct *)__gen_e_acsl_);
+ __e_acsl_assert(__gen_e_acsl_p2_tapp_2,(char *)"Assertion",
+ (char *)"main",
+ (char *)"p2(5, 99999999999999999999999999999)",44);
+ __gmpz_clear(__gen_e_acsl_);
+ }
+ /*@ assert f1(x, y) ≡ 3; */
+ {
+ long __gen_e_acsl_f1_tapp;
+ __gen_e_acsl_f1_tapp = __gen_e_acsl_f1(x,y);
+ __e_acsl_assert(__gen_e_acsl_f1_tapp == 3L,(char *)"Assertion",
+ (char *)"main",(char *)"f1(x, y) == 3",46);
+ }
+ /*@ assert p2(x, f1(3, 4)); */
+ {
+ long __gen_e_acsl_f1_tapp_2;
+ int __gen_e_acsl_p2_tapp_3;
+ __gen_e_acsl_f1_tapp_2 = __gen_e_acsl_f1(3,4);
+ __gen_e_acsl_p2_tapp_3 = __gen_e_acsl_p2_3(x,__gen_e_acsl_f1_tapp_2);
+ __e_acsl_assert(__gen_e_acsl_p2_tapp_3,(char *)"Assertion",
+ (char *)"main",(char *)"p2(x, f1(3, 4))",47);
+ }
+ /*@ assert f1(9, 99999999999999999999999999999) > 0; */
+ {
+ __e_acsl_mpz_t __gen_e_acsl__4;
+ __e_acsl_mpz_t __gen_e_acsl_f1_tapp_3;
+ __e_acsl_mpz_t __gen_e_acsl__5;
+ int __gen_e_acsl_gt_3;
+ __gmpz_init_set_str(__gen_e_acsl__4,"99999999999999999999999999999",10);
+ __gmpz_init(__gen_e_acsl_f1_tapp_3);
+ /*@ assert
+ Eva: initialization:
+ \initialized((__e_acsl_mpz_struct *)__gen_e_acsl_f1_tapp_3);
+ */
+ __gen_e_acsl_f1_2((__e_acsl_mpz_struct *)__gen_e_acsl_f1_tapp_3,9,
+ (__e_acsl_mpz_struct *)__gen_e_acsl__4);
+ __gmpz_init_set_si(__gen_e_acsl__5,0L);
+ __gen_e_acsl_gt_3 = __gmpz_cmp((__e_acsl_mpz_struct const *)(__gen_e_acsl_f1_tapp_3),
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl__5));
+ __e_acsl_assert(__gen_e_acsl_gt_3 > 0,(char *)"Assertion",(char *)"main",
+ (char *)"f1(9, 99999999999999999999999999999) > 0",48);
+ __gmpz_clear(__gen_e_acsl__4);
+ __gmpz_clear(__gen_e_acsl_f1_tapp_3);
+ __gmpz_clear(__gen_e_acsl__5);
+ }
+ /*@ assert
+ f1(99999999999999999999999999999, 99999999999999999999999999999) ≡
+ 199999999999999999999999999998;
+ */
+ {
+ __e_acsl_mpz_t __gen_e_acsl__6;
+ __e_acsl_mpz_t __gen_e_acsl_f1_tapp_4;
+ __e_acsl_mpz_t __gen_e_acsl__7;
+ int __gen_e_acsl_eq;
+ __gmpz_init_set_str(__gen_e_acsl__6,"99999999999999999999999999999",10);
+ __gmpz_init(__gen_e_acsl_f1_tapp_4);
+ __gen_e_acsl_f1_3((__e_acsl_mpz_struct *)__gen_e_acsl_f1_tapp_4,
+ (__e_acsl_mpz_struct *)__gen_e_acsl__6,
+ (__e_acsl_mpz_struct *)__gen_e_acsl__6);
+ __gmpz_init_set_str(__gen_e_acsl__7,"199999999999999999999999999998",10);
+ __gen_e_acsl_eq = __gmpz_cmp((__e_acsl_mpz_struct const *)(__gen_e_acsl_f1_tapp_4),
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl__7));
+ __e_acsl_assert(__gen_e_acsl_eq == 0,(char *)"Assertion",(char *)"main",
+ (char *)"f1(99999999999999999999999999999, 99999999999999999999999999999) ==\n199999999999999999999999999998",
+ 49);
+ __gmpz_clear(__gen_e_acsl__6);
+ __gmpz_clear(__gen_e_acsl_f1_tapp_4);
+ __gmpz_clear(__gen_e_acsl__7);
+ }
+ /*@ assert g(x) ≡ x; */
+ {
+ int __gen_e_acsl_g_tapp;
+ __gen_e_acsl_g_tapp = __gen_e_acsl_g(x);
+ __e_acsl_assert(__gen_e_acsl_g_tapp == x,(char *)"Assertion",
+ (char *)"main",(char *)"g(x) == x",53);
+ }
+ char c = (char)'c';
+ /*@ assert h_char(c) ≡ c; */
+ {
+ char __gen_e_acsl_h_char_tapp;
+ __gen_e_acsl_h_char_tapp = __gen_e_acsl_h_char((int)c);
+ __e_acsl_assert((int)__gen_e_acsl_h_char_tapp == (int)c,
+ (char *)"Assertion",(char *)"main",
+ (char *)"h_char(c) == c",56);
+ }
+ short s = (short)1;
+ /*@ assert h_short(s) ≡ s; */
+ {
+ short __gen_e_acsl_h_short_tapp;
+ __gen_e_acsl_h_short_tapp = __gen_e_acsl_h_short((int)s);
+ __e_acsl_assert((int)__gen_e_acsl_h_short_tapp == (int)s,
+ (char *)"Assertion",(char *)"main",
+ (char *)"h_short(s) == s",58);
+ }
+ m.k = 8;
+ m.l = 9;
+ /*@ assert t2(t1(m)) ≡ 17; */
+ {
+ mystruct __gen_e_acsl_t1_tapp;
+ long __gen_e_acsl_t2_tapp;
+ __gen_e_acsl_t1_tapp = __gen_e_acsl_t1(m);
+ __gen_e_acsl_t2_tapp = __gen_e_acsl_t2(__gen_e_acsl_t1_tapp);
+ __e_acsl_assert(__gen_e_acsl_t2_tapp == 17L,(char *)"Assertion",
+ (char *)"main",(char *)"t2(t1(m)) == 17",63);
+ }
+ __gen_e_acsl_k(9);
+ double d = 2.0;
+ /*@ assert f2(d) > 0; */
+ {
+ double __gen_e_acsl_f2_tapp;
+ __gen_e_acsl_f2_tapp = __gen_e_acsl_f2(d);
+ __e_acsl_assert(__gen_e_acsl_f2_tapp > (double)0,(char *)"Assertion",
+ (char *)"main",(char *)"f2(d) > 0",68);
+ }
+ /*@ assert p_notyet(27); */ ;
+ /*@ assert f_notyet(27) ≡ 27; */ ;
+ __retres = 0;
+ return __retres;
+}
+
+/*@ requires k_pred(x); */
+void __gen_e_acsl_k(int x)
+{
+ {
+ int __gen_e_acsl_k_pred_tapp;
+ __gen_e_acsl_k_pred_tapp = __gen_e_acsl_k_pred(x);
+ __e_acsl_assert(__gen_e_acsl_k_pred_tapp,(char *)"Precondition",
+ (char *)"k",(char *)"k_pred(x)",25);
+ }
+ k(x);
+ return;
+}
+
+double __gen_e_acsl_f2(double __gen_e_acsl_x_arg)
+{
+ double __retres;
+ __retres = (double)((long double)1 / __gen_e_acsl_x_arg);
+ return __retres;
+}
+
+int __gen_e_acsl_k_pred(int __gen_e_acsl_x_arg)
+{
+ int __retres;
+ __retres = __gen_e_acsl_x_arg > 0;
+ return __retres;
+}
+
+long __gen_e_acsl_t2(mystruct __gen_e_acsl_m_arg)
+{
+ long __retres;
+ __retres = __gen_e_acsl_m_arg.k + (long)__gen_e_acsl_m_arg.l;
+ return __retres;
+}
+
+mystruct __gen_e_acsl_t1(mystruct __gen_e_acsl_m_arg)
+{
+ mystruct __retres;
+ __retres = __gen_e_acsl_m_arg;
+ return __retres;
+}
+
+int __gen_e_acsl_g(int __gen_e_acsl_x_arg)
+{
+ int __retres;
+ int __gen_e_acsl_g_hidden_tapp;
+ __gen_e_acsl_g_hidden_tapp = __gen_e_acsl_g_hidden(__gen_e_acsl_x_arg);
+ __retres = __gen_e_acsl_g_hidden_tapp;
+ return __retres;
+}
+
+int __gen_e_acsl_g_hidden(int __gen_e_acsl_x_arg)
+{
+ int __retres;
+ __retres = __gen_e_acsl_x_arg;
+ return __retres;
+}
+
+short __gen_e_acsl_h_short(int __gen_e_acsl_s_arg)
+{
+ int __retres;
+ __retres = (short)__gen_e_acsl_s_arg;
+ return __retres;
+}
+
+char __gen_e_acsl_h_char(int __gen_e_acsl_c_arg)
+{
+ int __retres;
+ __retres = (char)__gen_e_acsl_c_arg;
+ return __retres;
+}
+
+void __gen_e_acsl_f1_3(__e_acsl_mpz_struct * __retres_arg,
+ __e_acsl_mpz_struct * __gen_e_acsl_x_arg,
+ __e_acsl_mpz_struct * __gen_e_acsl_y_arg)
+{
+ __e_acsl_mpz_t __gen_e_acsl_x_4;
+ __e_acsl_mpz_t __gen_e_acsl_y_4;
+ __e_acsl_mpz_t __gen_e_acsl_add_4;
+ __gmpz_init_set(__gen_e_acsl_x_4,
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_x_arg));
+ __gmpz_init_set(__gen_e_acsl_y_4,
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_y_arg));
+ __gmpz_init(__gen_e_acsl_add_4);
+ __gmpz_add(__gen_e_acsl_add_4,
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_x_4),
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_y_4));
+ __gmpz_init_set(__retres_arg,
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_add_4));
+ __gmpz_clear(__gen_e_acsl_x_4);
+ __gmpz_clear(__gen_e_acsl_y_4);
+ __gmpz_clear(__gen_e_acsl_add_4);
+ return;
+}
+
+void __gen_e_acsl_f1_2(__e_acsl_mpz_struct * __retres_arg,
+ int __gen_e_acsl_x_arg,
+ __e_acsl_mpz_struct * __gen_e_acsl_y_arg)
+{
+ __e_acsl_mpz_t __gen_e_acsl_y_3;
+ __e_acsl_mpz_t __gen_e_acsl_x_3;
+ __e_acsl_mpz_t __gen_e_acsl_add_3;
+ __gmpz_init_set(__gen_e_acsl_y_3,
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_y_arg));
+ __gmpz_init_set_si(__gen_e_acsl_x_3,(long)__gen_e_acsl_x_arg);
+ __gmpz_init(__gen_e_acsl_add_3);
+ __gmpz_add(__gen_e_acsl_add_3,
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_x_3),
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_y_3));
+ __gmpz_init_set(__retres_arg,
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_add_3));
+ __gmpz_clear(__gen_e_acsl_y_3);
+ __gmpz_clear(__gen_e_acsl_x_3);
+ __gmpz_clear(__gen_e_acsl_add_3);
+ return;
+}
+
+long __gen_e_acsl_f1(int __gen_e_acsl_x_arg, int __gen_e_acsl_y_arg)
+{
+ long __retres;
+ __retres = __gen_e_acsl_x_arg + (long)__gen_e_acsl_y_arg;
+ return __retres;
+}
+
+int __gen_e_acsl_p2_3(int __gen_e_acsl_x_arg, long __gen_e_acsl_y_arg)
+{
+ int __retres;
+ __e_acsl_mpz_t __gen_e_acsl_x_2;
+ __e_acsl_mpz_t __gen_e_acsl_y_2;
+ __e_acsl_mpz_t __gen_e_acsl_add_2;
+ __e_acsl_mpz_t __gen_e_acsl__3;
+ int __gen_e_acsl_gt_2;
+ __gmpz_init_set_si(__gen_e_acsl_x_2,(long)__gen_e_acsl_x_arg);
+ __gmpz_init_set_si(__gen_e_acsl_y_2,__gen_e_acsl_y_arg);
+ __gmpz_init(__gen_e_acsl_add_2);
+ __gmpz_add(__gen_e_acsl_add_2,
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_x_2),
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_y_2));
+ __gmpz_init_set_si(__gen_e_acsl__3,0L);
+ __gen_e_acsl_gt_2 = __gmpz_cmp((__e_acsl_mpz_struct const *)(__gen_e_acsl_add_2),
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl__3));
+ __retres = __gen_e_acsl_gt_2 > 0;
+ __gmpz_clear(__gen_e_acsl_x_2);
+ __gmpz_clear(__gen_e_acsl_y_2);
+ __gmpz_clear(__gen_e_acsl_add_2);
+ __gmpz_clear(__gen_e_acsl__3);
+ return __retres;
+}
+
+int __gen_e_acsl_p2(int __gen_e_acsl_x_arg, int __gen_e_acsl_y_arg)
+{
+ int __retres;
+ __retres = __gen_e_acsl_x_arg + (long)__gen_e_acsl_y_arg > 0L;
+ return __retres;
+}
+
+int __gen_e_acsl_p2_2(int __gen_e_acsl_x_arg,
+ __e_acsl_mpz_struct * __gen_e_acsl_y_arg)
+{
+ int __retres;
+ __e_acsl_mpz_t __gen_e_acsl_y;
+ __e_acsl_mpz_t __gen_e_acsl_x;
+ __e_acsl_mpz_t __gen_e_acsl_add;
+ __e_acsl_mpz_t __gen_e_acsl__2;
+ int __gen_e_acsl_gt;
+ __gmpz_init_set(__gen_e_acsl_y,
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_y_arg));
+ __gmpz_init_set_si(__gen_e_acsl_x,(long)__gen_e_acsl_x_arg);
+ __gmpz_init(__gen_e_acsl_add);
+ __gmpz_add(__gen_e_acsl_add,(__e_acsl_mpz_struct const *)(__gen_e_acsl_x),
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_y));
+ __gmpz_init_set_si(__gen_e_acsl__2,0L);
+ __gen_e_acsl_gt = __gmpz_cmp((__e_acsl_mpz_struct const *)(__gen_e_acsl_add),
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl__2));
+ __retres = __gen_e_acsl_gt > 0;
+ __gmpz_clear(__gen_e_acsl_y);
+ __gmpz_clear(__gen_e_acsl_x);
+ __gmpz_clear(__gen_e_acsl_add);
+ __gmpz_clear(__gen_e_acsl__2);
+ return __retres;
+}
+
+int __gen_e_acsl_p1(int __gen_e_acsl_x_arg, int __gen_e_acsl_y_arg)
+{
+ int __retres;
+ __retres = __gen_e_acsl_x_arg + (long)__gen_e_acsl_y_arg > 0L;
+ return __retres;
+}
+
+
diff --git a/src/plugins/e-acsl/tests/gmp/oracle/gen_functions2.c b/src/plugins/e-acsl/tests/gmp/oracle/gen_functions2.c
new file mode 100644
index 00000000000..890ef4bf2c6
--- /dev/null
+++ b/src/plugins/e-acsl/tests/gmp/oracle/gen_functions2.c
@@ -0,0 +1,513 @@
+/* Generated by Frama-C */
+#include "stdio.h"
+#include "stdlib.h"
+struct mystruct {
+ int k ;
+ int l ;
+};
+typedef struct mystruct mystruct;
+/*@ predicate p1(int x, int y) = x + y > 0;
+ */
+int __gen_e_acsl_p1(int __gen_e_acsl_x_arg, int __gen_e_acsl_y_arg);
+
+/*@ predicate p2(ℤ x, ℤ y) = x + y > 0;
+
+*/
+int __gen_e_acsl_p2_2(int __gen_e_acsl_x_arg,
+ __e_acsl_mpz_struct * __gen_e_acsl_y_arg);
+
+int __gen_e_acsl_p2(int __gen_e_acsl_x_arg, int __gen_e_acsl_y_arg);
+
+/*@ logic ℤ f1(ℤ x, ℤ y) = x + y;
+
+*/
+void __gen_e_acsl_f1_2(__e_acsl_mpz_struct * __retres_arg,
+ int __gen_e_acsl_x_arg,
+ __e_acsl_mpz_struct * __gen_e_acsl_y_arg);
+
+void __gen_e_acsl_f1(__e_acsl_mpz_struct * __retres_arg,
+ int __gen_e_acsl_x_arg, int __gen_e_acsl_y_arg);
+
+void __gen_e_acsl_f1_3(__e_acsl_mpz_struct * __retres_arg,
+ __e_acsl_mpz_struct * __gen_e_acsl_x_arg,
+ __e_acsl_mpz_struct * __gen_e_acsl_y_arg);
+
+/*@ logic char h_char(char c) = c;
+ */
+char __gen_e_acsl_h_char(int __gen_e_acsl_c_arg);
+
+/*@ logic short h_short(short s) = s;
+ */
+short __gen_e_acsl_h_short(int __gen_e_acsl_s_arg);
+
+/*@ logic int g_hidden(int x) = x;
+ */
+int __gen_e_acsl_g_hidden(int __gen_e_acsl_x_arg);
+
+/*@ logic int g(int x) = g_hidden(x);
+ */
+int __gen_e_acsl_g(int __gen_e_acsl_x_arg);
+
+/*@ logic mystruct t1(mystruct m) = m;
+ */
+mystruct __gen_e_acsl_t1(mystruct __gen_e_acsl_m_arg);
+
+/*@ logic ℤ t2(mystruct m) = m.k + m.l;
+
+*/
+void __gen_e_acsl_t2(__e_acsl_mpz_struct * __retres_arg,
+ mystruct __gen_e_acsl_m_arg);
+
+/*@ predicate k_pred(ℤ x) = x > 0;
+
+*/
+int __gen_e_acsl_k_pred(int __gen_e_acsl_x_arg);
+
+/*@ requires k_pred(x); */
+void __gen_e_acsl_k(int x);
+
+void k(int x)
+{
+ return;
+}
+
+int glob = 5;
+/*@ predicate never_called(int x) = x ≡ x;
+ */
+/*@ logic double f2(double x) = (double)(1 / x);
+ */
+double __gen_e_acsl_f2(double __gen_e_acsl_x_arg);
+
+/*@ predicate p_notyet{L}(ℤ x) = x > 0;
+ */
+/*@ logic ℤ f_notyet{L}(ℤ x) = x;
+
+*/
+int main(void)
+{
+ int __retres;
+ mystruct m;
+ __e_acsl_memory_init((int *)0,(char ***)0,(size_t)8);
+ int x = 1;
+ int y = 2;
+ /*@ assert p1(x, y); */
+ {
+ int __gen_e_acsl_p1_tapp;
+ __gen_e_acsl_p1_tapp = __gen_e_acsl_p1(x,y);
+ __e_acsl_assert(__gen_e_acsl_p1_tapp,(char *)"Assertion",(char *)"main",
+ (char *)"p1(x, y)",42);
+ }
+ /*@ assert p2(3, 4); */
+ {
+ int __gen_e_acsl_p2_tapp;
+ __gen_e_acsl_p2_tapp = __gen_e_acsl_p2(3,4);
+ __e_acsl_assert(__gen_e_acsl_p2_tapp,(char *)"Assertion",(char *)"main",
+ (char *)"p2(3, 4)",43);
+ }
+ /*@ assert p2(5, 99999999999999999999999999999); */
+ {
+ __e_acsl_mpz_t __gen_e_acsl__3;
+ int __gen_e_acsl_p2_tapp_2;
+ __gmpz_init_set_str(__gen_e_acsl__3,"99999999999999999999999999999",10);
+ __gen_e_acsl_p2_tapp_2 = __gen_e_acsl_p2_2(5,
+ (__e_acsl_mpz_struct *)__gen_e_acsl__3);
+ __e_acsl_assert(__gen_e_acsl_p2_tapp_2,(char *)"Assertion",
+ (char *)"main",
+ (char *)"p2(5, 99999999999999999999999999999)",44);
+ __gmpz_clear(__gen_e_acsl__3);
+ }
+ /*@ assert f1(x, y) ≡ 3; */
+ {
+ __e_acsl_mpz_t __gen_e_acsl_f1_tapp;
+ __e_acsl_mpz_t __gen_e_acsl__5;
+ int __gen_e_acsl_eq;
+ __gmpz_init(__gen_e_acsl_f1_tapp);
+ /*@ assert
+ Eva: initialization:
+ \initialized((__e_acsl_mpz_struct *)__gen_e_acsl_f1_tapp);
+ */
+ __gen_e_acsl_f1((__e_acsl_mpz_struct *)__gen_e_acsl_f1_tapp,x,y);
+ __gmpz_init_set_si(__gen_e_acsl__5,3L);
+ __gen_e_acsl_eq = __gmpz_cmp((__e_acsl_mpz_struct const *)(__gen_e_acsl_f1_tapp),
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl__5));
+ __e_acsl_assert(__gen_e_acsl_eq == 0,(char *)"Assertion",(char *)"main",
+ (char *)"f1(x, y) == 3",46);
+ __gmpz_clear(__gen_e_acsl_f1_tapp);
+ __gmpz_clear(__gen_e_acsl__5);
+ }
+ /*@ assert p2(x, f1(3, 4)); */
+ {
+ __e_acsl_mpz_t __gen_e_acsl_f1_tapp_2;
+ int __gen_e_acsl_p2_tapp_3;
+ __gmpz_init(__gen_e_acsl_f1_tapp_2);
+ __gen_e_acsl_f1((__e_acsl_mpz_struct *)__gen_e_acsl_f1_tapp_2,3,4);
+ __gen_e_acsl_p2_tapp_3 = __gen_e_acsl_p2_2(x,
+ (__e_acsl_mpz_struct *)__gen_e_acsl_f1_tapp_2);
+ __e_acsl_assert(__gen_e_acsl_p2_tapp_3,(char *)"Assertion",
+ (char *)"main",(char *)"p2(x, f1(3, 4))",47);
+ __gmpz_clear(__gen_e_acsl_f1_tapp_2);
+ }
+ /*@ assert f1(9, 99999999999999999999999999999) > 0; */
+ {
+ __e_acsl_mpz_t __gen_e_acsl__6;
+ __e_acsl_mpz_t __gen_e_acsl_f1_tapp_3;
+ __e_acsl_mpz_t __gen_e_acsl__7;
+ int __gen_e_acsl_gt_4;
+ __gmpz_init_set_str(__gen_e_acsl__6,"99999999999999999999999999999",10);
+ __gmpz_init(__gen_e_acsl_f1_tapp_3);
+ __gen_e_acsl_f1_2((__e_acsl_mpz_struct *)__gen_e_acsl_f1_tapp_3,9,
+ (__e_acsl_mpz_struct *)__gen_e_acsl__6);
+ __gmpz_init_set_si(__gen_e_acsl__7,0L);
+ __gen_e_acsl_gt_4 = __gmpz_cmp((__e_acsl_mpz_struct const *)(__gen_e_acsl_f1_tapp_3),
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl__7));
+ __e_acsl_assert(__gen_e_acsl_gt_4 > 0,(char *)"Assertion",(char *)"main",
+ (char *)"f1(9, 99999999999999999999999999999) > 0",48);
+ __gmpz_clear(__gen_e_acsl__6);
+ __gmpz_clear(__gen_e_acsl_f1_tapp_3);
+ __gmpz_clear(__gen_e_acsl__7);
+ }
+ /*@ assert
+ f1(99999999999999999999999999999, 99999999999999999999999999999) ≡
+ 199999999999999999999999999998;
+ */
+ {
+ __e_acsl_mpz_t __gen_e_acsl__8;
+ __e_acsl_mpz_t __gen_e_acsl_f1_tapp_4;
+ __e_acsl_mpz_t __gen_e_acsl__9;
+ int __gen_e_acsl_eq_2;
+ __gmpz_init_set_str(__gen_e_acsl__8,"99999999999999999999999999999",10);
+ __gmpz_init(__gen_e_acsl_f1_tapp_4);
+ __gen_e_acsl_f1_3((__e_acsl_mpz_struct *)__gen_e_acsl_f1_tapp_4,
+ (__e_acsl_mpz_struct *)__gen_e_acsl__8,
+ (__e_acsl_mpz_struct *)__gen_e_acsl__8);
+ __gmpz_init_set_str(__gen_e_acsl__9,"199999999999999999999999999998",10);
+ __gen_e_acsl_eq_2 = __gmpz_cmp((__e_acsl_mpz_struct const *)(__gen_e_acsl_f1_tapp_4),
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl__9));
+ __e_acsl_assert(__gen_e_acsl_eq_2 == 0,(char *)"Assertion",
+ (char *)"main",
+ (char *)"f1(99999999999999999999999999999, 99999999999999999999999999999) ==\n199999999999999999999999999998",
+ 49);
+ __gmpz_clear(__gen_e_acsl__8);
+ __gmpz_clear(__gen_e_acsl_f1_tapp_4);
+ __gmpz_clear(__gen_e_acsl__9);
+ }
+ /*@ assert g(x) ≡ x; */
+ {
+ int __gen_e_acsl_g_tapp;
+ __e_acsl_mpz_t __gen_e_acsl_app;
+ __e_acsl_mpz_t __gen_e_acsl_x_7;
+ int __gen_e_acsl_eq_3;
+ __gen_e_acsl_g_tapp = __gen_e_acsl_g(x);
+ __gmpz_init_set_si(__gen_e_acsl_app,(long)__gen_e_acsl_g_tapp);
+ __gmpz_init_set_si(__gen_e_acsl_x_7,(long)x);
+ __gen_e_acsl_eq_3 = __gmpz_cmp((__e_acsl_mpz_struct const *)(__gen_e_acsl_app),
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_x_7));
+ __e_acsl_assert(__gen_e_acsl_eq_3 == 0,(char *)"Assertion",
+ (char *)"main",(char *)"g(x) == x",53);
+ __gmpz_clear(__gen_e_acsl_app);
+ __gmpz_clear(__gen_e_acsl_x_7);
+ }
+ char c = (char)'c';
+ /*@ assert h_char(c) ≡ c; */
+ {
+ char __gen_e_acsl_h_char_tapp;
+ __e_acsl_mpz_t __gen_e_acsl_app_2;
+ __e_acsl_mpz_t __gen_e_acsl_c;
+ int __gen_e_acsl_eq_4;
+ __gen_e_acsl_h_char_tapp = __gen_e_acsl_h_char((int)c);
+ __gmpz_init_set_si(__gen_e_acsl_app_2,(long)__gen_e_acsl_h_char_tapp);
+ __gmpz_init_set_si(__gen_e_acsl_c,(long)c);
+ __gen_e_acsl_eq_4 = __gmpz_cmp((__e_acsl_mpz_struct const *)(__gen_e_acsl_app_2),
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_c));
+ __e_acsl_assert(__gen_e_acsl_eq_4 == 0,(char *)"Assertion",
+ (char *)"main",(char *)"h_char(c) == c",56);
+ __gmpz_clear(__gen_e_acsl_app_2);
+ __gmpz_clear(__gen_e_acsl_c);
+ }
+ short s = (short)1;
+ /*@ assert h_short(s) ≡ s; */
+ {
+ short __gen_e_acsl_h_short_tapp;
+ __e_acsl_mpz_t __gen_e_acsl_app_3;
+ __e_acsl_mpz_t __gen_e_acsl_s;
+ int __gen_e_acsl_eq_5;
+ __gen_e_acsl_h_short_tapp = __gen_e_acsl_h_short((int)s);
+ __gmpz_init_set_si(__gen_e_acsl_app_3,(long)__gen_e_acsl_h_short_tapp);
+ __gmpz_init_set_si(__gen_e_acsl_s,(long)s);
+ __gen_e_acsl_eq_5 = __gmpz_cmp((__e_acsl_mpz_struct const *)(__gen_e_acsl_app_3),
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_s));
+ __e_acsl_assert(__gen_e_acsl_eq_5 == 0,(char *)"Assertion",
+ (char *)"main",(char *)"h_short(s) == s",58);
+ __gmpz_clear(__gen_e_acsl_app_3);
+ __gmpz_clear(__gen_e_acsl_s);
+ }
+ m.k = 8;
+ m.l = 9;
+ /*@ assert t2(t1(m)) ≡ 17; */
+ {
+ mystruct __gen_e_acsl_t1_tapp;
+ __e_acsl_mpz_t __gen_e_acsl_t2_tapp;
+ __e_acsl_mpz_t __gen_e_acsl__12;
+ int __gen_e_acsl_eq_6;
+ __gen_e_acsl_t1_tapp = __gen_e_acsl_t1(m);
+ __gmpz_init(__gen_e_acsl_t2_tapp);
+ __gen_e_acsl_t2((__e_acsl_mpz_struct *)__gen_e_acsl_t2_tapp,
+ __gen_e_acsl_t1_tapp);
+ __gmpz_init_set_si(__gen_e_acsl__12,17L);
+ __gen_e_acsl_eq_6 = __gmpz_cmp((__e_acsl_mpz_struct const *)(__gen_e_acsl_t2_tapp),
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl__12));
+ __e_acsl_assert(__gen_e_acsl_eq_6 == 0,(char *)"Assertion",
+ (char *)"main",(char *)"t2(t1(m)) == 17",63);
+ __gmpz_clear(__gen_e_acsl_t2_tapp);
+ __gmpz_clear(__gen_e_acsl__12);
+ }
+ __gen_e_acsl_k(9);
+ double d = 2.0;
+ /*@ assert f2(d) > 0; */
+ {
+ double __gen_e_acsl_f2_tapp;
+ __gen_e_acsl_f2_tapp = __gen_e_acsl_f2(d);
+ __e_acsl_assert(__gen_e_acsl_f2_tapp > (double)0,(char *)"Assertion",
+ (char *)"main",(char *)"f2(d) > 0",68);
+ }
+ /*@ assert p_notyet(27); */ ;
+ /*@ assert f_notyet(27) ≡ 27; */ ;
+ __retres = 0;
+ return __retres;
+}
+
+/*@ requires k_pred(x); */
+void __gen_e_acsl_k(int x)
+{
+ {
+ int __gen_e_acsl_k_pred_tapp;
+ __gen_e_acsl_k_pred_tapp = __gen_e_acsl_k_pred(x);
+ __e_acsl_assert(__gen_e_acsl_k_pred_tapp,(char *)"Precondition",
+ (char *)"k",(char *)"k_pred(x)",25);
+ }
+ k(x);
+ return;
+}
+
+double __gen_e_acsl_f2(double __gen_e_acsl_x_arg)
+{
+ double __retres;
+ __retres = (double)((long double)1 / __gen_e_acsl_x_arg);
+ return __retres;
+}
+
+int __gen_e_acsl_k_pred(int __gen_e_acsl_x_arg)
+{
+ int __retres;
+ __e_acsl_mpz_t __gen_e_acsl_x;
+ __e_acsl_mpz_t __gen_e_acsl_;
+ int __gen_e_acsl_gt;
+ __gmpz_init_set_si(__gen_e_acsl_x,(long)__gen_e_acsl_x_arg);
+ __gmpz_init_set_si(__gen_e_acsl_,0L);
+ __gen_e_acsl_gt = __gmpz_cmp((__e_acsl_mpz_struct const *)(__gen_e_acsl_x),
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_));
+ __retres = __gen_e_acsl_gt > 0;
+ __gmpz_clear(__gen_e_acsl_x);
+ __gmpz_clear(__gen_e_acsl_);
+ return __retres;
+}
+
+void __gen_e_acsl_t2(__e_acsl_mpz_struct * __retres_arg,
+ mystruct __gen_e_acsl_m_arg)
+{
+ __e_acsl_mpz_t __gen_e_acsl__10;
+ __e_acsl_mpz_t __gen_e_acsl__11;
+ __e_acsl_mpz_t __gen_e_acsl_add_7;
+ __gmpz_init_set_si(__gen_e_acsl__10,(long)__gen_e_acsl_m_arg.k);
+ __gmpz_init_set_si(__gen_e_acsl__11,(long)__gen_e_acsl_m_arg.l);
+ __gmpz_init(__gen_e_acsl_add_7);
+ __gmpz_add(__gen_e_acsl_add_7,
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl__10),
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl__11));
+ __gmpz_init_set(__retres_arg,
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_add_7));
+ __gmpz_clear(__gen_e_acsl__10);
+ __gmpz_clear(__gen_e_acsl__11);
+ __gmpz_clear(__gen_e_acsl_add_7);
+ return;
+}
+
+mystruct __gen_e_acsl_t1(mystruct __gen_e_acsl_m_arg)
+{
+ mystruct __retres;
+ __retres = __gen_e_acsl_m_arg;
+ return __retres;
+}
+
+int __gen_e_acsl_g(int __gen_e_acsl_x_arg)
+{
+ int __retres;
+ int __gen_e_acsl_g_hidden_tapp;
+ __gen_e_acsl_g_hidden_tapp = __gen_e_acsl_g_hidden(__gen_e_acsl_x_arg);
+ __retres = __gen_e_acsl_g_hidden_tapp;
+ return __retres;
+}
+
+int __gen_e_acsl_g_hidden(int __gen_e_acsl_x_arg)
+{
+ int __retres;
+ __retres = __gen_e_acsl_x_arg;
+ return __retres;
+}
+
+short __gen_e_acsl_h_short(int __gen_e_acsl_s_arg)
+{
+ int __retres;
+ __retres = (short)__gen_e_acsl_s_arg;
+ return __retres;
+}
+
+char __gen_e_acsl_h_char(int __gen_e_acsl_c_arg)
+{
+ int __retres;
+ __retres = (char)__gen_e_acsl_c_arg;
+ return __retres;
+}
+
+void __gen_e_acsl_f1_3(__e_acsl_mpz_struct * __retres_arg,
+ __e_acsl_mpz_struct * __gen_e_acsl_x_arg,
+ __e_acsl_mpz_struct * __gen_e_acsl_y_arg)
+{
+ __e_acsl_mpz_t __gen_e_acsl_x_6;
+ __e_acsl_mpz_t __gen_e_acsl_y_6;
+ __e_acsl_mpz_t __gen_e_acsl_add_6;
+ __gmpz_init_set(__gen_e_acsl_x_6,
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_x_arg));
+ __gmpz_init_set(__gen_e_acsl_y_6,
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_y_arg));
+ __gmpz_init(__gen_e_acsl_add_6);
+ __gmpz_add(__gen_e_acsl_add_6,
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_x_6),
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_y_6));
+ __gmpz_init_set(__retres_arg,
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_add_6));
+ __gmpz_clear(__gen_e_acsl_x_6);
+ __gmpz_clear(__gen_e_acsl_y_6);
+ __gmpz_clear(__gen_e_acsl_add_6);
+ return;
+}
+
+void __gen_e_acsl_f1(__e_acsl_mpz_struct * __retres_arg,
+ int __gen_e_acsl_x_arg, int __gen_e_acsl_y_arg)
+{
+ __e_acsl_mpz_t __gen_e_acsl_x_4;
+ __e_acsl_mpz_t __gen_e_acsl_y_4;
+ __e_acsl_mpz_t __gen_e_acsl_add_4;
+ __gmpz_init_set_si(__gen_e_acsl_x_4,(long)__gen_e_acsl_x_arg);
+ __gmpz_init_set_si(__gen_e_acsl_y_4,(long)__gen_e_acsl_y_arg);
+ __gmpz_init(__gen_e_acsl_add_4);
+ __gmpz_add(__gen_e_acsl_add_4,
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_x_4),
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_y_4));
+ __gmpz_init_set(__retres_arg,
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_add_4));
+ __gmpz_clear(__gen_e_acsl_x_4);
+ __gmpz_clear(__gen_e_acsl_y_4);
+ __gmpz_clear(__gen_e_acsl_add_4);
+ return;
+}
+
+void __gen_e_acsl_f1_2(__e_acsl_mpz_struct * __retres_arg,
+ int __gen_e_acsl_x_arg,
+ __e_acsl_mpz_struct * __gen_e_acsl_y_arg)
+{
+ __e_acsl_mpz_t __gen_e_acsl_y_5;
+ __e_acsl_mpz_t __gen_e_acsl_x_5;
+ __e_acsl_mpz_t __gen_e_acsl_add_5;
+ __gmpz_init_set(__gen_e_acsl_y_5,
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_y_arg));
+ __gmpz_init_set_si(__gen_e_acsl_x_5,(long)__gen_e_acsl_x_arg);
+ __gmpz_init(__gen_e_acsl_add_5);
+ __gmpz_add(__gen_e_acsl_add_5,
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_x_5),
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_y_5));
+ __gmpz_init_set(__retres_arg,
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_add_5));
+ __gmpz_clear(__gen_e_acsl_y_5);
+ __gmpz_clear(__gen_e_acsl_x_5);
+ __gmpz_clear(__gen_e_acsl_add_5);
+ return;
+}
+
+int __gen_e_acsl_p2(int __gen_e_acsl_x_arg, int __gen_e_acsl_y_arg)
+{
+ int __retres;
+ __e_acsl_mpz_t __gen_e_acsl_x_2;
+ __e_acsl_mpz_t __gen_e_acsl_y_2;
+ __e_acsl_mpz_t __gen_e_acsl_add_2;
+ __e_acsl_mpz_t __gen_e_acsl__2;
+ int __gen_e_acsl_gt_2;
+ __gmpz_init_set_si(__gen_e_acsl_x_2,(long)__gen_e_acsl_x_arg);
+ __gmpz_init_set_si(__gen_e_acsl_y_2,(long)__gen_e_acsl_y_arg);
+ __gmpz_init(__gen_e_acsl_add_2);
+ __gmpz_add(__gen_e_acsl_add_2,
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_x_2),
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_y_2));
+ __gmpz_init_set_si(__gen_e_acsl__2,0L);
+ __gen_e_acsl_gt_2 = __gmpz_cmp((__e_acsl_mpz_struct const *)(__gen_e_acsl_add_2),
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl__2));
+ __retres = __gen_e_acsl_gt_2 > 0;
+ __gmpz_clear(__gen_e_acsl_x_2);
+ __gmpz_clear(__gen_e_acsl_y_2);
+ __gmpz_clear(__gen_e_acsl_add_2);
+ __gmpz_clear(__gen_e_acsl__2);
+ return __retres;
+}
+
+int __gen_e_acsl_p2_2(int __gen_e_acsl_x_arg,
+ __e_acsl_mpz_struct * __gen_e_acsl_y_arg)
+{
+ int __retres;
+ __e_acsl_mpz_t __gen_e_acsl_y_3;
+ __e_acsl_mpz_t __gen_e_acsl_x_3;
+ __e_acsl_mpz_t __gen_e_acsl_add_3;
+ __e_acsl_mpz_t __gen_e_acsl__4;
+ int __gen_e_acsl_gt_3;
+ __gmpz_init_set(__gen_e_acsl_y_3,
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_y_arg));
+ __gmpz_init_set_si(__gen_e_acsl_x_3,(long)__gen_e_acsl_x_arg);
+ __gmpz_init(__gen_e_acsl_add_3);
+ __gmpz_add(__gen_e_acsl_add_3,
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_x_3),
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_y_3));
+ __gmpz_init_set_si(__gen_e_acsl__4,0L);
+ __gen_e_acsl_gt_3 = __gmpz_cmp((__e_acsl_mpz_struct const *)(__gen_e_acsl_add_3),
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl__4));
+ __retres = __gen_e_acsl_gt_3 > 0;
+ __gmpz_clear(__gen_e_acsl_y_3);
+ __gmpz_clear(__gen_e_acsl_x_3);
+ __gmpz_clear(__gen_e_acsl_add_3);
+ __gmpz_clear(__gen_e_acsl__4);
+ return __retres;
+}
+
+int __gen_e_acsl_p1(int __gen_e_acsl_x_arg, int __gen_e_acsl_y_arg)
+{
+ int __retres;
+ __e_acsl_mpz_t __gen_e_acsl_x;
+ __e_acsl_mpz_t __gen_e_acsl_y;
+ __e_acsl_mpz_t __gen_e_acsl_add;
+ __e_acsl_mpz_t __gen_e_acsl_;
+ int __gen_e_acsl_gt;
+ __gmpz_init_set_si(__gen_e_acsl_x,(long)__gen_e_acsl_x_arg);
+ __gmpz_init_set_si(__gen_e_acsl_y,(long)__gen_e_acsl_y_arg);
+ __gmpz_init(__gen_e_acsl_add);
+ __gmpz_add(__gen_e_acsl_add,(__e_acsl_mpz_struct const *)(__gen_e_acsl_x),
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_y));
+ __gmpz_init_set_si(__gen_e_acsl_,0L);
+ __gen_e_acsl_gt = __gmpz_cmp((__e_acsl_mpz_struct const *)(__gen_e_acsl_add),
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_));
+ __retres = __gen_e_acsl_gt > 0;
+ __gmpz_clear(__gen_e_acsl_x);
+ __gmpz_clear(__gen_e_acsl_y);
+ __gmpz_clear(__gen_e_acsl_add);
+ __gmpz_clear(__gen_e_acsl_);
+ return __retres;
+}
+
+
diff --git a/src/plugins/e-acsl/tests/gmp/oracle/gen_functions_contiki.c b/src/plugins/e-acsl/tests/gmp/oracle/gen_functions_contiki.c
new file mode 100644
index 00000000000..259afb2e7cf
--- /dev/null
+++ b/src/plugins/e-acsl/tests/gmp/oracle/gen_functions_contiki.c
@@ -0,0 +1,45 @@
+/* Generated by Frama-C */
+#include "stdio.h"
+#include "stdlib.h"
+struct list {
+ struct list *next ;
+ int value ;
+};
+/*@
+logic ℤ length_aux{L}(struct list *l, ℤ n) =
+ \at(n < 0? -1:
+ (l ≡ (struct list *)((void *)0)? n:
+ (n < 2147483647? length_aux(l->next, n + 1): -1)),
+ L);
+ */
+/*@ logic ℤ length{L}(struct list *l) = \at(length_aux(l, 0),L);
+
+*/
+int main(void)
+{
+ int __retres;
+ struct list node1;
+ struct list node2;
+ struct list node3;
+ __e_acsl_memory_init((int *)0,(char ***)0,(size_t)8);
+ __e_acsl_store_block((void *)(& node3),(size_t)16);
+ __e_acsl_store_block((void *)(& node2),(size_t)16);
+ __e_acsl_store_block((void *)(& node1),(size_t)16);
+ __e_acsl_initialize((void *)(& node1.next),sizeof(struct list *));
+ node1.next = & node2;
+ __e_acsl_initialize((void *)(& node2.next),sizeof(struct list *));
+ node2.next = & node3;
+ struct list *l = & node1;
+ __e_acsl_store_block((void *)(& l),(size_t)8);
+ __e_acsl_full_init((void *)(& l));
+ /*@ assert length(l) ≡ 3; */ ;
+ __retres = 0;
+ __e_acsl_delete_block((void *)(& l));
+ __e_acsl_delete_block((void *)(& node3));
+ __e_acsl_delete_block((void *)(& node2));
+ __e_acsl_delete_block((void *)(& node1));
+ __e_acsl_memory_clean();
+ return __retres;
+}
+
+
diff --git a/src/plugins/e-acsl/tests/gmp/oracle/gen_functions_contiki2.c b/src/plugins/e-acsl/tests/gmp/oracle/gen_functions_contiki2.c
new file mode 100644
index 00000000000..259afb2e7cf
--- /dev/null
+++ b/src/plugins/e-acsl/tests/gmp/oracle/gen_functions_contiki2.c
@@ -0,0 +1,45 @@
+/* Generated by Frama-C */
+#include "stdio.h"
+#include "stdlib.h"
+struct list {
+ struct list *next ;
+ int value ;
+};
+/*@
+logic ℤ length_aux{L}(struct list *l, ℤ n) =
+ \at(n < 0? -1:
+ (l ≡ (struct list *)((void *)0)? n:
+ (n < 2147483647? length_aux(l->next, n + 1): -1)),
+ L);
+ */
+/*@ logic ℤ length{L}(struct list *l) = \at(length_aux(l, 0),L);
+
+*/
+int main(void)
+{
+ int __retres;
+ struct list node1;
+ struct list node2;
+ struct list node3;
+ __e_acsl_memory_init((int *)0,(char ***)0,(size_t)8);
+ __e_acsl_store_block((void *)(& node3),(size_t)16);
+ __e_acsl_store_block((void *)(& node2),(size_t)16);
+ __e_acsl_store_block((void *)(& node1),(size_t)16);
+ __e_acsl_initialize((void *)(& node1.next),sizeof(struct list *));
+ node1.next = & node2;
+ __e_acsl_initialize((void *)(& node2.next),sizeof(struct list *));
+ node2.next = & node3;
+ struct list *l = & node1;
+ __e_acsl_store_block((void *)(& l),(size_t)8);
+ __e_acsl_full_init((void *)(& l));
+ /*@ assert length(l) ≡ 3; */ ;
+ __retres = 0;
+ __e_acsl_delete_block((void *)(& l));
+ __e_acsl_delete_block((void *)(& node3));
+ __e_acsl_delete_block((void *)(& node2));
+ __e_acsl_delete_block((void *)(& node1));
+ __e_acsl_memory_clean();
+ return __retres;
+}
+
+
diff --git a/src/plugins/e-acsl/tests/gmp/oracle/gen_functions_rec.c b/src/plugins/e-acsl/tests/gmp/oracle/gen_functions_rec.c
new file mode 100644
index 00000000000..c747ce87540
--- /dev/null
+++ b/src/plugins/e-acsl/tests/gmp/oracle/gen_functions_rec.c
@@ -0,0 +1,623 @@
+/* Generated by Frama-C */
+#include "stdio.h"
+#include "stdlib.h"
+/*@ logic ℤ f1(ℤ n) = n ≤ 0? 0: f1(n - 1) + n;
+
+*/
+void __gen_e_acsl_f1(__e_acsl_mpz_struct * __retres_arg,
+ int __gen_e_acsl_n_arg);
+
+void __gen_e_acsl_f1_2(__e_acsl_mpz_struct * __retres_arg,
+ long __gen_e_acsl_n_arg);
+
+void __gen_e_acsl_f1_3(__e_acsl_mpz_struct * __retres_arg,
+ __e_acsl_mpz_struct * __gen_e_acsl_n_arg);
+
+/*@ logic ℤ f2(ℤ n) = n < 0? 1: (f2(n - 1) * f2(n - 2)) / f2(n - 3);
+
+*/
+int __gen_e_acsl_f2(int __gen_e_acsl_n_arg);
+
+int __gen_e_acsl_f2_2(long __gen_e_acsl_n_arg);
+
+int __gen_e_acsl_f2_3(__e_acsl_mpz_struct * __gen_e_acsl_n_arg);
+
+/*@ logic ℤ g(ℤ n) = 0;
+
+*/
+int __gen_e_acsl_g(int __gen_e_acsl_n_arg);
+
+int __gen_e_acsl_g_2(long __gen_e_acsl_n_arg);
+
+int __gen_e_acsl_g_3(__e_acsl_mpz_struct * __gen_e_acsl_n_arg);
+
+/*@ logic ℤ f3(ℤ n) = n > 0? g(n) * f3(n - 1) - 5: g(n + 1);
+
+*/
+int __gen_e_acsl_f3(int __gen_e_acsl_n_arg);
+
+int __gen_e_acsl_f3_2(long __gen_e_acsl_n_arg);
+
+int __gen_e_acsl_f3_3(__e_acsl_mpz_struct * __gen_e_acsl_n_arg);
+
+/*@
+logic ℤ f4(ℤ n) =
+ n < 100? f4(n + 1): (n < 0x7fffffffffffffffL? 0x7fffffffffffffffL: 6);
+
+*/
+long __gen_e_acsl_f4_3(__e_acsl_mpz_struct * __gen_e_acsl_n_arg);
+
+long __gen_e_acsl_f4(int __gen_e_acsl_n_arg);
+
+long __gen_e_acsl_f4_2(long __gen_e_acsl_n_arg);
+
+int main(void)
+{
+ int __retres;
+ __e_acsl_memory_init((int *)0,(char ***)0,(size_t)8);
+ /*@ assert f1(0) ≡ 0; */
+ {
+ __e_acsl_mpz_t __gen_e_acsl_f1_tapp;
+ __e_acsl_mpz_t __gen_e_acsl__7;
+ int __gen_e_acsl_eq;
+ __gmpz_init(__gen_e_acsl_f1_tapp);
+ /*@ assert
+ Eva: initialization:
+ \initialized((__e_acsl_mpz_struct *)__gen_e_acsl_f1_tapp);
+ */
+ __gen_e_acsl_f1((__e_acsl_mpz_struct *)__gen_e_acsl_f1_tapp,0);
+ __gmpz_init_set_si(__gen_e_acsl__7,0L);
+ __gen_e_acsl_eq = __gmpz_cmp((__e_acsl_mpz_struct const *)(__gen_e_acsl_f1_tapp),
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl__7));
+ __e_acsl_assert(__gen_e_acsl_eq == 0,(char *)"Assertion",(char *)"main",
+ (char *)"f1(0) == 0",21);
+ __gmpz_clear(__gen_e_acsl_f1_tapp);
+ __gmpz_clear(__gen_e_acsl__7);
+ }
+ /*@ assert f1(1) ≡ 1; */
+ {
+ __e_acsl_mpz_t __gen_e_acsl_f1_tapp_5;
+ __e_acsl_mpz_t __gen_e_acsl__8;
+ int __gen_e_acsl_eq_2;
+ __gmpz_init(__gen_e_acsl_f1_tapp_5);
+ __gen_e_acsl_f1((__e_acsl_mpz_struct *)__gen_e_acsl_f1_tapp_5,1);
+ __gmpz_init_set_si(__gen_e_acsl__8,1L);
+ __gen_e_acsl_eq_2 = __gmpz_cmp((__e_acsl_mpz_struct const *)(__gen_e_acsl_f1_tapp_5),
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl__8));
+ __e_acsl_assert(__gen_e_acsl_eq_2 == 0,(char *)"Assertion",
+ (char *)"main",(char *)"f1(1) == 1",22);
+ __gmpz_clear(__gen_e_acsl_f1_tapp_5);
+ __gmpz_clear(__gen_e_acsl__8);
+ }
+ /*@ assert f1(100) ≡ 5050; */
+ {
+ __e_acsl_mpz_t __gen_e_acsl_f1_tapp_6;
+ __e_acsl_mpz_t __gen_e_acsl__9;
+ int __gen_e_acsl_eq_3;
+ __gmpz_init(__gen_e_acsl_f1_tapp_6);
+ __gen_e_acsl_f1((__e_acsl_mpz_struct *)__gen_e_acsl_f1_tapp_6,100);
+ __gmpz_init_set_si(__gen_e_acsl__9,5050L);
+ __gen_e_acsl_eq_3 = __gmpz_cmp((__e_acsl_mpz_struct const *)(__gen_e_acsl_f1_tapp_6),
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl__9));
+ __e_acsl_assert(__gen_e_acsl_eq_3 == 0,(char *)"Assertion",
+ (char *)"main",(char *)"f1(100) == 5050",23);
+ __gmpz_clear(__gen_e_acsl_f1_tapp_6);
+ __gmpz_clear(__gen_e_acsl__9);
+ }
+ /*@ assert f2(7) ≡ 1; */
+ {
+ int __gen_e_acsl_f2_tapp;
+ __gen_e_acsl_f2_tapp = __gen_e_acsl_f2(7);
+ __e_acsl_assert(__gen_e_acsl_f2_tapp == 1,(char *)"Assertion",
+ (char *)"main",(char *)"f2(7) == 1",25);
+ }
+ /*@ assert f3(6) ≡ -5; */
+ {
+ int __gen_e_acsl_f3_tapp;
+ __gen_e_acsl_f3_tapp = __gen_e_acsl_f3(6);
+ __e_acsl_assert(__gen_e_acsl_f3_tapp == -5,(char *)"Assertion",
+ (char *)"main",(char *)"f3(6) == -5",27);
+ }
+ /*@ assert f4(9) > 0; */
+ {
+ long __gen_e_acsl_f4_tapp;
+ __gen_e_acsl_f4_tapp = __gen_e_acsl_f4(9);
+ __e_acsl_assert(__gen_e_acsl_f4_tapp > 0L,(char *)"Assertion",
+ (char *)"main",(char *)"f4(9) > 0",29);
+ }
+ __retres = 0;
+ return __retres;
+}
+
+long __gen_e_acsl_f4_2(long __gen_e_acsl_n_arg)
+{
+ long __retres;
+ long __gen_e_acsl_if_13;
+ if (__gen_e_acsl_n_arg < 100L) {
+ __e_acsl_mpz_t __gen_e_acsl_n_10;
+ __e_acsl_mpz_t __gen_e_acsl__22;
+ __e_acsl_mpz_t __gen_e_acsl_add_6;
+ long __gen_e_acsl_f4_tapp_3;
+ __gmpz_init_set_si(__gen_e_acsl_n_10,__gen_e_acsl_n_arg);
+ __gmpz_init_set_si(__gen_e_acsl__22,1L);
+ __gmpz_init(__gen_e_acsl_add_6);
+ __gmpz_add(__gen_e_acsl_add_6,
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_n_10),
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl__22));
+ __gen_e_acsl_f4_tapp_3 = __gen_e_acsl_f4_3((__e_acsl_mpz_struct *)__gen_e_acsl_add_6);
+ __gen_e_acsl_if_13 = __gen_e_acsl_f4_tapp_3;
+ __gmpz_clear(__gen_e_acsl_n_10);
+ __gmpz_clear(__gen_e_acsl__22);
+ __gmpz_clear(__gen_e_acsl_add_6);
+ }
+ else {
+ unsigned long __gen_e_acsl_if_12;
+ if (__gen_e_acsl_n_arg < 9223372036854775807L) __gen_e_acsl_if_12 = 9223372036854775807UL;
+ else __gen_e_acsl_if_12 = 6UL;
+ __gen_e_acsl_if_13 = (long)__gen_e_acsl_if_12;
+ }
+ __retres = __gen_e_acsl_if_13;
+ return __retres;
+}
+
+long __gen_e_acsl_f4(int __gen_e_acsl_n_arg)
+{
+ long __retres;
+ long __gen_e_acsl_if_15;
+ if (__gen_e_acsl_n_arg < 100) {
+ long __gen_e_acsl_f4_tapp_2;
+ __gen_e_acsl_f4_tapp_2 = __gen_e_acsl_f4_2(__gen_e_acsl_n_arg + 1L);
+ __gen_e_acsl_if_15 = __gen_e_acsl_f4_tapp_2;
+ }
+ else {
+ unsigned long __gen_e_acsl_if_14;
+ if ((long)__gen_e_acsl_n_arg < 9223372036854775807L) __gen_e_acsl_if_14 = 9223372036854775807UL;
+ else __gen_e_acsl_if_14 = 6UL;
+ __gen_e_acsl_if_15 = (long)__gen_e_acsl_if_14;
+ }
+ __retres = __gen_e_acsl_if_15;
+ return __retres;
+}
+
+long __gen_e_acsl_f4_3(__e_acsl_mpz_struct * __gen_e_acsl_n_arg)
+{
+ long __retres;
+ __e_acsl_mpz_t __gen_e_acsl_n_11;
+ __e_acsl_mpz_t __gen_e_acsl__23;
+ int __gen_e_acsl_lt_2;
+ long __gen_e_acsl_if_11;
+ __gmpz_init_set(__gen_e_acsl_n_11,
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_n_arg));
+ __gmpz_init_set_si(__gen_e_acsl__23,100L);
+ __gen_e_acsl_lt_2 = __gmpz_cmp((__e_acsl_mpz_struct const *)(__gen_e_acsl_n_11),
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl__23));
+ if (__gen_e_acsl_lt_2 < 0) {
+ __e_acsl_mpz_t __gen_e_acsl__24;
+ __e_acsl_mpz_t __gen_e_acsl_add_7;
+ long __gen_e_acsl_f4_tapp_4;
+ __gmpz_init_set_si(__gen_e_acsl__24,1L);
+ __gmpz_init(__gen_e_acsl_add_7);
+ __gmpz_add(__gen_e_acsl_add_7,
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_n_11),
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl__24));
+ __gen_e_acsl_f4_tapp_4 = __gen_e_acsl_f4_3((__e_acsl_mpz_struct *)__gen_e_acsl_add_7);
+ __gen_e_acsl_if_11 = __gen_e_acsl_f4_tapp_4;
+ __gmpz_clear(__gen_e_acsl__24);
+ __gmpz_clear(__gen_e_acsl_add_7);
+ }
+ else {
+ __e_acsl_mpz_t __gen_e_acsl__25;
+ int __gen_e_acsl_lt_3;
+ unsigned long __gen_e_acsl_if_10;
+ __gmpz_init_set_ui(__gen_e_acsl__25,9223372036854775807UL);
+ __gen_e_acsl_lt_3 = __gmpz_cmp((__e_acsl_mpz_struct const *)(__gen_e_acsl_n_11),
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl__25));
+ if (__gen_e_acsl_lt_3 < 0) __gen_e_acsl_if_10 = 9223372036854775807UL;
+ else __gen_e_acsl_if_10 = 6UL;
+ __gen_e_acsl_if_11 = (long)__gen_e_acsl_if_10;
+ __gmpz_clear(__gen_e_acsl__25);
+ }
+ __retres = __gen_e_acsl_if_11;
+ __gmpz_clear(__gen_e_acsl_n_11);
+ __gmpz_clear(__gen_e_acsl__23);
+ return __retres;
+}
+
+int __gen_e_acsl_f3_3(__e_acsl_mpz_struct * __gen_e_acsl_n_arg)
+{
+ int __retres;
+ __e_acsl_mpz_t __gen_e_acsl_n_7;
+ __e_acsl_mpz_t __gen_e_acsl__18;
+ int __gen_e_acsl_gt;
+ int __gen_e_acsl_if_7;
+ __gmpz_init_set(__gen_e_acsl_n_7,
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_n_arg));
+ __gmpz_init_set_si(__gen_e_acsl__18,0L);
+ __gen_e_acsl_gt = __gmpz_cmp((__e_acsl_mpz_struct const *)(__gen_e_acsl_n_7),
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl__18));
+ if (__gen_e_acsl_gt > 0) {
+ int __gen_e_acsl_g_tapp_3;
+ __e_acsl_mpz_t __gen_e_acsl__19;
+ __e_acsl_mpz_t __gen_e_acsl_sub_10;
+ int __gen_e_acsl_f3_tapp_4;
+ __gen_e_acsl_g_tapp_3 = __gen_e_acsl_g_3((__e_acsl_mpz_struct *)__gen_e_acsl_n_7);
+ __gmpz_init_set_si(__gen_e_acsl__19,1L);
+ __gmpz_init(__gen_e_acsl_sub_10);
+ __gmpz_sub(__gen_e_acsl_sub_10,
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_n_7),
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl__19));
+ __gen_e_acsl_f3_tapp_4 = __gen_e_acsl_f3_3((__e_acsl_mpz_struct *)__gen_e_acsl_sub_10);
+ __gen_e_acsl_if_7 = __gen_e_acsl_g_tapp_3 * __gen_e_acsl_f3_tapp_4 - 5;
+ __gmpz_clear(__gen_e_acsl__19);
+ __gmpz_clear(__gen_e_acsl_sub_10);
+ }
+ else {
+ __e_acsl_mpz_t __gen_e_acsl__20;
+ __e_acsl_mpz_t __gen_e_acsl_add_4;
+ int __gen_e_acsl_g_tapp_4;
+ __gmpz_init_set_si(__gen_e_acsl__20,1L);
+ __gmpz_init(__gen_e_acsl_add_4);
+ __gmpz_add(__gen_e_acsl_add_4,
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_n_7),
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl__20));
+ __gen_e_acsl_g_tapp_4 = __gen_e_acsl_g_3((__e_acsl_mpz_struct *)__gen_e_acsl_add_4);
+ __gen_e_acsl_if_7 = __gen_e_acsl_g_tapp_4;
+ __gmpz_clear(__gen_e_acsl__20);
+ __gmpz_clear(__gen_e_acsl_add_4);
+ }
+ __retres = __gen_e_acsl_if_7;
+ __gmpz_clear(__gen_e_acsl_n_7);
+ __gmpz_clear(__gen_e_acsl__18);
+ return __retres;
+}
+
+int __gen_e_acsl_f3_2(long __gen_e_acsl_n_arg)
+{
+ int __retres;
+ int __gen_e_acsl_if_8;
+ if (__gen_e_acsl_n_arg > 0L) {
+ int __gen_e_acsl_g_tapp_2;
+ __e_acsl_mpz_t __gen_e_acsl_n_6;
+ __e_acsl_mpz_t __gen_e_acsl__17;
+ __e_acsl_mpz_t __gen_e_acsl_sub_9;
+ int __gen_e_acsl_f3_tapp_3;
+ __gen_e_acsl_g_tapp_2 = __gen_e_acsl_g_2(__gen_e_acsl_n_arg);
+ __gmpz_init_set_si(__gen_e_acsl_n_6,__gen_e_acsl_n_arg);
+ __gmpz_init_set_si(__gen_e_acsl__17,1L);
+ __gmpz_init(__gen_e_acsl_sub_9);
+ __gmpz_sub(__gen_e_acsl_sub_9,
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_n_6),
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl__17));
+ __gen_e_acsl_f3_tapp_3 = __gen_e_acsl_f3_3((__e_acsl_mpz_struct *)__gen_e_acsl_sub_9);
+ __gen_e_acsl_if_8 = __gen_e_acsl_g_tapp_2 * __gen_e_acsl_f3_tapp_3 - 5;
+ __gmpz_clear(__gen_e_acsl_n_6);
+ __gmpz_clear(__gen_e_acsl__17);
+ __gmpz_clear(__gen_e_acsl_sub_9);
+ }
+ else {
+ __e_acsl_mpz_t __gen_e_acsl_n_9;
+ __e_acsl_mpz_t __gen_e_acsl__21;
+ __e_acsl_mpz_t __gen_e_acsl_add_5;
+ int __gen_e_acsl_g_tapp_5;
+ __gmpz_init_set_si(__gen_e_acsl_n_9,__gen_e_acsl_n_arg);
+ __gmpz_init_set_si(__gen_e_acsl__21,1L);
+ __gmpz_init(__gen_e_acsl_add_5);
+ __gmpz_add(__gen_e_acsl_add_5,
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_n_9),
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl__21));
+ __gen_e_acsl_g_tapp_5 = __gen_e_acsl_g_3((__e_acsl_mpz_struct *)__gen_e_acsl_add_5);
+ __gen_e_acsl_if_8 = __gen_e_acsl_g_tapp_5;
+ __gmpz_clear(__gen_e_acsl_n_9);
+ __gmpz_clear(__gen_e_acsl__21);
+ __gmpz_clear(__gen_e_acsl_add_5);
+ }
+ __retres = __gen_e_acsl_if_8;
+ return __retres;
+}
+
+int __gen_e_acsl_f3(int __gen_e_acsl_n_arg)
+{
+ int __retres;
+ int __gen_e_acsl_if_9;
+ if (__gen_e_acsl_n_arg > 0) {
+ int __gen_e_acsl_g_tapp;
+ int __gen_e_acsl_f3_tapp_2;
+ __gen_e_acsl_g_tapp = __gen_e_acsl_g(__gen_e_acsl_n_arg);
+ __gen_e_acsl_f3_tapp_2 = __gen_e_acsl_f3_2(__gen_e_acsl_n_arg - 1L);
+ __gen_e_acsl_if_9 = __gen_e_acsl_g_tapp * __gen_e_acsl_f3_tapp_2 - 5;
+ }
+ else {
+ int __gen_e_acsl_g_tapp_6;
+ __gen_e_acsl_g_tapp_6 = __gen_e_acsl_g_2(__gen_e_acsl_n_arg + 1L);
+ __gen_e_acsl_if_9 = __gen_e_acsl_g_tapp_6;
+ }
+ __retres = __gen_e_acsl_if_9;
+ return __retres;
+}
+
+int __gen_e_acsl_g_3(__e_acsl_mpz_struct * __gen_e_acsl_n_arg)
+{
+ int __retres;
+ __e_acsl_mpz_t __gen_e_acsl_n_8;
+ __gmpz_init_set(__gen_e_acsl_n_8,
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_n_arg));
+ __retres = 0;
+ __gmpz_clear(__gen_e_acsl_n_8);
+ return __retres;
+}
+
+int __gen_e_acsl_g_2(long __gen_e_acsl_n_arg)
+{
+ int __retres;
+ __retres = 0;
+ return __retres;
+}
+
+int __gen_e_acsl_g(int __gen_e_acsl_n_arg)
+{
+ int __retres;
+ __retres = 0;
+ return __retres;
+}
+
+int __gen_e_acsl_f2_3(__e_acsl_mpz_struct * __gen_e_acsl_n_arg)
+{
+ int __retres;
+ __e_acsl_mpz_t __gen_e_acsl_n_5;
+ __e_acsl_mpz_t __gen_e_acsl__11;
+ int __gen_e_acsl_lt;
+ int __gen_e_acsl_if_4;
+ __gmpz_init_set(__gen_e_acsl_n_5,
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_n_arg));
+ __gmpz_init_set_si(__gen_e_acsl__11,0L);
+ __gen_e_acsl_lt = __gmpz_cmp((__e_acsl_mpz_struct const *)(__gen_e_acsl_n_5),
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl__11));
+ if (__gen_e_acsl_lt < 0) __gen_e_acsl_if_4 = 1;
+ else {
+ __e_acsl_mpz_t __gen_e_acsl__12;
+ __e_acsl_mpz_t __gen_e_acsl_sub_4;
+ int __gen_e_acsl_f2_tapp_4;
+ __e_acsl_mpz_t __gen_e_acsl__13;
+ __e_acsl_mpz_t __gen_e_acsl_sub_5;
+ int __gen_e_acsl_f2_tapp_5;
+ __e_acsl_mpz_t __gen_e_acsl__14;
+ __e_acsl_mpz_t __gen_e_acsl_sub_6;
+ int __gen_e_acsl_f2_tapp_6;
+ __gmpz_init_set_si(__gen_e_acsl__12,1L);
+ __gmpz_init(__gen_e_acsl_sub_4);
+ __gmpz_sub(__gen_e_acsl_sub_4,
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_n_5),
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl__12));
+ __gen_e_acsl_f2_tapp_4 = __gen_e_acsl_f2_3((__e_acsl_mpz_struct *)__gen_e_acsl_sub_4);
+ __gmpz_init_set_si(__gen_e_acsl__13,2L);
+ __gmpz_init(__gen_e_acsl_sub_5);
+ __gmpz_sub(__gen_e_acsl_sub_5,
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_n_5),
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl__13));
+ __gen_e_acsl_f2_tapp_5 = __gen_e_acsl_f2_3((__e_acsl_mpz_struct *)__gen_e_acsl_sub_5);
+ __gmpz_init_set_si(__gen_e_acsl__14,3L);
+ __gmpz_init(__gen_e_acsl_sub_6);
+ __gmpz_sub(__gen_e_acsl_sub_6,
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_n_5),
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl__14));
+ __gen_e_acsl_f2_tapp_6 = __gen_e_acsl_f2_3((__e_acsl_mpz_struct *)__gen_e_acsl_sub_6);
+ __e_acsl_assert(__gen_e_acsl_f2_tapp_6 != 0,(char *)"RTE",(char *)"f2_3",
+ (char *)"division_by_zero: __gen_e_acsl_f2_tapp_6 != 0",
+ 9);
+ __gen_e_acsl_if_4 = (__gen_e_acsl_f2_tapp_4 * __gen_e_acsl_f2_tapp_5) / __gen_e_acsl_f2_tapp_6;
+ __gmpz_clear(__gen_e_acsl__12);
+ __gmpz_clear(__gen_e_acsl_sub_4);
+ __gmpz_clear(__gen_e_acsl__13);
+ __gmpz_clear(__gen_e_acsl_sub_5);
+ __gmpz_clear(__gen_e_acsl__14);
+ __gmpz_clear(__gen_e_acsl_sub_6);
+ }
+ __retres = __gen_e_acsl_if_4;
+ __gmpz_clear(__gen_e_acsl_n_5);
+ __gmpz_clear(__gen_e_acsl__11);
+ return __retres;
+}
+
+int __gen_e_acsl_f2_2(long __gen_e_acsl_n_arg)
+{
+ int __retres;
+ int __gen_e_acsl_if_5;
+ if (__gen_e_acsl_n_arg < 0L) __gen_e_acsl_if_5 = 1;
+ else {
+ __e_acsl_mpz_t __gen_e_acsl_n_4;
+ __e_acsl_mpz_t __gen_e_acsl__10;
+ __e_acsl_mpz_t __gen_e_acsl_sub_3;
+ int __gen_e_acsl_f2_tapp_3;
+ __e_acsl_mpz_t __gen_e_acsl__15;
+ __e_acsl_mpz_t __gen_e_acsl_sub_7;
+ int __gen_e_acsl_f2_tapp_7;
+ __e_acsl_mpz_t __gen_e_acsl__16;
+ __e_acsl_mpz_t __gen_e_acsl_sub_8;
+ int __gen_e_acsl_f2_tapp_8;
+ __gmpz_init_set_si(__gen_e_acsl_n_4,__gen_e_acsl_n_arg);
+ __gmpz_init_set_si(__gen_e_acsl__10,1L);
+ __gmpz_init(__gen_e_acsl_sub_3);
+ __gmpz_sub(__gen_e_acsl_sub_3,
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_n_4),
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl__10));
+ __gen_e_acsl_f2_tapp_3 = __gen_e_acsl_f2_3((__e_acsl_mpz_struct *)__gen_e_acsl_sub_3);
+ __gmpz_init_set_si(__gen_e_acsl__15,2L);
+ __gmpz_init(__gen_e_acsl_sub_7);
+ __gmpz_sub(__gen_e_acsl_sub_7,
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_n_4),
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl__15));
+ __gen_e_acsl_f2_tapp_7 = __gen_e_acsl_f2_3((__e_acsl_mpz_struct *)__gen_e_acsl_sub_7);
+ __gmpz_init_set_si(__gen_e_acsl__16,3L);
+ __gmpz_init(__gen_e_acsl_sub_8);
+ __gmpz_sub(__gen_e_acsl_sub_8,
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_n_4),
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl__16));
+ __gen_e_acsl_f2_tapp_8 = __gen_e_acsl_f2_3((__e_acsl_mpz_struct *)__gen_e_acsl_sub_8);
+ __e_acsl_assert(__gen_e_acsl_f2_tapp_8 != 0,(char *)"RTE",(char *)"f2_2",
+ (char *)"division_by_zero: __gen_e_acsl_f2_tapp_8 != 0",
+ 9);
+ __gen_e_acsl_if_5 = (__gen_e_acsl_f2_tapp_3 * __gen_e_acsl_f2_tapp_7) / __gen_e_acsl_f2_tapp_8;
+ __gmpz_clear(__gen_e_acsl_n_4);
+ __gmpz_clear(__gen_e_acsl__10);
+ __gmpz_clear(__gen_e_acsl_sub_3);
+ __gmpz_clear(__gen_e_acsl__15);
+ __gmpz_clear(__gen_e_acsl_sub_7);
+ __gmpz_clear(__gen_e_acsl__16);
+ __gmpz_clear(__gen_e_acsl_sub_8);
+ }
+ __retres = __gen_e_acsl_if_5;
+ return __retres;
+}
+
+int __gen_e_acsl_f2(int __gen_e_acsl_n_arg)
+{
+ int __retres;
+ int __gen_e_acsl_if_6;
+ if (__gen_e_acsl_n_arg < 0) __gen_e_acsl_if_6 = 1;
+ else {
+ int __gen_e_acsl_f2_tapp_2;
+ int __gen_e_acsl_f2_tapp_9;
+ int __gen_e_acsl_f2_tapp_10;
+ __gen_e_acsl_f2_tapp_2 = __gen_e_acsl_f2_2(__gen_e_acsl_n_arg - 1L);
+ __gen_e_acsl_f2_tapp_9 = __gen_e_acsl_f2_2(__gen_e_acsl_n_arg - 2L);
+ __gen_e_acsl_f2_tapp_10 = __gen_e_acsl_f2_2(__gen_e_acsl_n_arg - 3L);
+ __e_acsl_assert(__gen_e_acsl_f2_tapp_10 != 0,(char *)"RTE",(char *)"f2",
+ (char *)"division_by_zero: __gen_e_acsl_f2_tapp_10 != 0",
+ 9);
+ __gen_e_acsl_if_6 = (__gen_e_acsl_f2_tapp_2 * __gen_e_acsl_f2_tapp_9) / __gen_e_acsl_f2_tapp_10;
+ }
+ __retres = __gen_e_acsl_if_6;
+ return __retres;
+}
+
+void __gen_e_acsl_f1_3(__e_acsl_mpz_struct * __retres_arg,
+ __e_acsl_mpz_struct * __gen_e_acsl_n_arg)
+{
+ __e_acsl_mpz_t __gen_e_acsl_n_2;
+ __e_acsl_mpz_t __gen_e_acsl__4;
+ int __gen_e_acsl_le;
+ __e_acsl_mpz_t __gen_e_acsl_if;
+ __gmpz_init_set(__gen_e_acsl_n_2,
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_n_arg));
+ __gmpz_init_set_si(__gen_e_acsl__4,0L);
+ __gen_e_acsl_le = __gmpz_cmp((__e_acsl_mpz_struct const *)(__gen_e_acsl_n_2),
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl__4));
+ if (__gen_e_acsl_le <= 0) {
+ __e_acsl_mpz_t __gen_e_acsl__5;
+ __gmpz_init_set_si(__gen_e_acsl__5,0L);
+ __gmpz_init_set(__gen_e_acsl_if,
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl__5));
+ __gmpz_clear(__gen_e_acsl__5);
+ }
+ else {
+ __e_acsl_mpz_t __gen_e_acsl__6;
+ __e_acsl_mpz_t __gen_e_acsl_sub_2;
+ __e_acsl_mpz_t __gen_e_acsl_f1_tapp_4;
+ __e_acsl_mpz_t __gen_e_acsl_add;
+ __gmpz_init_set_si(__gen_e_acsl__6,1L);
+ __gmpz_init(__gen_e_acsl_sub_2);
+ __gmpz_sub(__gen_e_acsl_sub_2,
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_n_2),
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl__6));
+ __gmpz_init(__gen_e_acsl_f1_tapp_4);
+ __gen_e_acsl_f1_3((__e_acsl_mpz_struct *)__gen_e_acsl_f1_tapp_4,
+ (__e_acsl_mpz_struct *)__gen_e_acsl_sub_2);
+ __gmpz_init(__gen_e_acsl_add);
+ __gmpz_add(__gen_e_acsl_add,
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_f1_tapp_4),
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_n_2));
+ __gmpz_init_set(__gen_e_acsl_if,
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_add));
+ __gmpz_clear(__gen_e_acsl__6);
+ __gmpz_clear(__gen_e_acsl_sub_2);
+ __gmpz_clear(__gen_e_acsl_f1_tapp_4);
+ __gmpz_clear(__gen_e_acsl_add);
+ }
+ __gmpz_init_set(__retres_arg,
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_if));
+ __gmpz_clear(__gen_e_acsl_n_2);
+ __gmpz_clear(__gen_e_acsl__4);
+ __gmpz_clear(__gen_e_acsl_if);
+ return;
+}
+
+void __gen_e_acsl_f1_2(__e_acsl_mpz_struct * __retres_arg,
+ long __gen_e_acsl_n_arg)
+{
+ __e_acsl_mpz_t __gen_e_acsl_if_2;
+ if (__gen_e_acsl_n_arg <= 0L) {
+ __e_acsl_mpz_t __gen_e_acsl__2;
+ __gmpz_init_set_si(__gen_e_acsl__2,0L);
+ __gmpz_init_set(__gen_e_acsl_if_2,
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl__2));
+ __gmpz_clear(__gen_e_acsl__2);
+ }
+ else {
+ __e_acsl_mpz_t __gen_e_acsl_n;
+ __e_acsl_mpz_t __gen_e_acsl__3;
+ __e_acsl_mpz_t __gen_e_acsl_sub;
+ __e_acsl_mpz_t __gen_e_acsl_f1_tapp_3;
+ __e_acsl_mpz_t __gen_e_acsl_add_2;
+ __gmpz_init_set_si(__gen_e_acsl_n,__gen_e_acsl_n_arg);
+ __gmpz_init_set_si(__gen_e_acsl__3,1L);
+ __gmpz_init(__gen_e_acsl_sub);
+ __gmpz_sub(__gen_e_acsl_sub,
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_n),
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl__3));
+ __gmpz_init(__gen_e_acsl_f1_tapp_3);
+ __gen_e_acsl_f1_3((__e_acsl_mpz_struct *)__gen_e_acsl_f1_tapp_3,
+ (__e_acsl_mpz_struct *)__gen_e_acsl_sub);
+ __gmpz_init(__gen_e_acsl_add_2);
+ __gmpz_add(__gen_e_acsl_add_2,
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_f1_tapp_3),
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_n));
+ __gmpz_init_set(__gen_e_acsl_if_2,
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_add_2));
+ __gmpz_clear(__gen_e_acsl_n);
+ __gmpz_clear(__gen_e_acsl__3);
+ __gmpz_clear(__gen_e_acsl_sub);
+ __gmpz_clear(__gen_e_acsl_f1_tapp_3);
+ __gmpz_clear(__gen_e_acsl_add_2);
+ }
+ __gmpz_init_set(__retres_arg,
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_if_2));
+ __gmpz_clear(__gen_e_acsl_if_2);
+ return;
+}
+
+void __gen_e_acsl_f1(__e_acsl_mpz_struct * __retres_arg,
+ int __gen_e_acsl_n_arg)
+{
+ __e_acsl_mpz_t __gen_e_acsl_if_3;
+ if (__gen_e_acsl_n_arg <= 0) {
+ __e_acsl_mpz_t __gen_e_acsl_;
+ __gmpz_init_set_si(__gen_e_acsl_,0L);
+ __gmpz_init_set(__gen_e_acsl_if_3,
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_));
+ __gmpz_clear(__gen_e_acsl_);
+ }
+ else {
+ __e_acsl_mpz_t __gen_e_acsl_f1_tapp_2;
+ __e_acsl_mpz_t __gen_e_acsl_n_3;
+ __e_acsl_mpz_t __gen_e_acsl_add_3;
+ __gmpz_init(__gen_e_acsl_f1_tapp_2);
+ __gen_e_acsl_f1_2((__e_acsl_mpz_struct *)__gen_e_acsl_f1_tapp_2,
+ __gen_e_acsl_n_arg - 1L);
+ __gmpz_init_set_si(__gen_e_acsl_n_3,(long)__gen_e_acsl_n_arg);
+ __gmpz_init(__gen_e_acsl_add_3);
+ __gmpz_add(__gen_e_acsl_add_3,
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_f1_tapp_2),
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_n_3));
+ __gmpz_init_set(__gen_e_acsl_if_3,
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_add_3));
+ __gmpz_clear(__gen_e_acsl_f1_tapp_2);
+ __gmpz_clear(__gen_e_acsl_n_3);
+ __gmpz_clear(__gen_e_acsl_add_3);
+ }
+ __gmpz_init_set(__retres_arg,
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_if_3));
+ __gmpz_clear(__gen_e_acsl_if_3);
+ return;
+}
+
+
diff --git a/src/plugins/e-acsl/tests/gmp/oracle/gen_functions_rec2.c b/src/plugins/e-acsl/tests/gmp/oracle/gen_functions_rec2.c
new file mode 100644
index 00000000000..35f5f695298
--- /dev/null
+++ b/src/plugins/e-acsl/tests/gmp/oracle/gen_functions_rec2.c
@@ -0,0 +1,782 @@
+/* Generated by Frama-C */
+#include "stdio.h"
+#include "stdlib.h"
+/*@ logic ℤ f1(ℤ n) = n ≤ 0? 0: f1(n - 1) + n;
+
+*/
+void __gen_e_acsl_f1(__e_acsl_mpz_struct * __retres_arg,
+ int __gen_e_acsl_n_arg);
+
+void __gen_e_acsl_f1_2(__e_acsl_mpz_struct * __retres_arg,
+ __e_acsl_mpz_struct * __gen_e_acsl_n_arg);
+
+/*@ logic ℤ f2(ℤ n) = n < 0? 1: (f2(n - 1) * f2(n - 2)) / f2(n - 3);
+
+*/
+void __gen_e_acsl_f2_2(__e_acsl_mpz_struct * __retres_arg,
+ __e_acsl_mpz_struct * __gen_e_acsl_n_arg);
+
+void __gen_e_acsl_f2(__e_acsl_mpz_struct * __retres_arg,
+ int __gen_e_acsl_n_arg);
+
+/*@ logic ℤ g(ℤ n) = 0;
+
+*/
+void __gen_e_acsl_g_2(__e_acsl_mpz_struct * __retres_arg,
+ __e_acsl_mpz_struct * __gen_e_acsl_n_arg);
+
+void __gen_e_acsl_g(__e_acsl_mpz_struct * __retres_arg,
+ int __gen_e_acsl_n_arg);
+
+/*@ logic ℤ f3(ℤ n) = n > 0? g(n) * f3(n - 1) - 5: g(n + 1);
+
+*/
+void __gen_e_acsl_f3(__e_acsl_mpz_struct * __retres_arg,
+ int __gen_e_acsl_n_arg);
+
+void __gen_e_acsl_f3_2(__e_acsl_mpz_struct * __retres_arg,
+ __e_acsl_mpz_struct * __gen_e_acsl_n_arg);
+
+/*@
+logic ℤ f4(ℤ n) =
+ n < 100? f4(n + 1): (n < 0x7fffffffffffffffL? 0x7fffffffffffffffL: 6);
+
+*/
+void __gen_e_acsl_f4(__e_acsl_mpz_struct * __retres_arg,
+ int __gen_e_acsl_n_arg);
+
+void __gen_e_acsl_f4_2(__e_acsl_mpz_struct * __retres_arg,
+ __e_acsl_mpz_struct * __gen_e_acsl_n_arg);
+
+int main(void)
+{
+ int __retres;
+ __e_acsl_memory_init((int *)0,(char ***)0,(size_t)8);
+ /*@ assert f1(0) ≡ 0; */
+ {
+ __e_acsl_mpz_t __gen_e_acsl_f1_tapp;
+ __e_acsl_mpz_t __gen_e_acsl__7;
+ int __gen_e_acsl_eq;
+ __gmpz_init(__gen_e_acsl_f1_tapp);
+ /*@ assert
+ Eva: initialization:
+ \initialized((__e_acsl_mpz_struct *)__gen_e_acsl_f1_tapp);
+ */
+ __gen_e_acsl_f1((__e_acsl_mpz_struct *)__gen_e_acsl_f1_tapp,0);
+ __gmpz_init_set_si(__gen_e_acsl__7,0L);
+ __gen_e_acsl_eq = __gmpz_cmp((__e_acsl_mpz_struct const *)(__gen_e_acsl_f1_tapp),
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl__7));
+ __e_acsl_assert(__gen_e_acsl_eq == 0,(char *)"Assertion",(char *)"main",
+ (char *)"f1(0) == 0",21);
+ __gmpz_clear(__gen_e_acsl_f1_tapp);
+ __gmpz_clear(__gen_e_acsl__7);
+ }
+ /*@ assert f1(1) ≡ 1; */
+ {
+ __e_acsl_mpz_t __gen_e_acsl_f1_tapp_4;
+ __e_acsl_mpz_t __gen_e_acsl__8;
+ int __gen_e_acsl_eq_2;
+ __gmpz_init(__gen_e_acsl_f1_tapp_4);
+ __gen_e_acsl_f1((__e_acsl_mpz_struct *)__gen_e_acsl_f1_tapp_4,1);
+ __gmpz_init_set_si(__gen_e_acsl__8,1L);
+ __gen_e_acsl_eq_2 = __gmpz_cmp((__e_acsl_mpz_struct const *)(__gen_e_acsl_f1_tapp_4),
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl__8));
+ __e_acsl_assert(__gen_e_acsl_eq_2 == 0,(char *)"Assertion",
+ (char *)"main",(char *)"f1(1) == 1",22);
+ __gmpz_clear(__gen_e_acsl_f1_tapp_4);
+ __gmpz_clear(__gen_e_acsl__8);
+ }
+ /*@ assert f1(100) ≡ 5050; */
+ {
+ __e_acsl_mpz_t __gen_e_acsl_f1_tapp_5;
+ __e_acsl_mpz_t __gen_e_acsl__9;
+ int __gen_e_acsl_eq_3;
+ __gmpz_init(__gen_e_acsl_f1_tapp_5);
+ __gen_e_acsl_f1((__e_acsl_mpz_struct *)__gen_e_acsl_f1_tapp_5,100);
+ __gmpz_init_set_si(__gen_e_acsl__9,5050L);
+ __gen_e_acsl_eq_3 = __gmpz_cmp((__e_acsl_mpz_struct const *)(__gen_e_acsl_f1_tapp_5),
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl__9));
+ __e_acsl_assert(__gen_e_acsl_eq_3 == 0,(char *)"Assertion",
+ (char *)"main",(char *)"f1(100) == 5050",23);
+ __gmpz_clear(__gen_e_acsl_f1_tapp_5);
+ __gmpz_clear(__gen_e_acsl__9);
+ }
+ /*@ assert f2(7) ≡ 1; */
+ {
+ __e_acsl_mpz_t __gen_e_acsl_f2_tapp;
+ __e_acsl_mpz_t __gen_e_acsl__22;
+ int __gen_e_acsl_eq_4;
+ __gmpz_init(__gen_e_acsl_f2_tapp);
+ __gen_e_acsl_f2((__e_acsl_mpz_struct *)__gen_e_acsl_f2_tapp,7);
+ __gmpz_init_set_si(__gen_e_acsl__22,1L);
+ __gen_e_acsl_eq_4 = __gmpz_cmp((__e_acsl_mpz_struct const *)(__gen_e_acsl_f2_tapp),
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl__22));
+ __e_acsl_assert(__gen_e_acsl_eq_4 == 0,(char *)"Assertion",
+ (char *)"main",(char *)"f2(7) == 1",25);
+ __gmpz_clear(__gen_e_acsl_f2_tapp);
+ __gmpz_clear(__gen_e_acsl__22);
+ }
+ /*@ assert f3(6) ≡ -5; */
+ {
+ __e_acsl_mpz_t __gen_e_acsl_f3_tapp;
+ __e_acsl_mpz_t __gen_e_acsl__33;
+ __e_acsl_mpz_t __gen_e_acsl_neg;
+ int __gen_e_acsl_eq_5;
+ __gmpz_init(__gen_e_acsl_f3_tapp);
+ __gen_e_acsl_f3((__e_acsl_mpz_struct *)__gen_e_acsl_f3_tapp,6);
+ __gmpz_init_set_si(__gen_e_acsl__33,5L);
+ __gmpz_init(__gen_e_acsl_neg);
+ __gmpz_neg(__gen_e_acsl_neg,
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl__33));
+ __gen_e_acsl_eq_5 = __gmpz_cmp((__e_acsl_mpz_struct const *)(__gen_e_acsl_f3_tapp),
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_neg));
+ __e_acsl_assert(__gen_e_acsl_eq_5 == 0,(char *)"Assertion",
+ (char *)"main",(char *)"f3(6) == -5",27);
+ __gmpz_clear(__gen_e_acsl_f3_tapp);
+ __gmpz_clear(__gen_e_acsl__33);
+ __gmpz_clear(__gen_e_acsl_neg);
+ }
+ /*@ assert f4(9) > 0; */
+ {
+ __e_acsl_mpz_t __gen_e_acsl_f4_tapp;
+ __e_acsl_mpz_t __gen_e_acsl__44;
+ int __gen_e_acsl_gt_3;
+ __gmpz_init(__gen_e_acsl_f4_tapp);
+ __gen_e_acsl_f4((__e_acsl_mpz_struct *)__gen_e_acsl_f4_tapp,9);
+ __gmpz_init_set_si(__gen_e_acsl__44,0L);
+ __gen_e_acsl_gt_3 = __gmpz_cmp((__e_acsl_mpz_struct const *)(__gen_e_acsl_f4_tapp),
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl__44));
+ __e_acsl_assert(__gen_e_acsl_gt_3 > 0,(char *)"Assertion",(char *)"main",
+ (char *)"f4(9) > 0",29);
+ __gmpz_clear(__gen_e_acsl_f4_tapp);
+ __gmpz_clear(__gen_e_acsl__44);
+ }
+ __retres = 0;
+ return __retres;
+}
+
+void __gen_e_acsl_f4_2(__e_acsl_mpz_struct * __retres_arg,
+ __e_acsl_mpz_struct * __gen_e_acsl_n_arg)
+{
+ __e_acsl_mpz_t __gen_e_acsl_n_14;
+ __e_acsl_mpz_t __gen_e_acsl__36;
+ int __gen_e_acsl_lt_4;
+ __e_acsl_mpz_t __gen_e_acsl_if_8;
+ __gmpz_init_set(__gen_e_acsl_n_14,
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_n_arg));
+ __gmpz_init_set_si(__gen_e_acsl__36,100L);
+ __gen_e_acsl_lt_4 = __gmpz_cmp((__e_acsl_mpz_struct const *)(__gen_e_acsl_n_14),
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl__36));
+ if (__gen_e_acsl_lt_4 < 0) {
+ __e_acsl_mpz_t __gen_e_acsl__37;
+ __e_acsl_mpz_t __gen_e_acsl_add_6;
+ __e_acsl_mpz_t __gen_e_acsl_f4_tapp_3;
+ __gmpz_init_set_si(__gen_e_acsl__37,1L);
+ __gmpz_init(__gen_e_acsl_add_6);
+ __gmpz_add(__gen_e_acsl_add_6,
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_n_14),
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl__37));
+ __gmpz_init(__gen_e_acsl_f4_tapp_3);
+ __gen_e_acsl_f4_2((__e_acsl_mpz_struct *)__gen_e_acsl_f4_tapp_3,
+ (__e_acsl_mpz_struct *)__gen_e_acsl_add_6);
+ __gmpz_init_set(__gen_e_acsl_if_8,
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_f4_tapp_3));
+ __gmpz_clear(__gen_e_acsl__37);
+ __gmpz_clear(__gen_e_acsl_add_6);
+ __gmpz_clear(__gen_e_acsl_f4_tapp_3);
+ }
+ else {
+ __e_acsl_mpz_t __gen_e_acsl__38;
+ int __gen_e_acsl_lt_5;
+ __e_acsl_mpz_t __gen_e_acsl_if_7;
+ __gmpz_init_set_ui(__gen_e_acsl__38,9223372036854775807UL);
+ __gen_e_acsl_lt_5 = __gmpz_cmp((__e_acsl_mpz_struct const *)(__gen_e_acsl_n_14),
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl__38));
+ if (__gen_e_acsl_lt_5 < 0) {
+ __e_acsl_mpz_t __gen_e_acsl__39;
+ __gmpz_init_set_ui(__gen_e_acsl__39,9223372036854775807UL);
+ __gmpz_init_set(__gen_e_acsl_if_7,
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl__39));
+ __gmpz_clear(__gen_e_acsl__39);
+ }
+ else {
+ __e_acsl_mpz_t __gen_e_acsl__40;
+ __gmpz_init_set_si(__gen_e_acsl__40,6L);
+ __gmpz_init_set(__gen_e_acsl_if_7,
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl__40));
+ __gmpz_clear(__gen_e_acsl__40);
+ }
+ __gmpz_init_set(__gen_e_acsl_if_8,
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_if_7));
+ __gmpz_clear(__gen_e_acsl__38);
+ __gmpz_clear(__gen_e_acsl_if_7);
+ }
+ __gmpz_init_set(__retres_arg,
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_if_8));
+ __gmpz_clear(__gen_e_acsl_n_14);
+ __gmpz_clear(__gen_e_acsl__36);
+ __gmpz_clear(__gen_e_acsl_if_8);
+ return;
+}
+
+void __gen_e_acsl_f4(__e_acsl_mpz_struct * __retres_arg,
+ int __gen_e_acsl_n_arg)
+{
+ __e_acsl_mpz_t __gen_e_acsl_n_12;
+ __e_acsl_mpz_t __gen_e_acsl__34;
+ int __gen_e_acsl_lt_3;
+ __e_acsl_mpz_t __gen_e_acsl_if_10;
+ __gmpz_init_set_si(__gen_e_acsl_n_12,(long)__gen_e_acsl_n_arg);
+ __gmpz_init_set_si(__gen_e_acsl__34,100L);
+ __gen_e_acsl_lt_3 = __gmpz_cmp((__e_acsl_mpz_struct const *)(__gen_e_acsl_n_12),
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl__34));
+ if (__gen_e_acsl_lt_3 < 0) {
+ __e_acsl_mpz_t __gen_e_acsl_n_13;
+ __e_acsl_mpz_t __gen_e_acsl__35;
+ __e_acsl_mpz_t __gen_e_acsl_add_5;
+ __e_acsl_mpz_t __gen_e_acsl_f4_tapp_2;
+ __gmpz_init_set_si(__gen_e_acsl_n_13,(long)__gen_e_acsl_n_arg);
+ __gmpz_init_set_si(__gen_e_acsl__35,1L);
+ __gmpz_init(__gen_e_acsl_add_5);
+ __gmpz_add(__gen_e_acsl_add_5,
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_n_13),
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl__35));
+ __gmpz_init(__gen_e_acsl_f4_tapp_2);
+ __gen_e_acsl_f4_2((__e_acsl_mpz_struct *)__gen_e_acsl_f4_tapp_2,
+ (__e_acsl_mpz_struct *)__gen_e_acsl_add_5);
+ __gmpz_init_set(__gen_e_acsl_if_10,
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_f4_tapp_2));
+ __gmpz_clear(__gen_e_acsl_n_13);
+ __gmpz_clear(__gen_e_acsl__35);
+ __gmpz_clear(__gen_e_acsl_add_5);
+ __gmpz_clear(__gen_e_acsl_f4_tapp_2);
+ }
+ else {
+ __e_acsl_mpz_t __gen_e_acsl_n_15;
+ __e_acsl_mpz_t __gen_e_acsl__41;
+ int __gen_e_acsl_lt_6;
+ __e_acsl_mpz_t __gen_e_acsl_if_9;
+ __gmpz_init_set_si(__gen_e_acsl_n_15,(long)__gen_e_acsl_n_arg);
+ __gmpz_init_set_ui(__gen_e_acsl__41,9223372036854775807UL);
+ __gen_e_acsl_lt_6 = __gmpz_cmp((__e_acsl_mpz_struct const *)(__gen_e_acsl_n_15),
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl__41));
+ if (__gen_e_acsl_lt_6 < 0) {
+ __e_acsl_mpz_t __gen_e_acsl__42;
+ __gmpz_init_set_ui(__gen_e_acsl__42,9223372036854775807UL);
+ __gmpz_init_set(__gen_e_acsl_if_9,
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl__42));
+ __gmpz_clear(__gen_e_acsl__42);
+ }
+ else {
+ __e_acsl_mpz_t __gen_e_acsl__43;
+ __gmpz_init_set_si(__gen_e_acsl__43,6L);
+ __gmpz_init_set(__gen_e_acsl_if_9,
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl__43));
+ __gmpz_clear(__gen_e_acsl__43);
+ }
+ __gmpz_init_set(__gen_e_acsl_if_10,
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_if_9));
+ __gmpz_clear(__gen_e_acsl_n_15);
+ __gmpz_clear(__gen_e_acsl__41);
+ __gmpz_clear(__gen_e_acsl_if_9);
+ }
+ __gmpz_init_set(__retres_arg,
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_if_10));
+ __gmpz_clear(__gen_e_acsl_n_12);
+ __gmpz_clear(__gen_e_acsl__34);
+ __gmpz_clear(__gen_e_acsl_if_10);
+ return;
+}
+
+void __gen_e_acsl_f3_2(__e_acsl_mpz_struct * __retres_arg,
+ __e_acsl_mpz_struct * __gen_e_acsl_n_arg)
+{
+ __e_acsl_mpz_t __gen_e_acsl_n_9;
+ __e_acsl_mpz_t __gen_e_acsl__26;
+ int __gen_e_acsl_gt_2;
+ __e_acsl_mpz_t __gen_e_acsl_if_5;
+ __gmpz_init_set(__gen_e_acsl_n_9,
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_n_arg));
+ __gmpz_init_set_si(__gen_e_acsl__26,0L);
+ __gen_e_acsl_gt_2 = __gmpz_cmp((__e_acsl_mpz_struct const *)(__gen_e_acsl_n_9),
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl__26));
+ if (__gen_e_acsl_gt_2 > 0) {
+ __e_acsl_mpz_t __gen_e_acsl_g_tapp_2;
+ __e_acsl_mpz_t __gen_e_acsl__28;
+ __e_acsl_mpz_t __gen_e_acsl_sub_10;
+ __e_acsl_mpz_t __gen_e_acsl_f3_tapp_3;
+ __e_acsl_mpz_t __gen_e_acsl_mul_3;
+ __e_acsl_mpz_t __gen_e_acsl__29;
+ __e_acsl_mpz_t __gen_e_acsl_sub_11;
+ __gmpz_init(__gen_e_acsl_g_tapp_2);
+ __gen_e_acsl_g_2((__e_acsl_mpz_struct *)__gen_e_acsl_g_tapp_2,
+ (__e_acsl_mpz_struct *)__gen_e_acsl_n_9);
+ __gmpz_init_set_si(__gen_e_acsl__28,1L);
+ __gmpz_init(__gen_e_acsl_sub_10);
+ __gmpz_sub(__gen_e_acsl_sub_10,
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_n_9),
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl__28));
+ __gmpz_init(__gen_e_acsl_f3_tapp_3);
+ __gen_e_acsl_f3_2((__e_acsl_mpz_struct *)__gen_e_acsl_f3_tapp_3,
+ (__e_acsl_mpz_struct *)__gen_e_acsl_sub_10);
+ __gmpz_init(__gen_e_acsl_mul_3);
+ __gmpz_mul(__gen_e_acsl_mul_3,
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_g_tapp_2),
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_f3_tapp_3));
+ __gmpz_init_set_si(__gen_e_acsl__29,5L);
+ __gmpz_init(__gen_e_acsl_sub_11);
+ __gmpz_sub(__gen_e_acsl_sub_11,
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_mul_3),
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl__29));
+ __gmpz_init_set(__gen_e_acsl_if_5,
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_sub_11));
+ __gmpz_clear(__gen_e_acsl_g_tapp_2);
+ __gmpz_clear(__gen_e_acsl__28);
+ __gmpz_clear(__gen_e_acsl_sub_10);
+ __gmpz_clear(__gen_e_acsl_f3_tapp_3);
+ __gmpz_clear(__gen_e_acsl_mul_3);
+ __gmpz_clear(__gen_e_acsl__29);
+ __gmpz_clear(__gen_e_acsl_sub_11);
+ }
+ else {
+ __e_acsl_mpz_t __gen_e_acsl__30;
+ __e_acsl_mpz_t __gen_e_acsl_add_3;
+ __e_acsl_mpz_t __gen_e_acsl_g_tapp_3;
+ __gmpz_init_set_si(__gen_e_acsl__30,1L);
+ __gmpz_init(__gen_e_acsl_add_3);
+ __gmpz_add(__gen_e_acsl_add_3,
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_n_9),
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl__30));
+ __gmpz_init(__gen_e_acsl_g_tapp_3);
+ __gen_e_acsl_g_2((__e_acsl_mpz_struct *)__gen_e_acsl_g_tapp_3,
+ (__e_acsl_mpz_struct *)__gen_e_acsl_add_3);
+ __gmpz_init_set(__gen_e_acsl_if_5,
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_g_tapp_3));
+ __gmpz_clear(__gen_e_acsl__30);
+ __gmpz_clear(__gen_e_acsl_add_3);
+ __gmpz_clear(__gen_e_acsl_g_tapp_3);
+ }
+ __gmpz_init_set(__retres_arg,
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_if_5));
+ __gmpz_clear(__gen_e_acsl_n_9);
+ __gmpz_clear(__gen_e_acsl__26);
+ __gmpz_clear(__gen_e_acsl_if_5);
+ return;
+}
+
+void __gen_e_acsl_f3(__e_acsl_mpz_struct * __retres_arg,
+ int __gen_e_acsl_n_arg)
+{
+ __e_acsl_mpz_t __gen_e_acsl_n_7;
+ __e_acsl_mpz_t __gen_e_acsl__23;
+ int __gen_e_acsl_gt;
+ __e_acsl_mpz_t __gen_e_acsl_if_6;
+ __gmpz_init_set_si(__gen_e_acsl_n_7,(long)__gen_e_acsl_n_arg);
+ __gmpz_init_set_si(__gen_e_acsl__23,0L);
+ __gen_e_acsl_gt = __gmpz_cmp((__e_acsl_mpz_struct const *)(__gen_e_acsl_n_7),
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl__23));
+ if (__gen_e_acsl_gt > 0) {
+ __e_acsl_mpz_t __gen_e_acsl_g_tapp;
+ __e_acsl_mpz_t __gen_e_acsl_n_8;
+ __e_acsl_mpz_t __gen_e_acsl__25;
+ __e_acsl_mpz_t __gen_e_acsl_sub_9;
+ __e_acsl_mpz_t __gen_e_acsl_f3_tapp_2;
+ __e_acsl_mpz_t __gen_e_acsl_mul_4;
+ __e_acsl_mpz_t __gen_e_acsl__31;
+ __e_acsl_mpz_t __gen_e_acsl_sub_12;
+ __gmpz_init(__gen_e_acsl_g_tapp);
+ __gen_e_acsl_g((__e_acsl_mpz_struct *)__gen_e_acsl_g_tapp,
+ __gen_e_acsl_n_arg);
+ __gmpz_init_set_si(__gen_e_acsl_n_8,(long)__gen_e_acsl_n_arg);
+ __gmpz_init_set_si(__gen_e_acsl__25,1L);
+ __gmpz_init(__gen_e_acsl_sub_9);
+ __gmpz_sub(__gen_e_acsl_sub_9,
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_n_8),
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl__25));
+ __gmpz_init(__gen_e_acsl_f3_tapp_2);
+ __gen_e_acsl_f3_2((__e_acsl_mpz_struct *)__gen_e_acsl_f3_tapp_2,
+ (__e_acsl_mpz_struct *)__gen_e_acsl_sub_9);
+ __gmpz_init(__gen_e_acsl_mul_4);
+ __gmpz_mul(__gen_e_acsl_mul_4,
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_g_tapp),
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_f3_tapp_2));
+ __gmpz_init_set_si(__gen_e_acsl__31,5L);
+ __gmpz_init(__gen_e_acsl_sub_12);
+ __gmpz_sub(__gen_e_acsl_sub_12,
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_mul_4),
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl__31));
+ __gmpz_init_set(__gen_e_acsl_if_6,
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_sub_12));
+ __gmpz_clear(__gen_e_acsl_g_tapp);
+ __gmpz_clear(__gen_e_acsl_n_8);
+ __gmpz_clear(__gen_e_acsl__25);
+ __gmpz_clear(__gen_e_acsl_sub_9);
+ __gmpz_clear(__gen_e_acsl_f3_tapp_2);
+ __gmpz_clear(__gen_e_acsl_mul_4);
+ __gmpz_clear(__gen_e_acsl__31);
+ __gmpz_clear(__gen_e_acsl_sub_12);
+ }
+ else {
+ __e_acsl_mpz_t __gen_e_acsl_n_11;
+ __e_acsl_mpz_t __gen_e_acsl__32;
+ __e_acsl_mpz_t __gen_e_acsl_add_4;
+ __e_acsl_mpz_t __gen_e_acsl_g_tapp_4;
+ __gmpz_init_set_si(__gen_e_acsl_n_11,(long)__gen_e_acsl_n_arg);
+ __gmpz_init_set_si(__gen_e_acsl__32,1L);
+ __gmpz_init(__gen_e_acsl_add_4);
+ __gmpz_add(__gen_e_acsl_add_4,
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_n_11),
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl__32));
+ __gmpz_init(__gen_e_acsl_g_tapp_4);
+ __gen_e_acsl_g_2((__e_acsl_mpz_struct *)__gen_e_acsl_g_tapp_4,
+ (__e_acsl_mpz_struct *)__gen_e_acsl_add_4);
+ __gmpz_init_set(__gen_e_acsl_if_6,
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_g_tapp_4));
+ __gmpz_clear(__gen_e_acsl_n_11);
+ __gmpz_clear(__gen_e_acsl__32);
+ __gmpz_clear(__gen_e_acsl_add_4);
+ __gmpz_clear(__gen_e_acsl_g_tapp_4);
+ }
+ __gmpz_init_set(__retres_arg,
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_if_6));
+ __gmpz_clear(__gen_e_acsl_n_7);
+ __gmpz_clear(__gen_e_acsl__23);
+ __gmpz_clear(__gen_e_acsl_if_6);
+ return;
+}
+
+void __gen_e_acsl_g(__e_acsl_mpz_struct * __retres_arg,
+ int __gen_e_acsl_n_arg)
+{
+ __e_acsl_mpz_t __gen_e_acsl__24;
+ __gmpz_init_set_si(__gen_e_acsl__24,0L);
+ __gmpz_init_set(__retres_arg,
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl__24));
+ __gmpz_clear(__gen_e_acsl__24);
+ return;
+}
+
+void __gen_e_acsl_g_2(__e_acsl_mpz_struct * __retres_arg,
+ __e_acsl_mpz_struct * __gen_e_acsl_n_arg)
+{
+ __e_acsl_mpz_t __gen_e_acsl_n_10;
+ __e_acsl_mpz_t __gen_e_acsl__27;
+ __gmpz_init_set(__gen_e_acsl_n_10,
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_n_arg));
+ __gmpz_init_set_si(__gen_e_acsl__27,0L);
+ __gmpz_init_set(__retres_arg,
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl__27));
+ __gmpz_clear(__gen_e_acsl_n_10);
+ __gmpz_clear(__gen_e_acsl__27);
+ return;
+}
+
+void __gen_e_acsl_f2(__e_acsl_mpz_struct * __retres_arg,
+ int __gen_e_acsl_n_arg)
+{
+ __e_acsl_mpz_t __gen_e_acsl_n_4;
+ __e_acsl_mpz_t __gen_e_acsl__10;
+ int __gen_e_acsl_lt;
+ __e_acsl_mpz_t __gen_e_acsl_if_4;
+ __gmpz_init_set_si(__gen_e_acsl_n_4,(long)__gen_e_acsl_n_arg);
+ __gmpz_init_set_si(__gen_e_acsl__10,0L);
+ __gen_e_acsl_lt = __gmpz_cmp((__e_acsl_mpz_struct const *)(__gen_e_acsl_n_4),
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl__10));
+ if (__gen_e_acsl_lt < 0) {
+ __e_acsl_mpz_t __gen_e_acsl__11;
+ __gmpz_init_set_si(__gen_e_acsl__11,1L);
+ __gmpz_init_set(__gen_e_acsl_if_4,
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl__11));
+ __gmpz_clear(__gen_e_acsl__11);
+ }
+ else {
+ __e_acsl_mpz_t __gen_e_acsl_n_5;
+ __e_acsl_mpz_t __gen_e_acsl__12;
+ __e_acsl_mpz_t __gen_e_acsl_sub_3;
+ __e_acsl_mpz_t __gen_e_acsl_f2_tapp_2;
+ __e_acsl_mpz_t __gen_e_acsl__19;
+ __e_acsl_mpz_t __gen_e_acsl_sub_7;
+ __e_acsl_mpz_t __gen_e_acsl_f2_tapp_6;
+ __e_acsl_mpz_t __gen_e_acsl_mul_2;
+ __e_acsl_mpz_t __gen_e_acsl__20;
+ __e_acsl_mpz_t __gen_e_acsl_sub_8;
+ __e_acsl_mpz_t __gen_e_acsl_f2_tapp_7;
+ __e_acsl_mpz_t __gen_e_acsl__21;
+ int __gen_e_acsl_div_guard_2;
+ __e_acsl_mpz_t __gen_e_acsl_div_2;
+ __gmpz_init_set_si(__gen_e_acsl_n_5,(long)__gen_e_acsl_n_arg);
+ __gmpz_init_set_si(__gen_e_acsl__12,1L);
+ __gmpz_init(__gen_e_acsl_sub_3);
+ __gmpz_sub(__gen_e_acsl_sub_3,
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_n_5),
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl__12));
+ __gmpz_init(__gen_e_acsl_f2_tapp_2);
+ __gen_e_acsl_f2_2((__e_acsl_mpz_struct *)__gen_e_acsl_f2_tapp_2,
+ (__e_acsl_mpz_struct *)__gen_e_acsl_sub_3);
+ __gmpz_init_set_si(__gen_e_acsl__19,2L);
+ __gmpz_init(__gen_e_acsl_sub_7);
+ __gmpz_sub(__gen_e_acsl_sub_7,
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_n_5),
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl__19));
+ __gmpz_init(__gen_e_acsl_f2_tapp_6);
+ __gen_e_acsl_f2_2((__e_acsl_mpz_struct *)__gen_e_acsl_f2_tapp_6,
+ (__e_acsl_mpz_struct *)__gen_e_acsl_sub_7);
+ __gmpz_init(__gen_e_acsl_mul_2);
+ __gmpz_mul(__gen_e_acsl_mul_2,
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_f2_tapp_2),
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_f2_tapp_6));
+ __gmpz_init_set_si(__gen_e_acsl__20,3L);
+ __gmpz_init(__gen_e_acsl_sub_8);
+ __gmpz_sub(__gen_e_acsl_sub_8,
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_n_5),
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl__20));
+ __gmpz_init(__gen_e_acsl_f2_tapp_7);
+ __gen_e_acsl_f2_2((__e_acsl_mpz_struct *)__gen_e_acsl_f2_tapp_7,
+ (__e_acsl_mpz_struct *)__gen_e_acsl_sub_8);
+ __gmpz_init_set_si(__gen_e_acsl__21,0L);
+ __gen_e_acsl_div_guard_2 = __gmpz_cmp((__e_acsl_mpz_struct const *)(__gen_e_acsl_f2_tapp_7),
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl__21));
+ __gmpz_init(__gen_e_acsl_div_2);
+ __e_acsl_assert(! (__gen_e_acsl_div_guard_2 == 0),(char *)"Assertion",
+ (char *)"f2_2",(char *)"f2(n - 3) == 0",9);
+ __gmpz_tdiv_q(__gen_e_acsl_div_2,
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_mul_2),
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_f2_tapp_7));
+ __gmpz_init_set(__gen_e_acsl_if_4,
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_div_2));
+ __gmpz_clear(__gen_e_acsl_n_5);
+ __gmpz_clear(__gen_e_acsl__12);
+ __gmpz_clear(__gen_e_acsl_sub_3);
+ __gmpz_clear(__gen_e_acsl_f2_tapp_2);
+ __gmpz_clear(__gen_e_acsl__19);
+ __gmpz_clear(__gen_e_acsl_sub_7);
+ __gmpz_clear(__gen_e_acsl_f2_tapp_6);
+ __gmpz_clear(__gen_e_acsl_mul_2);
+ __gmpz_clear(__gen_e_acsl__20);
+ __gmpz_clear(__gen_e_acsl_sub_8);
+ __gmpz_clear(__gen_e_acsl_f2_tapp_7);
+ __gmpz_clear(__gen_e_acsl__21);
+ __gmpz_clear(__gen_e_acsl_div_2);
+ }
+ __gmpz_init_set(__retres_arg,
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_if_4));
+ __gmpz_clear(__gen_e_acsl_n_4);
+ __gmpz_clear(__gen_e_acsl__10);
+ __gmpz_clear(__gen_e_acsl_if_4);
+ return;
+}
+
+void __gen_e_acsl_f2_2(__e_acsl_mpz_struct * __retres_arg,
+ __e_acsl_mpz_struct * __gen_e_acsl_n_arg)
+{
+ __e_acsl_mpz_t __gen_e_acsl_n_6;
+ __e_acsl_mpz_t __gen_e_acsl__13;
+ int __gen_e_acsl_lt_2;
+ __e_acsl_mpz_t __gen_e_acsl_if_3;
+ __gmpz_init_set(__gen_e_acsl_n_6,
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_n_arg));
+ __gmpz_init_set_si(__gen_e_acsl__13,0L);
+ __gen_e_acsl_lt_2 = __gmpz_cmp((__e_acsl_mpz_struct const *)(__gen_e_acsl_n_6),
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl__13));
+ if (__gen_e_acsl_lt_2 < 0) {
+ __e_acsl_mpz_t __gen_e_acsl__14;
+ __gmpz_init_set_si(__gen_e_acsl__14,1L);
+ __gmpz_init_set(__gen_e_acsl_if_3,
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl__14));
+ __gmpz_clear(__gen_e_acsl__14);
+ }
+ else {
+ __e_acsl_mpz_t __gen_e_acsl__15;
+ __e_acsl_mpz_t __gen_e_acsl_sub_4;
+ __e_acsl_mpz_t __gen_e_acsl_f2_tapp_3;
+ __e_acsl_mpz_t __gen_e_acsl__16;
+ __e_acsl_mpz_t __gen_e_acsl_sub_5;
+ __e_acsl_mpz_t __gen_e_acsl_f2_tapp_4;
+ __e_acsl_mpz_t __gen_e_acsl_mul;
+ __e_acsl_mpz_t __gen_e_acsl__17;
+ __e_acsl_mpz_t __gen_e_acsl_sub_6;
+ __e_acsl_mpz_t __gen_e_acsl_f2_tapp_5;
+ __e_acsl_mpz_t __gen_e_acsl__18;
+ int __gen_e_acsl_div_guard;
+ __e_acsl_mpz_t __gen_e_acsl_div;
+ __gmpz_init_set_si(__gen_e_acsl__15,1L);
+ __gmpz_init(__gen_e_acsl_sub_4);
+ __gmpz_sub(__gen_e_acsl_sub_4,
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_n_6),
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl__15));
+ __gmpz_init(__gen_e_acsl_f2_tapp_3);
+ __gen_e_acsl_f2_2((__e_acsl_mpz_struct *)__gen_e_acsl_f2_tapp_3,
+ (__e_acsl_mpz_struct *)__gen_e_acsl_sub_4);
+ __gmpz_init_set_si(__gen_e_acsl__16,2L);
+ __gmpz_init(__gen_e_acsl_sub_5);
+ __gmpz_sub(__gen_e_acsl_sub_5,
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_n_6),
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl__16));
+ __gmpz_init(__gen_e_acsl_f2_tapp_4);
+ __gen_e_acsl_f2_2((__e_acsl_mpz_struct *)__gen_e_acsl_f2_tapp_4,
+ (__e_acsl_mpz_struct *)__gen_e_acsl_sub_5);
+ __gmpz_init(__gen_e_acsl_mul);
+ __gmpz_mul(__gen_e_acsl_mul,
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_f2_tapp_3),
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_f2_tapp_4));
+ __gmpz_init_set_si(__gen_e_acsl__17,3L);
+ __gmpz_init(__gen_e_acsl_sub_6);
+ __gmpz_sub(__gen_e_acsl_sub_6,
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_n_6),
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl__17));
+ __gmpz_init(__gen_e_acsl_f2_tapp_5);
+ __gen_e_acsl_f2_2((__e_acsl_mpz_struct *)__gen_e_acsl_f2_tapp_5,
+ (__e_acsl_mpz_struct *)__gen_e_acsl_sub_6);
+ __gmpz_init_set_si(__gen_e_acsl__18,0L);
+ __gen_e_acsl_div_guard = __gmpz_cmp((__e_acsl_mpz_struct const *)(__gen_e_acsl_f2_tapp_5),
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl__18));
+ __gmpz_init(__gen_e_acsl_div);
+ __e_acsl_assert(! (__gen_e_acsl_div_guard == 0),(char *)"Assertion",
+ (char *)"f2_2",(char *)"f2(n - 3) == 0",9);
+ __gmpz_tdiv_q(__gen_e_acsl_div,
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_mul),
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_f2_tapp_5));
+ __gmpz_init_set(__gen_e_acsl_if_3,
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_div));
+ __gmpz_clear(__gen_e_acsl__15);
+ __gmpz_clear(__gen_e_acsl_sub_4);
+ __gmpz_clear(__gen_e_acsl_f2_tapp_3);
+ __gmpz_clear(__gen_e_acsl__16);
+ __gmpz_clear(__gen_e_acsl_sub_5);
+ __gmpz_clear(__gen_e_acsl_f2_tapp_4);
+ __gmpz_clear(__gen_e_acsl_mul);
+ __gmpz_clear(__gen_e_acsl__17);
+ __gmpz_clear(__gen_e_acsl_sub_6);
+ __gmpz_clear(__gen_e_acsl_f2_tapp_5);
+ __gmpz_clear(__gen_e_acsl__18);
+ __gmpz_clear(__gen_e_acsl_div);
+ }
+ __gmpz_init_set(__retres_arg,
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_if_3));
+ __gmpz_clear(__gen_e_acsl_n_6);
+ __gmpz_clear(__gen_e_acsl__13);
+ __gmpz_clear(__gen_e_acsl_if_3);
+ return;
+}
+
+void __gen_e_acsl_f1_2(__e_acsl_mpz_struct * __retres_arg,
+ __e_acsl_mpz_struct * __gen_e_acsl_n_arg)
+{
+ __e_acsl_mpz_t __gen_e_acsl_n_3;
+ __e_acsl_mpz_t __gen_e_acsl__4;
+ int __gen_e_acsl_le_2;
+ __e_acsl_mpz_t __gen_e_acsl_if;
+ __gmpz_init_set(__gen_e_acsl_n_3,
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_n_arg));
+ __gmpz_init_set_si(__gen_e_acsl__4,0L);
+ __gen_e_acsl_le_2 = __gmpz_cmp((__e_acsl_mpz_struct const *)(__gen_e_acsl_n_3),
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl__4));
+ if (__gen_e_acsl_le_2 <= 0) {
+ __e_acsl_mpz_t __gen_e_acsl__5;
+ __gmpz_init_set_si(__gen_e_acsl__5,0L);
+ __gmpz_init_set(__gen_e_acsl_if,
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl__5));
+ __gmpz_clear(__gen_e_acsl__5);
+ }
+ else {
+ __e_acsl_mpz_t __gen_e_acsl__6;
+ __e_acsl_mpz_t __gen_e_acsl_sub_2;
+ __e_acsl_mpz_t __gen_e_acsl_f1_tapp_3;
+ __e_acsl_mpz_t __gen_e_acsl_add;
+ __gmpz_init_set_si(__gen_e_acsl__6,1L);
+ __gmpz_init(__gen_e_acsl_sub_2);
+ __gmpz_sub(__gen_e_acsl_sub_2,
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_n_3),
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl__6));
+ __gmpz_init(__gen_e_acsl_f1_tapp_3);
+ /*@ assert
+ Eva: initialization:
+ \initialized((__e_acsl_mpz_struct *)__gen_e_acsl_sub_2);
+ */
+ /*@ assert
+ Eva: initialization:
+ \initialized((__e_acsl_mpz_struct *)__gen_e_acsl_f1_tapp_3);
+ */
+ __gen_e_acsl_f1_2((__e_acsl_mpz_struct *)__gen_e_acsl_f1_tapp_3,
+ (__e_acsl_mpz_struct *)__gen_e_acsl_sub_2);
+ __gmpz_init(__gen_e_acsl_add);
+ __gmpz_add(__gen_e_acsl_add,
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_f1_tapp_3),
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_n_3));
+ __gmpz_init_set(__gen_e_acsl_if,
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_add));
+ __gmpz_clear(__gen_e_acsl__6);
+ __gmpz_clear(__gen_e_acsl_sub_2);
+ __gmpz_clear(__gen_e_acsl_f1_tapp_3);
+ __gmpz_clear(__gen_e_acsl_add);
+ }
+ __gmpz_init_set(__retres_arg,
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_if));
+ __gmpz_clear(__gen_e_acsl_n_3);
+ __gmpz_clear(__gen_e_acsl__4);
+ __gmpz_clear(__gen_e_acsl_if);
+ return;
+}
+
+void __gen_e_acsl_f1(__e_acsl_mpz_struct * __retres_arg,
+ int __gen_e_acsl_n_arg)
+{
+ __e_acsl_mpz_t __gen_e_acsl_n;
+ __e_acsl_mpz_t __gen_e_acsl_;
+ int __gen_e_acsl_le;
+ __e_acsl_mpz_t __gen_e_acsl_if_2;
+ __gmpz_init_set_si(__gen_e_acsl_n,(long)__gen_e_acsl_n_arg);
+ __gmpz_init_set_si(__gen_e_acsl_,0L);
+ __gen_e_acsl_le = __gmpz_cmp((__e_acsl_mpz_struct const *)(__gen_e_acsl_n),
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_));
+ if (__gen_e_acsl_le <= 0) {
+ __e_acsl_mpz_t __gen_e_acsl__2;
+ __gmpz_init_set_si(__gen_e_acsl__2,0L);
+ __gmpz_init_set(__gen_e_acsl_if_2,
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl__2));
+ __gmpz_clear(__gen_e_acsl__2);
+ }
+ else {
+ __e_acsl_mpz_t __gen_e_acsl_n_2;
+ __e_acsl_mpz_t __gen_e_acsl__3;
+ __e_acsl_mpz_t __gen_e_acsl_sub;
+ __e_acsl_mpz_t __gen_e_acsl_f1_tapp_2;
+ __e_acsl_mpz_t __gen_e_acsl_add_2;
+ __gmpz_init_set_si(__gen_e_acsl_n_2,(long)__gen_e_acsl_n_arg);
+ __gmpz_init_set_si(__gen_e_acsl__3,1L);
+ __gmpz_init(__gen_e_acsl_sub);
+ __gmpz_sub(__gen_e_acsl_sub,
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_n_2),
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl__3));
+ __gmpz_init(__gen_e_acsl_f1_tapp_2);
+ /*@ assert
+ Eva: initialization:
+ \initialized((__e_acsl_mpz_struct *)__gen_e_acsl_sub);
+ */
+ /*@ assert
+ Eva: initialization:
+ \initialized((__e_acsl_mpz_struct *)__gen_e_acsl_f1_tapp_2);
+ */
+ __gen_e_acsl_f1_2((__e_acsl_mpz_struct *)__gen_e_acsl_f1_tapp_2,
+ (__e_acsl_mpz_struct *)__gen_e_acsl_sub);
+ __gmpz_init(__gen_e_acsl_add_2);
+ __gmpz_add(__gen_e_acsl_add_2,
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_f1_tapp_2),
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_n_2));
+ __gmpz_init_set(__gen_e_acsl_if_2,
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_add_2));
+ __gmpz_clear(__gen_e_acsl_n_2);
+ __gmpz_clear(__gen_e_acsl__3);
+ __gmpz_clear(__gen_e_acsl_sub);
+ __gmpz_clear(__gen_e_acsl_f1_tapp_2);
+ __gmpz_clear(__gen_e_acsl_add_2);
+ }
+ __gmpz_init_set(__retres_arg,
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_if_2));
+ __gmpz_clear(__gen_e_acsl_n);
+ __gmpz_clear(__gen_e_acsl_);
+ __gmpz_clear(__gen_e_acsl_if_2);
+ return;
+}
+
+
diff --git a/src/plugins/e-acsl/tests/runtime/oracle/local_goto.res.oracle b/src/plugins/e-acsl/tests/runtime/oracle/local_goto.res.oracle
index bdfaabe9c32..a2e7e709cc1 100644
--- a/src/plugins/e-acsl/tests/runtime/oracle/local_goto.res.oracle
+++ b/src/plugins/e-acsl/tests/runtime/oracle/local_goto.res.oracle
@@ -9,19 +9,19 @@
the generated program may miss memory instrumentation
if there are memory-related annotations.
[e-acsl] tests/runtime/local_goto.c:37: Warning:
- E-ACSL construct `logic function application' is not yet supported.
+ E-ACSL construct `logic functions with labels' is not yet supported.
Ignoring annotation.
[e-acsl] tests/runtime/local_goto.c:37: Warning:
E-ACSL construct `assigns clause in behavior' is not yet supported.
Ignoring annotation.
[e-acsl] tests/runtime/local_goto.c:28: Warning:
- E-ACSL construct `logic function application' is not yet supported.
+ E-ACSL construct `logic functions with labels' is not yet supported.
Ignoring annotation.
[e-acsl] tests/runtime/local_goto.c:28: Warning:
E-ACSL construct `assigns clause in behavior' is not yet supported.
Ignoring annotation.
[e-acsl] tests/runtime/local_goto.c:16: Warning:
- E-ACSL construct `logic function application' is not yet supported.
+ E-ACSL construct `logic functions with labels' is not yet supported.
Ignoring annotation.
[e-acsl] tests/runtime/local_goto.c:16: Warning:
E-ACSL construct `assigns clause in behavior' is not yet supported.
diff --git a/src/plugins/e-acsl/tests/runtime/oracle/mainargs.res.oracle b/src/plugins/e-acsl/tests/runtime/oracle/mainargs.res.oracle
index f0225cf73e6..bb9147c4b0e 100644
--- a/src/plugins/e-acsl/tests/runtime/oracle/mainargs.res.oracle
+++ b/src/plugins/e-acsl/tests/runtime/oracle/mainargs.res.oracle
@@ -3,13 +3,14 @@
the generated program may miss memory instrumentation
if there are memory-related annotations.
[e-acsl] FRAMAC_SHARE/libc/string.h:125: Warning:
- E-ACSL construct `logic function application' is not yet supported.
+ E-ACSL construct `logic functions with labels' is not yet supported.
Ignoring annotation.
[e-acsl] FRAMAC_SHARE/libc/string.h:125: Warning:
E-ACSL construct `assigns clause in behavior' is not yet supported.
Ignoring annotation.
[e-acsl] FRAMAC_SHARE/libc/string.h:127: Warning:
- E-ACSL construct `logic function returning an integer' is not yet supported.
+ E-ACSL construct `logic functions performing read accesses'
+ is not yet supported.
Ignoring annotation.
[e-acsl] translation done in project "e-acsl".
[eva:alarm] tests/runtime/mainargs.c:12: Warning: assertion got status unknown.
diff --git a/src/plugins/e-acsl/tests/temporal/oracle/t_getenv.res.oracle b/src/plugins/e-acsl/tests/temporal/oracle/t_getenv.res.oracle
index 1b9876f5a9b..90bbf0ce762 100644
--- a/src/plugins/e-acsl/tests/temporal/oracle/t_getenv.res.oracle
+++ b/src/plugins/e-acsl/tests/temporal/oracle/t_getenv.res.oracle
@@ -2,8 +2,8 @@
[e-acsl] Warning: annotating undefined function `getenv':
the generated program may miss memory instrumentation
if there are memory-related annotations.
-[e-acsl] FRAMAC_SHARE/libc/stdlib.h:482: Warning:
- E-ACSL construct `logic function application' is not yet supported.
+[e-acsl] FRAMAC_SHARE/libc/stdlib.h:419: Warning:
+ E-ACSL construct `logic functions with labels' is not yet supported.
Ignoring annotation.
[e-acsl] FRAMAC_SHARE/libc/stdlib.h:482: Warning:
E-ACSL construct `assigns clause in behavior' is not yet supported.
diff --git a/src/plugins/e-acsl/tests/temporal/oracle/t_malloc-asan.res.oracle b/src/plugins/e-acsl/tests/temporal/oracle/t_malloc-asan.res.oracle
index dfe484df046..1b8c383a119 100644
--- a/src/plugins/e-acsl/tests/temporal/oracle/t_malloc-asan.res.oracle
+++ b/src/plugins/e-acsl/tests/temporal/oracle/t_malloc-asan.res.oracle
@@ -3,7 +3,7 @@
the generated program may miss memory instrumentation
if there are memory-related annotations.
[e-acsl] tests/temporal/t_malloc-asan.c:31: Warning:
- E-ACSL construct `logic function application' is not yet supported.
+ E-ACSL construct `logic functions with labels' is not yet supported.
Ignoring annotation.
[e-acsl] tests/temporal/t_malloc-asan.c:31: Warning:
E-ACSL construct `assigns clause in behavior' is not yet supported.
diff --git a/src/plugins/e-acsl/tests/temporal/oracle/t_memcpy.res.oracle b/src/plugins/e-acsl/tests/temporal/oracle/t_memcpy.res.oracle
index 70f435a9631..52253f07981 100644
--- a/src/plugins/e-acsl/tests/temporal/oracle/t_memcpy.res.oracle
+++ b/src/plugins/e-acsl/tests/temporal/oracle/t_memcpy.res.oracle
@@ -8,19 +8,20 @@
[e-acsl] FRAMAC_SHARE/libc/string.h:92: Warning:
E-ACSL construct `\separated' is not yet supported. Ignoring annotation.
[e-acsl] FRAMAC_SHARE/libc/string.h:115: Warning:
- E-ACSL construct `logic function application' is not yet supported.
+ E-ACSL construct `logic functions with labels' is not yet supported.
Ignoring annotation.
[e-acsl] FRAMAC_SHARE/libc/string.h:115: Warning:
E-ACSL construct `assigns clause in behavior' is not yet supported.
Ignoring annotation.
[e-acsl] FRAMAC_SHARE/libc/string.h:118: Warning:
- E-ACSL construct `user-defined logic type' is not yet supported.
+ E-ACSL construct `logic functions performing read accesses'
+ is not yet supported.
Ignoring annotation.
[e-acsl] FRAMAC_SHARE/libc/string.h:92: Warning:
- E-ACSL construct `logic function application' is not yet supported.
+ E-ACSL construct `logic functions with labels' is not yet supported.
Ignoring annotation.
[e-acsl] FRAMAC_SHARE/libc/string.h:93: Warning:
- E-ACSL construct `logic function application' is not yet supported.
+ E-ACSL construct `logic functions with labels' is not yet supported.
Ignoring annotation.
[e-acsl] FRAMAC_SHARE/libc/string.h:95: Warning:
E-ACSL construct `\separated' is not yet supported. Ignoring annotation.
@@ -28,6 +29,7 @@
E-ACSL construct `assigns clause in behavior' is not yet supported.
Ignoring annotation.
[e-acsl] FRAMAC_SHARE/libc/string.h:98: Warning:
- E-ACSL construct `logic function returning an integer' is not yet supported.
+ E-ACSL construct `logic functions performing read accesses'
+ is not yet supported.
Ignoring annotation.
[e-acsl] translation done in project "e-acsl".
diff --git a/src/plugins/e-acsl/translate.ml b/src/plugins/e-acsl/translate.ml
index 60bc68beda0..7f39ca576ab 100644
--- a/src/plugins/e-acsl/translate.ml
+++ b/src/plugins/e-acsl/translate.ml
@@ -448,8 +448,7 @@ and context_insensitive_term_to_exp kf env t =
| TStartOf lv ->
let lv, env, _ = tlval_to_lval kf env lv in
Cil.mkAddrOrStartOf ~loc lv, env, false, "startof"
- | Tapp(li, [], args) when Builtins.mem li.l_var_info.lv_name ->
- (* E-ACSL built-in function call *)
+ | Tapp(li, [], targs) ->
let fname = li.l_var_info.lv_name in
let args, env = (* args computed in the reverse order *)
try
@@ -458,7 +457,7 @@ and context_insensitive_term_to_exp kf env t =
let e, env = term_to_exp kf env a in
e :: l, env)
([], env)
- args
+ targs
with Invalid_argument _ ->
Options.fatal "[Tapp] unexpected number of arguments when calling %s"
fname
@@ -466,6 +465,8 @@ and context_insensitive_term_to_exp kf env t =
(* build the varinfo (as an expression) which stores the result of the
function call. *)
let _, e, env =
+ if Builtins.mem li.l_var_info.lv_name then begin
+ (* E-ACSL built-in function call *)
Env.new_var
~loc
~name:(fname ^ "_app")
@@ -474,10 +475,20 @@ and context_insensitive_term_to_exp kf env t =
(Misc.cty (Extlib.the li.l_type))
(fun vi _ ->
[ Misc.mk_call ~loc ~result:(Cil.var vi) fname (List.rev args) ])
+ end
+ else
+ let args_lty = List.map
+ (fun targ ->
+ match Typing.get_integer_ty targ with
+ | Typing.Gmp -> Linteger
+ | Typing.C_type _ | Typing.Other -> Ctype (Typing.get_typ targ))
+ targs
+ in
+ Lfunctions.generate ~loc env t li (List.rev args) args_lty
in
e, env, false, "app"
- | Tapp _ ->
- not_yet env "applying logic function"
+ | Tapp(_, _ :: _, _) ->
+ not_yet env "logic functions with labels"
| Tlambda _ -> not_yet env "functional"
| TDataCons _ -> not_yet env "constructor"
| Tif(t1, t2, t3) ->
@@ -648,7 +659,22 @@ and named_predicate_content_to_exp ?name kf env p =
match p.pred_content with
| Pfalse -> Cil.zero ~loc, env
| Ptrue -> Cil.one ~loc, env
- | Papp _ -> not_yet env "logic function application"
+ | Papp(li, labels, args) ->
+ (* Simply use the implementation of Tapp(li, labels, args).
+ To achieve this, we create a clone of [li] for which the type is
+ transformed from [None] (type of predicates) to
+ [Some int] (type as a term).
+ TODO: the approach seems dangerous. A better way would probably use a
+ version of [Lfunctions.generate] generalized to predicates. *)
+ let prj = Project.current () in
+ let o = object inherit Visitor.frama_c_copy prj end in
+ let li = Visitor.visitFramacLogicInfo o li in
+ let lty = Ctype Cil.intType in
+ li.l_type <- Some lty;
+ let tapp = Logic_const.term ~loc (Tapp(li, labels, args)) lty in
+ Typing.type_term ~use_gmp_opt:false ~ctx:Typing.c_int tapp;
+ let e, env = term_to_exp kf env tapp in
+ e, env
| Pseparated _ -> not_yet env "\\separated"
| Pdangling _ -> not_yet env "\\dangling"
| Pvalid_function _ -> not_yet env "\\valid_function"
@@ -837,6 +863,9 @@ and translate_named_predicate kf env p =
let named_predicate_to_exp ?name kf env p =
named_predicate_to_exp ?name kf env p (* forget optional argument ?rte *)
+let add_cast_lfunctions loc env cty is_mpz e =
+ add_cast ~loc env cty is_mpz None e
+
let () =
Loops.term_to_exp_ref := term_to_exp;
Loops.translate_named_predicate_ref := translate_named_predicate;
@@ -845,7 +874,10 @@ let () =
At_with_lscope.term_to_exp_ref := term_to_exp;
At_with_lscope.predicate_to_exp_ref := named_predicate_to_exp;
Mmodel_translate.term_to_exp_ref := term_to_exp;
- Mmodel_translate.predicate_to_exp_ref := named_predicate_to_exp
+ Mmodel_translate.predicate_to_exp_ref := named_predicate_to_exp;
+ Lfunctions.term_to_exp_ref := term_to_exp;
+ Lfunctions.predicate_to_exp_ref := named_predicate_to_exp;
+ Lfunctions.add_cast_ref := add_cast_lfunctions
(* This function is used by Guillaume.
However, it is correct to use it only in specific contexts. *)
diff --git a/src/plugins/e-acsl/typing.ml b/src/plugins/e-acsl/typing.ml
index ee2dcb2ffe5..556981d303a 100644
--- a/src/plugins/e-acsl/typing.ml
+++ b/src/plugins/e-acsl/typing.ml
@@ -94,6 +94,12 @@ let typ_of_integer_ty = function
| C_type ik -> TInt(ik, [])
| Other -> raise Not_an_integer
+let typ_of_lty = function
+ | Ctype cty -> cty
+ | Linteger -> Gmpz.t ()
+ | Lreal -> Error.not_yet "real numbers"
+ | Ltype _ | Lvar _ | Larrow _ -> Options.fatal "unexpected logic type"
+
(******************************************************************************)
(** Memoization *)
(******************************************************************************)
@@ -110,6 +116,7 @@ type computed_info =
module Memo: sig
val memo: (term -> computed_info) -> term -> computed_info
val get: term -> computed_info
+ val remove_all: term -> unit
val clear: unit -> unit
end = struct
@@ -148,10 +155,30 @@ end = struct
H.add tbl t x;
x
+ let rec remove_all t =
+ try
+ ignore (H.find tbl t);
+ H.remove tbl t;
+ remove_all t
+ with Not_found ->
+ ()
+
let clear () = H.clear tbl
end
+let clear_all_pred_or_term pot =
+ let o = object inherit Visitor.frama_c_inplace
+ method !vterm t =
+ Memo.remove_all t;
+ Cil.DoChildren
+ end
+ in
+ begin match pot with
+ | Misc.PoT_term t -> ignore(Visitor.visitFramacTerm o t)
+ | Misc.PoT_pred p -> ignore(Visitor.visitFramacPredicate o p)
+ end
+
(******************************************************************************)
(** {2 Coercion rules} *)
(******************************************************************************)
@@ -171,19 +198,7 @@ let integer_ty_of_typ ty = ty_of_logic_ty (Ctype ty)
interval. It is the \theta operator of the JFLA's paper. *)
let ty_of_interv ?ctx i =
try
- let itv_kind =
- if Ival.is_bottom i then IInt
- else match Ival.min_and_max i with
- | Some l, Some u ->
- let is_pos = Integer.ge l Integer.zero in
- let lkind = Cil.intKindForValue l is_pos in
- let ukind = Cil.intKindForValue u is_pos in
- (* kind corresponding to the interval *)
- if Cil.intTypeIncluded lkind ukind then ukind else lkind
- | None, None -> raise Cil.Not_representable (* GMP *)
- | None, Some _ | Some _, None ->
- Kernel.fatal ~current:true "ival: %a" Ival.pretty i
- in
+ let itv_kind = Misc.itv_kind i in
(* convert the kind to [IInt] whenever smaller. *)
let kind = if Cil.intTypeIncluded itv_kind IInt then IInt else itv_kind in
(* ctx type whenever possible to prevent superfluous casts in the generated
@@ -462,14 +477,43 @@ let rec type_term ~use_gmp_opt ?(arith_operand=false) ?ctx t =
dup Other
| Tapp(li, _, args) ->
- let typ_arg lvi arg =
- let ctx = ty_of_logic_ty lvi.lv_type in
- ignore (type_term ~use_gmp_opt:false ~ctx arg)
- in
- List.iter2 typ_arg li.l_profile args;
- (* [li.l_type is [None] for predicate only: not possible here.
- Thus using [Extlib.the] is fine *)
- dup (ty_of_logic_ty (Extlib.the li.l_type))
+ List.iter
+ (fun arg -> ignore (type_term ~use_gmp_opt:true arg))
+ args;
+ begin match li.l_body with
+ | LBpred _ ->
+ (* We can have an [LBpred] here because we transformed
+ [Papp] into [Tapp] *)
+ dup c_int
+ | LBterm _ ->
+ begin match li.l_type with
+ | None ->
+ assert false
+ | Some lty ->
+ begin match lty with
+ | Linteger ->
+ let i = Interval.infer t in
+ if Options.Gmp_only.get () then dup Gmp
+ else dup (ty_of_interv i)
+ | Ctype TInt(ik, _ ) ->
+ dup (C_type ik)
+ | Ctype TFloat _ -> (* TODO: handle in MR !226 *)
+ dup Other
+ | Lreal ->
+ Error.not_yet "real numbers"
+ | Ctype _ ->
+ dup Other
+ | Ltype _ | Lvar _ | Larrow _ ->
+ Options.fatal "unexpected type"
+ end
+ end
+ | LBnone ->
+ Error.not_yet "logic functions with no definition nor reads clause"
+ | LBreads _ ->
+ Error.not_yet "logic functions performing read accesses"
+ | LBinductive _ ->
+ Error.not_yet "logic functions inductively defined"
+ end
| Tunion _ -> Error.not_yet "tset union"
| Tinter _ -> Error.not_yet "tset intersection"
@@ -528,7 +572,18 @@ let rec type_predicate p =
(* this pattern matching also follows the formal rules of the JFLA's paper *)
let op = match p.pred_content with
| Pfalse | Ptrue -> c_int
- | Papp _ -> Error.not_yet "logic function application"
+ | Papp(li, _, _) ->
+ begin match li.l_body with
+ | LBpred _ ->
+ (* No need to type subpredicates
+ since Papp will be transformed into Tapp in Translate:
+ a retyping is done there *)
+ c_int
+ | LBnone -> (* Eg: \is_finite *)
+ Error.not_yet "logic functions with no definition nor reads clause"
+ | LBreads _ | LBterm _ | LBinductive _ ->
+ Options.fatal "unexpected logic definition"
+ end
| Pseparated _ -> Error.not_yet "\\separated"
| Pdangling _ -> Error.not_yet "\\dangling"
| Prel(_, t1, t2) ->
diff --git a/src/plugins/e-acsl/typing.mli b/src/plugins/e-acsl/typing.mli
index 8182360e77e..7f26c6e68d7 100644
--- a/src/plugins/e-acsl/typing.mli
+++ b/src/plugins/e-acsl/typing.mli
@@ -76,6 +76,9 @@ val typ_of_integer_ty: integer_ty -> typ
val integer_ty_of_typ: typ -> integer_ty
(** Reverse of [typ_of_integer_ty] *)
+val ty_of_logic_ty: logic_type -> integer_ty
+(** @return the {!integer_ty} that correponds to the given logic type. *)
+
val join: integer_ty -> integer_ty -> integer_ty
(** {!integer_ty} is a join-semi-lattice if you do not consider [Other]. If
there is no [Other] in argument, this function computes the join of this
@@ -98,6 +101,10 @@ val type_named_predicate: ?must_clear:bool -> predicate -> unit
val clear: unit -> unit
(** Remove all the previously computed types. *)
+val clear_all_pred_or_term: Misc.pred_or_term -> unit
+(** Remove all the previously computed types for the given term or predicate
+ AND its subterms. *)
+
(** {3 Getters}
Below, the functions assume that either {!type_term} or
@@ -132,15 +139,17 @@ val unsafe_set: term -> ?ctx:integer_ty -> integer_ty -> unit
(** Register that the given term has the given type in the given context (if
any). No verification is done. *)
-
(*****************************************************************************)
-(* Utils *)
+(** {2 Typing/types-related utils} *)
(*****************************************************************************)
val ty_of_interv: ?ctx:integer_ty -> Ival.t -> integer_ty
(* Compute the smallest type (bigger than [int]) which can contain the whole
interval. It is the \theta operator of the JFLA's paper. *)
+val typ_of_lty: logic_type -> typ
+(** @return the C type that correponds to the given logic type. *)
+
(******************************************************************************)
(** {2 Internal stuff} *)
(******************************************************************************)
diff --git a/src/plugins/e-acsl/visit.ml b/src/plugins/e-acsl/visit.ml
index a512b5eb8e5..226d8ced23d 100644
--- a/src/plugins/e-acsl/visit.ml
+++ b/src/plugins/e-acsl/visit.ml
@@ -369,6 +369,8 @@ class e_acsl_visitor prj generate = object (self)
if generate then Project.copy ~selection ~src:cur prj;
Cil.DoChildrenPost
(fun f ->
+ (* generate the C functions that correspond to the logic ones *)
+ Lfunctions.do_visit f;
(* extend [main] with forward initialization and put it at end *)
if generate then begin
if not (Global_observer.is_empty () && Literal_strings.is_empty ())
--
GitLab