diff --git a/src/plugins/e-acsl/Makefile.in b/src/plugins/e-acsl/Makefile.in
index c366ab4588b3466bc5ebd711bc779af46c8a88e7..fc9b5349f30bd57b7b4b40dc4845a32b7051612b 100644
--- a/src/plugins/e-acsl/Makefile.in
+++ b/src/plugins/e-acsl/Makefile.in
@@ -79,6 +79,7 @@ PLUGIN_CMO:= local_config \
quantif \
at_with_lscope \
mmodel_translate \
+ logic_functions \
translate \
temporal \
prepare_ast \
diff --git a/src/plugins/e-acsl/at_with_lscope.ml b/src/plugins/e-acsl/at_with_lscope.ml
index c4981badab3bdf0f309f841e3b22eebd0a2e1ccc..9602bb5b61445e8aeb7051612f5faf469314052a 100644
--- a/src/plugins/e-acsl/at_with_lscope.ml
+++ b/src/plugins/e-acsl/at_with_lscope.ml
@@ -237,46 +237,47 @@ let to_exp ~loc kf env pot label =
end
in
let ty_ptr = TPtr(ty, []) in
- let vi_at, e_at, env = Env.new_var
- ~loc
- ~name:"at"
- ~scope:Env.Function
- env
- None
- ty_ptr
- (fun vi e ->
- (* Handle [malloc] and [free] stmts *)
- let lty_sizeof = Ctype Cil.(theMachine.typeOfSizeOf) in
- let t_sizeof = Logic_const.term ~loc (TSizeOf ty) lty_sizeof in
- let t_size = size_from_sizes_and_shifts ~loc sizes_and_shifts in
- let t_size =
- Logic_const.term ~loc (TBinOp(Mult, t_sizeof, t_size)) lty_sizeof
- in
- Typing.type_term ~use_gmp_opt:false t_size;
- let malloc_stmt = match Typing.get_integer_ty t_size with
- | Typing.C_type IInt ->
- let e_size, _ = term_to_exp kf env t_size in
- let e_size = Cil.constFold false e_size in
- let malloc_stmt =
- Misc.mk_call ~loc ~result:(Cil.var vi) "malloc" [e_size]
- in
- malloc_stmt
- | Typing.C_type _ | Typing.Gmp ->
- Error.not_yet
- "\\at on purely logic variables that needs to allocate \
- too much memory (bigger than int_max bytes)"
- | Typing.Other ->
- Options.fatal
- "quantification over non-integer type is not part of E-ACSL"
- in
- let free_stmt = Misc.mk_call ~loc "free" [e] in
- (* The list of stmts returned by the current closure are inserted
- LOCALLY to the block where the new var is FIRST used, whatever scope
- is indicated to [Env.new_var].
- Thus we need to add [malloc] and [free] through dedicated functions. *)
- Malloc.add kf malloc_stmt;
- Free.add kf free_stmt;
- [])
+ let vi_at, e_at, env =
+ Env.new_var
+ ~loc
+ ~name:"at"
+ ~scope:Env.Function
+ env
+ None
+ ty_ptr
+ (fun vi e ->
+ (* Handle [malloc] and [free] stmts *)
+ let lty_sizeof = Ctype Cil.(theMachine.typeOfSizeOf) in
+ let t_sizeof = Logic_const.term ~loc (TSizeOf ty) lty_sizeof in
+ let t_size = size_from_sizes_and_shifts ~loc sizes_and_shifts in
+ let t_size =
+ Logic_const.term ~loc (TBinOp(Mult, t_sizeof, t_size)) lty_sizeof
+ in
+ Typing.type_term ~use_gmp_opt:false t_size;
+ let malloc_stmt = match Typing.get_integer_ty t_size with
+ | Typing.C_type IInt ->
+ let e_size, _ = term_to_exp kf env t_size in
+ let e_size = Cil.constFold false e_size in
+ let malloc_stmt =
+ Misc.mk_call ~loc ~result:(Cil.var vi) "malloc" [e_size]
+ in
+ malloc_stmt
+ | Typing.C_type _ | Typing.Gmp ->
+ Error.not_yet
+ "\\at on purely logic variables that needs to allocate \
+ too much memory (bigger than int_max bytes)"
+ | Typing.Other ->
+ Options.fatal
+ "quantification over non-integer type is not part of E-ACSL"
+ in
+ let free_stmt = Misc.mk_call ~loc "free" [e] in
+ (* The list of stmts returned by the current closure are inserted
+ LOCALLY to the block where the new var is FIRST used, whatever scope
+ is indicated to [Env.new_var]. Thus we need to add [malloc] and
+ [free] through dedicated functions. *)
+ Malloc.add kf malloc_stmt;
+ Free.add kf free_stmt;
+ [])
in
(* Index *)
let t_index = index_from_sizes_and_shifts ~loc sizes_and_shifts in
@@ -337,4 +338,4 @@ let to_exp ~loc kf env pot label =
(* Returning *)
let lval_at_index, env = lval_at_index ~loc kf env (e_at, vi_at, t_index) in
let e = Cil.new_exp ~loc (Lval lval_at_index) in
- e, env
\ No newline at end of file
+ e, env
diff --git a/src/plugins/e-acsl/builtins.ml b/src/plugins/e-acsl/builtins.ml
index 45467db85bc2a5a59e5355efcff42e380860567a..ca591dc3496d098ac6e933a0f56a7bfbfa891b4c 100644
--- a/src/plugins/e-acsl/builtins.ml
+++ b/src/plugins/e-acsl/builtins.ml
@@ -39,7 +39,7 @@ let update s vi =
with Not_found ->
()
-(* add [vi] in the built-in table if it is an E-ACSL built-in which is not
+(* add [vi] in the built-in table if it is an E-ACSL built-in that is not
[already] registered. *)
let add_builtin vi already =
if not already then
diff --git a/src/plugins/e-acsl/doc/Changelog b/src/plugins/e-acsl/doc/Changelog
index d47f3ef037ef8ffb6449bd85bac690a6436b9582..d548c07e389d43c27bb25ef058a5b39c69fd5ab5 100644
--- a/src/plugins/e-acsl/doc/Changelog
+++ b/src/plugins/e-acsl/doc/Changelog
@@ -19,6 +19,8 @@
# configure configure
###############################################################################
+- E-ACSL [2019/04/29] Support for logic functions and predicates
+ without labels.
- runtime [2019/02/26] The behavior of __e_acsl_assert now depends on the
runtime value of the global variable __e_acsl_sound_verdict:
if 0, it means that its verdict is possibly incorrect.
diff --git a/src/plugins/e-acsl/dup_functions.ml b/src/plugins/e-acsl/dup_functions.ml
index 1e4b879d31923d8124661ae2f523674c8dc9f98d..0deac191f99cfd33e930bb3e9e19085a1e490fc3 100644
--- a/src/plugins/e-acsl/dup_functions.ml
+++ b/src/plugins/e-acsl/dup_functions.ml
@@ -123,7 +123,8 @@ let dup_fundec loc spec bhv sound_verdict_vi kf vi new_vi =
if vi.vname = "" then
(* unnamed formal parameter: must generate a fresh name since a fundec
cannot have unnamed formals (see bts #2303). *)
- Env.Varname.get ~scope:Env.Function
+ Env.Varname.get
+ ~scope:Env.Function
(Functions.RTL.mk_gen_name "unamed_formal")
else
vi.vname
diff --git a/src/plugins/e-acsl/env.ml b/src/plugins/e-acsl/env.ml
index c571fb5333ace122ff9f20d5fac8f1a0ad1fa5d8..fd2e6d3b2083e1f32fb6a0f4d16d27e8b803f49f 100644
--- a/src/plugins/e-acsl/env.ml
+++ b/src/plugins/e-acsl/env.ml
@@ -24,6 +24,11 @@ module E_acsl_label = Label
open Cil_types
open Cil_datatype
+type localized_scope =
+ | LGlobal
+ | LFunction of kernel_function
+ | LLocal_block of kernel_function
+
type scope =
| Global
| Function
@@ -55,7 +60,7 @@ type t =
lscope: Lscope.t;
lscope_reset: bool;
annotation_kind: Misc.annotation_kind;
- new_global_vars: (varinfo * scope) list;
+ new_global_vars: (varinfo * localized_scope) list;
(* generated variables. The scope indicates the level where the variable
should be added. *)
global_mpz_tbl: mpz_tbl;
@@ -141,6 +146,19 @@ let has_no_new_stmt env =
let local, _ = top env in
local.block_info = empty_block
+let current_kf env =
+ let v = env.visitor in
+ match v#current_kf with
+ | 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
+
(* ************************************************************************** *)
(** {2 Loop invariants} *)
(* ************************************************************************** *)
@@ -189,6 +207,11 @@ let do_new_var ~loc ?(scope=Local_block) ?(name="") env t ty mk_stmts =
ty
in
v.vreferenced <- true;
+ let lscope = match scope with
+ | Global -> LGlobal
+ | Function -> LFunction (Extlib.the (current_kf env))
+ | Local_block -> LLocal_block (Extlib.the (current_kf env))
+ in
(* Options.feedback "new variable %a (global? %b)" Varinfo.pretty v global;*)
let e = Cil.evar v in
let stmts = mk_stmts v e in
@@ -222,7 +245,7 @@ let do_new_var ~loc ?(scope=Local_block) ?(name="") env t ty mk_stmts =
(* also memoize the new variable, but must never be used *)
{ env with
cpt = n;
- new_global_vars = (v, scope) :: env.new_global_vars;
+ new_global_vars = (v, lscope) :: env.new_global_vars;
global_mpz_tbl = extend_tbl env.global_mpz_tbl;
env_stack = local_env :: tl_env }
| Local_block ->
@@ -234,9 +257,9 @@ let do_new_var ~loc ?(scope=Local_block) ?(name="") env t ty mk_stmts =
{ env with
cpt = n;
env_stack = local_env :: tl_env;
- new_global_vars = (v, scope) :: env.new_global_vars }
+ new_global_vars = (v, lscope) :: env.new_global_vars }
end else
- let new_global_vars = (v, scope) :: env.new_global_vars in
+ let new_global_vars = (v, lscope) :: env.new_global_vars in
let local_env =
{ local_env with
block_info = new_block;
@@ -262,10 +285,8 @@ let new_var ~loc ?(scope=Local_block) ?name env t ty mk_stmts =
do_new_var ~loc ~scope ?name env t ty mk_stmts
in
match scope with
- | Global | Function ->
- memo env.global_mpz_tbl
- | Local_block ->
- memo local_env.mpz_tbl
+ | Global | Function -> memo env.global_mpz_tbl
+ | Local_block -> memo local_env.mpz_tbl
let new_var_and_mpz_init ~loc ?scope ?name env t mk_stmts =
new_var
@@ -279,19 +300,29 @@ let new_var_and_mpz_init ~loc ?scope ?name env t mk_stmts =
module Logic_binding = struct
+ let add_binding env logic_v vi =
+ try
+ let varinfos = Logic_var.Map.find logic_v 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 logic_v varinfos env.var_mapping in
+ { env with var_mapping = var_mapping }
+
let add ?ty env logic_v =
let ty = match ty with
| Some ty -> ty
| None -> match logic_v.lv_type with
- | Ctype ty -> ty
- | Linteger -> Gmpz.t ()
- | Ltype _ as ty when Logic_const.is_boolean_type ty -> Cil.charType
- | Ltype _ | Lvar _ | Lreal | Larrow _ as lty ->
- let msg =
- Format.asprintf
- "logic variable of type %a" Logic_type.pretty lty
- in
- Error.not_yet msg
+ | Ctype ty -> ty
+ | Linteger -> Gmpz.t ()
+ | Ltype _ as ty when Logic_const.is_boolean_type ty -> Cil.charType
+ | Ltype _ | Lvar _ | Lreal | Larrow _ as lty ->
+ let msg =
+ Format.asprintf "logic variable of type %a" Logic_type.pretty lty
+ in
+ Error.not_yet msg
in
let v, e, env = new_var
~loc:Location.unknown
@@ -301,18 +332,7 @@ module Logic_binding = struct
ty
(fun _ _ -> [])
in
- let env =
- try
- let varinfos = Logic_var.Map.find logic_v env.var_mapping in
- Stack.push v varinfos;
- env
- with Not_found ->
- let varinfos = Stack.create () in
- Stack.push v varinfos;
- let var_mapping = Logic_var.Map.add logic_v varinfos env.var_mapping in
- { env with var_mapping = var_mapping }
- in
- v, e, env
+ v, e, add_binding env logic_v v
let get env logic_v =
try
@@ -324,22 +344,12 @@ module Logic_binding = struct
let remove env logic_v =
try
let varinfos = Logic_var.Map.find logic_v env.var_mapping in
- ignore (Stack.pop varinfos);
- env
+ ignore (Stack.pop varinfos)
with Not_found | Stack.Empty ->
assert false
end
-let current_kf env =
- let v = env.visitor in
- match v#current_kf with
- | None -> None
- | Some kf -> Some (Cil.get_kernel_function v#behavior kf)
-
-let get_visitor env = env.visitor
-let get_behavior env = env.visitor#behavior
-
module Logic_scope = struct
let get env = env.lscope
let extend env lvs = { env with lscope = Lscope.add lvs env.lscope }
@@ -508,7 +518,9 @@ module Context = struct
{ env with new_global_vars =
List.filter
(fun (v, scope) ->
- (scope = Global || scope = Function)
+ (match scope with
+ | LGlobal | LFunction _ -> true
+ | LLocal_block _ -> false)
&& List.for_all (fun (v', _) -> v != v') vars)
!ctx
@ vars }
diff --git a/src/plugins/e-acsl/env.mli b/src/plugins/e-acsl/env.mli
index 7fe184e3d026caead108691fab9f09660331006b..d3d408eb20d64a8accff900abab575376c981060 100644
--- a/src/plugins/e-acsl/env.mli
+++ b/src/plugins/e-acsl/env.mli
@@ -36,6 +36,11 @@ val has_no_new_stmt: t -> bool
(** Assume that a local context has been previously pushed.
@return true iff the given env does not contain any new statement. *)
+type localized_scope =
+ | LGlobal
+ | LFunction of kernel_function
+ | LLocal_block of kernel_function
+
type scope =
| Global
| Function
@@ -68,11 +73,16 @@ 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_binding: t -> logic_var -> varinfo -> t
+ (* [add_binding env lv vi] defines [vi] as the latest C binding for
+ [lv]. *)
+
val get: t -> logic_var -> varinfo
(* Return the latest C binding. *)
- val remove: t -> logic_var -> t
+ val remove: t -> logic_var -> unit
(* Remove the latest C binding. *)
+
end
val add_assert: t -> stmt -> predicate -> unit
@@ -111,10 +121,8 @@ val pop: t -> t
val transfer: from:t -> t -> t
(** Pop the last local context of [from] and push it into the other env. *)
-val get_generated_variables: t -> (varinfo * scope) list
-(** All the new variables local to the visited function.
- The boolean indicates whether the varinfo must be added to the outermost
- function block. *)
+val get_generated_variables: t -> (varinfo * localized_scope) list
+(** All the new variables local to the visited function. *)
val get_visitor: t -> Visitor.generic_frama_c_visitor
val get_behavior: t -> Cil.visitor_behavior
@@ -142,6 +150,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/gmpz.ml b/src/plugins/e-acsl/gmpz.ml
index ea9e81f9486f8b67d9f192df29f8b2ff47bbeade..54e5597f325b579cfd69968fdf0d4ee063b2fc64 100644
--- a/src/plugins/e-acsl/gmpz.ml
+++ b/src/plugins/e-acsl/gmpz.ml
@@ -28,13 +28,34 @@ 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 is_t ty = Cil_datatype.Typ.equal ty (t ())
+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 ()) || Cil_datatype.Typ.equal ty (t_ptr ())
let apply_on_var ~loc funname e = Misc.mk_call ~loc ("__gmpz_" ^ funname) [ e ]
let init ~loc e = apply_on_var "init" ~loc e
@@ -106,6 +127,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 503d9887391538af619d68add5c8f95da59f680f..4f1f25f47e3ff9378a89c8a3f03097b220e68c54 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/headers/header_spec.txt b/src/plugins/e-acsl/headers/header_spec.txt
index f6631bcaad981754bfeeb152348a57f562f71451..d1e50bebe74c088da2b7f6050b02021d859661b0 100644
--- a/src/plugins/e-acsl/headers/header_spec.txt
+++ b/src/plugins/e-acsl/headers/header_spec.txt
@@ -39,6 +39,8 @@ literal_strings.ml: CEA_LGPL_OR_PROPRIETARY.E_ACSL
literal_strings.mli: CEA_LGPL_OR_PROPRIETARY.E_ACSL
local_config.ml: .ignore
local_config.mli: CEA_LGPL_OR_PROPRIETARY.E_ACSL
+logic_functions.ml: CEA_LGPL_OR_PROPRIETARY.E_ACSL
+logic_functions.mli: CEA_LGPL_OR_PROPRIETARY.E_ACSL
loops.ml: CEA_LGPL_OR_PROPRIETARY.E_ACSL
loops.mli: CEA_LGPL_OR_PROPRIETARY.E_ACSL
lscope.ml: CEA_LGPL_OR_PROPRIETARY.E_ACSL
diff --git a/src/plugins/e-acsl/interval.ml b/src/plugins/e-acsl/interval.ml
index e2186708be58fcaa74693a8db9bbf956aaeafbca..0332ee10c8f66dd52fed572a6260a86dcc72ddd5 100644
--- a/src/plugins/e-acsl/interval.ml
+++ b/src/plugins/e-acsl/interval.ml
@@ -25,16 +25,24 @@ open Cil_types
(* Implement Figure 3 of J. Signoles' JFLA'15 paper "Rester statique pour
devenir plus rapide, plus précis et plus mince". *)
-exception Not_an_integer
-
(* ********************************************************************* *)
(* Basic datatypes and operations *)
(* ********************************************************************* *)
+exception Not_an_integer
+
(* constructors *)
let singleton_of_int n = Ival.inject_singleton (Integer.of_int n)
+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 *)
+ lazy
+ (Ival.inject_range
+ (Some Integer.zero)
+ (Some (Bit_utils.max_byte_address ())))
+
let rec interv_of_typ ty = match Cil.unrollType ty with
| TInt (k,_) as ty ->
let n = Cil.bitsSizeOf ty in
@@ -47,22 +55,118 @@ let rec interv_of_typ ty = match Cil.unrollType ty with
| _ ->
raise Not_an_integer
-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 *)
- lazy
- (Ival.inject_range (Some Integer.zero) (Some (Bit_utils.max_byte_address ())))
+let interv_of_logic_typ = function
+ | Ctype ty -> interv_of_typ ty
+ | Linteger -> Ival.inject_range None None
+ | Ltype _ -> Error.not_yet "user-defined logic type"
+ | Lvar _ -> Error.not_yet "type variable"
+ | Lreal -> Error.not_yet "real number"
+ | Larrow _ -> Error.not_yet "functional type"
-(* imperative environments *)
+let ikind_of_interv 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 *)
+ let kind = if Cil.intTypeIncluded lkind ukind then ukind else lkind in
+ (* convert the kind to [IInt] whenever smaller. *)
+ if Cil.intTypeIncluded kind IInt then IInt else kind
+ | None, None -> raise Cil.Not_representable (* GMP *)
+ | None, Some _ | Some _, None ->
+ Kernel.fatal ~current:true "ival: %a" Ival.pretty i
-module Env = struct
+(* Imperative environments *)
+module rec Env: sig
+ val clear: unit -> unit
+ val add: Cil_types.logic_var -> Ival.t -> unit
+ val find: Cil_types.logic_var -> Ival.t
+ val remove: Cil_types.logic_var -> unit
+ val replace: Cil_types.logic_var -> Ival.t -> unit
+end = struct
open Cil_datatype
let tbl: Ival.t Logic_var.Hashtbl.t = Logic_var.Hashtbl.create 7
- let clear () = Logic_var.Hashtbl.clear tbl
+
let add = Logic_var.Hashtbl.add tbl
let remove = Logic_var.Hashtbl.remove tbl
let replace = Logic_var.Hashtbl.replace tbl
let find = Logic_var.Hashtbl.find tbl
+
+ let clear () =
+ Logic_var.Hashtbl.clear tbl;
+ Logic_function_env.clear ()
+
+end
+
+(* Environment for handling recursive logic functions *)
+and Logic_function_env: sig
+ val widen: infer:(term -> Ival.t) -> term -> Ival.t -> bool * Ival.t
+ val clear: unit -> unit
+end = struct
+
+ module Profile =
+ Datatype.List_with_collections
+ (Ival)
+ (struct
+ let module_name = "E_ACSL.Interval.Logic_function_env.Profile"
+ end)
+
+ module LF =
+ Datatype.Pair_with_collections
+ (Datatype.String)
+ (Profile)
+ (struct
+ let module_name = "E_ACSL.Interval.Logic_function_env.LF"
+ end)
+
+ let tbl = LF.Hashtbl.create 7
+
+ let clear () = LF.Hashtbl.clear tbl
+
+ let interv_of_typ_containing_interv i =
+ try
+ let kind = ikind_of_interv i in
+ interv_of_typ (TInt(kind, []))
+ with Cil.Not_representable ->
+ (* infinity *)
+ Ival.inject_range None None
+
+ let extract_profile ~infer t = match t.term_node with
+ | Tapp(li, _, args) ->
+ li.l_var_info.lv_name,
+ List.map2
+ (fun param arg ->
+ try
+ let i = infer arg in
+ (* over-approximation of the interval to reach the fixpoint
+ faster, and to generate fewer specialized functions *)
+ let larger_i = interv_of_typ_containing_interv i in
+ Env.add param larger_i;
+ larger_i
+ with Not_an_integer ->
+ (* no need to add [param] to the environment *)
+ Ival.bottom)
+ li.l_profile
+ args
+ | _ ->
+ assert false
+
+ let widen ~infer t i =
+ let p = extract_profile ~infer t in
+ try
+ let old_i = LF.Hashtbl.find tbl p in
+ if Ival.is_included i old_i then true, old_i
+ else begin
+ let j = Ival.join i old_i in
+ LF.Hashtbl.replace tbl p j;
+ false, j
+ end
+ with Not_found ->
+ LF.Hashtbl.add tbl p i;
+ false, i
+
end
(* ********************************************************************* *)
@@ -183,11 +287,28 @@ let rec infer t =
Ival.meet i1 i2
| 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 (Ctype ty) -> interv_of_typ ty
- | Some _ -> raise Not_an_integer)
+ (match li.l_body with
+ | LBpred _ ->
+ Ival.zero_or_one
+ | LBterm t' ->
+ let rec fixpoint i =
+ let is_included, new_i = Logic_function_env.widen ~infer t i in
+ if is_included then begin
+ List.iter (fun lv -> Env.remove lv) li.l_profile;
+ new_i
+ end else
+ let i = infer t' in
+ List.iter (fun lv -> Env.remove lv) li.l_profile;
+ fixpoint i
+ in
+ fixpoint Ival.bottom
+ | LBnone
+ | LBreads _ ->
+ (match li.l_type with
+ | None -> assert false
+ | Some ret_type -> interv_of_logic_typ ret_type)
+ | LBinductive _ ->
+ Error.not_yet "logic functions inductively defined")
| Tunion _ -> Error.not_yet "tset union"
| Tinter _ -> Error.not_yet "tset intersection"
| Tcomprehension (_,_,_) -> Error.not_yet "tset comprehension"
@@ -230,7 +351,18 @@ and infer_term_lval (host, offset as tlv) =
and infer_term_host = function
| 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
diff --git a/src/plugins/e-acsl/interval.mli b/src/plugins/e-acsl/interval.mli
index 0a1e07d7b7845b5cb3305271bd22b74c452e3ffe..79ed83499b5327cba1d3e522657666de819079a7 100644
--- a/src/plugins/e-acsl/interval.mli
+++ b/src/plugins/e-acsl/interval.mli
@@ -52,6 +52,11 @@
exception Not_an_integer
+val ikind_of_interv: Ival.t -> Cil_types.ikind
+(** @return the smallest ikind that contains the given interval.
+ @raise Cil.Not_representable if the given interval does not fit into any C
+ integral type. *)
+
val interv_of_typ: Cil_types.typ -> Ival.t
(** @return the smallest interval which contains the given C type.
@raise Not_an_integer if the given type is not an integral type. *)
diff --git a/src/plugins/e-acsl/keep_status.ml b/src/plugins/e-acsl/keep_status.ml
index 69da42233489b929b8025a7f71693ced59b58002..cb76ec3fcc5a2f673d3a6b2a63ca37dca8ab2635 100644
--- a/src/plugins/e-acsl/keep_status.ml
+++ b/src/plugins/e-acsl/keep_status.ml
@@ -131,6 +131,7 @@ let must_translate kf kind =
duplicate by [Dup_function] but they are still associated to the original
function here *)
let name = Functions.RTL.get_original_name kf in
+ try
let info =
try Datatype.String.Hashtbl.find keep_status name
with Not_found ->
@@ -148,3 +149,4 @@ let must_translate kf kind =
pretty_kind kind
pretty_kind kind';
keep
+ with Not_found -> true
diff --git a/src/plugins/e-acsl/logic_functions.ml b/src/plugins/e-acsl/logic_functions.ml
new file mode 100644
index 0000000000000000000000000000000000000000..8955a154b2531cbb01d60aacf7ddb4b1dacdaf82
--- /dev/null
+++ b/src/plugins/e-acsl/logic_functions.ml
@@ -0,0 +1,344 @@
+(**************************************************************************)
+(* *)
+(* This file is part of the Frama-C's E-ACSL plug-in. *)
+(* *)
+(* Copyright (C) 2012-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
+open Cil_datatype
+
+(**************************************************************************)
+(********************** Forward references ********************************)
+(**************************************************************************)
+
+let named_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"
+
+(*****************************************************************************)
+(************************** Auxiliary functions* ****************************)
+(*****************************************************************************)
+
+(* @return true iff the result of the function is provided by reference as the
+ first extra argument at each call *)
+let result_as_extra_argument = Gmpz.is_t
+(* TODO: to be extended to any compound type? E.g. returning a struct is not
+ good practice... *)
+
+(*****************************************************************************)
+(****************** Generation of function bodies ****************************)
+(*****************************************************************************)
+
+(* Generate the block of code containing the statement assigning [e] to [ret_vi]
+ (the result). *)
+let generate_return_block ~loc env ret_vi e = match e.enode with
+ | Lval (Var _, NoOffset) ->
+ (* the returned value is a variable: Cil invariant preserved;
+ no need of [ret_vi] *)
+ let return_retres = Cil.mkStmt ~valid_sid:true (Return (Some e, loc)) in
+ let b, env =
+ Env.pop_and_get env return_retres ~global_clear:false Env.After
+ in
+ b.blocals <- b.blocals;
+ b.bscoping <- true;
+ b, env
+ | _ ->
+ (* the returned value is _not_ a variable: restore the invariant *)
+ let init = AssignInit (SingleInit e) in
+ let set =
+ Cil.mkStmtOneInstr ~valid_sid:true (Local_init (ret_vi, init, loc))
+ in
+ let return =
+ Cil.mkStmt ~valid_sid:true (Return (Some (Cil.evar ~loc ret_vi), loc))
+ in
+ let b, env = Env.pop_and_get env set ~global_clear:false Env.Middle in
+ ret_vi.vdefined <- true;
+ b.blocals <- ret_vi :: b.blocals;
+ b.bstmts <- b.bstmts @ [ return ];
+ b.bscoping <- true;
+ b, env
+
+(* Generate the function's body for predicates. *)
+let pred_to_block ~loc kf env ret_vi p =
+ Typing.type_named_predicate ~must_clear:false p;
+ let e, env = !named_predicate_to_exp_ref kf env p in
+ (* for predicate, since the result is either 0 or 1, return it directly (it
+ cannot be provided as extra argument *)
+ generate_return_block ~loc env ret_vi e
+
+(* Generate the function's body for terms. *)
+let term_to_block ~loc kf env ret_ty ret_vi t =
+ Typing.type_term ~use_gmp_opt:false ~ctx:(Typing.integer_ty_of_typ ret_ty) t;
+ let e, env = !term_to_exp_ref kf env t in
+ if Cil.isVoidType ret_ty then
+ (* if the function's result is a GMP, it is the first parameter of the
+ function (by reference). *)
+ let set =
+ let lv_star_ret = Cil.mkMem ~addr:(Cil.evar ~loc ret_vi) ~off:NoOffset in
+ let star_ret = Cil.new_exp ~loc (Lval lv_star_ret) in
+ Gmpz.init_set ~loc lv_star_ret star_ret e
+ in
+ let return_void = Cil.mkStmt ~valid_sid:true (Return (None, loc)) in
+ let b, env = Env.pop_and_get env set ~global_clear:false Env.Middle in
+ b.bstmts <- b.bstmts @ [ return_void ];
+ b.bscoping <- true;
+ b, env
+ else
+ generate_return_block ~loc env ret_vi e
+
+let generate_body ~loc kf env ret_ty ret_vi = function
+ | LBnone | LBreads _ ->
+ Options.abort
+ "logic function or predicate without explicit definition are not part of \
+ E-ACSL"
+ | LBterm t -> term_to_block ~loc kf env ret_ty ret_vi t
+ | LBpred p -> pred_to_block ~loc kf env ret_vi p
+ | LBinductive _ -> Error.not_yet "inductive definition"
+
+(* Generate a kernel function from a given logic info [li] *)
+let generate_kf ~loc fname env ret_ty params_ty li =
+ (* build the formal parameters *)
+ let params, params_ty =
+ List.fold_right2
+ (fun lvi pty (params, params_ty) ->
+ let ty = match pty with
+ | Typing.Gmp ->
+ (* GMP's integer are arrays: consider them as pointers in function's
+ parameters *)
+ Gmpz.t_ptr ()
+ | Typing.C_type ik -> TInt(ik, [])
+ | Typing.Other -> Typing.typ_of_lty lvi.lv_type
+ in
+ (* build the formals: cannot use [Cil.makeFormal] since the function
+ does not yet exist *)
+ let vi = Cil.makeVarinfo false true lvi.lv_name ty in
+ vi :: params, (lvi.lv_name, ty, []) :: params_ty)
+ li.l_profile
+ params_ty
+ ([], [])
+ in
+ (* build the varinfo storing the result *)
+ let ret_vi, ret_ty, params_with_ret, params_ty_with_ret =
+ let vname = "__retres" in
+ if result_as_extra_argument ret_ty then
+ let ret_ty_ptr = TPtr(ret_ty, []) (* call by reference *) in
+ let vname = vname ^ "_arg" in
+ let vi = Cil.makeVarinfo false true vname ret_ty_ptr in
+ vi, Cil.voidType, vi :: params, (vname, ret_ty_ptr, []) :: params_ty
+ else
+ Cil.makeVarinfo false false vname ret_ty, ret_ty, params, params_ty
+ in
+ (* build the function's varinfo *)
+ let vi =
+ Cil.makeGlobalVar
+ fname
+ (TFun
+ (ret_ty,
+ Some params_ty_with_ret,
+ false,
+ li.l_var_info.lv_attr))
+ in
+ vi.vdefined <- true;
+ (* create the fundec *)
+ let fundec =
+ { svar = vi;
+ sformals = params_with_ret;
+ slocals = []; (* filled later to break mutual dependencies between
+ creating this list and creating the kf *)
+ smaxid = 0;
+ sbody = Cil.mkBlock []; (* filled later; same as above *)
+ smaxstmtid = None;
+ sallstmts = [];
+ sspec = Cil.empty_funspec () }
+ in
+ Cil.setMaxId fundec;
+ let spec = Cil.empty_funspec () in
+ Queue.add
+ (fun () -> Globals.Functions.replace_by_definition spec fundec loc)
+ (Env.get_visitor env)#get_filling_actions;
+ (* create the kernel function itself *)
+ let kf = { fundec = Definition(fundec, loc); spec } in
+ (* closure generating the function's body.
+ Delay its generation after filling the memoisation table (for termination
+ of recursive function calls) *)
+ let gen_body () =
+ let env = Env.push env in
+ let old_kf = Extlib.the (Env.current_kf env) in
+ Env.set_current_kf env kf;
+ (* fill the typing environment with the function's parameters
+ before generating the code (code generation invokes typing) *)
+ let env =
+ let add env lvi vi =
+ (match vi.vtype with
+ | TInt _ as ty -> Interval.Env.add lvi (Interval.interv_of_typ ty)
+ | ty ->
+ if Gmpz.is_t ty then
+ Interval.Env.add lvi (Ival.inject_range None None));
+ Env.Logic_binding.add_binding env lvi vi
+ in
+ List.fold_left2 add env li.l_profile params
+ in
+ let b, env = generate_body ~loc kf env ret_ty ret_vi li.l_body in
+ fundec.sbody <- b;
+ (* add the generated variables in the necessary lists *)
+ (* TODO: factorized the code below that add the generated vars with method
+ [add_generated_variables_in_function] in the main visitor *)
+ let vars =
+ let l = Env.get_generated_variables env in
+ if ret_vi.vdefined then (ret_vi, Env.LFunction kf) :: l else l
+ in
+ let locals, blocks =
+ List.fold_left
+ (fun (local_vars, block_vars as acc) (v, scope) -> match scope with
+ | Env.LFunction kf' when Kernel_function.equal kf kf' ->
+ v :: local_vars, block_vars
+ | Env.LLocal_block kf' when Kernel_function.equal kf kf' ->
+ v :: local_vars, block_vars
+ | _ -> acc)
+ (fundec.slocals, fundec.sbody.blocals)
+ vars
+ in
+ fundec.slocals <- locals;
+ fundec.sbody.blocals <- blocks;
+ List.iter
+ (fun lvi ->
+ Interval.Env.remove lvi;
+ ignore (Env.Logic_binding.remove env lvi))
+ li.l_profile;
+ Env.set_current_kf
+ env
+ (Cil.get_original_kernel_function (Env.get_behavior env) old_kf)
+ in
+ vi, kf, gen_body
+
+(**************************************************************************)
+(***************************** Memoization ********************************)
+(**************************************************************************)
+
+module Params_ty =
+ Datatype.List_with_collections
+ (Typing.Datatype)
+ (struct let module_name = "E_ACSL.Logic_functions.Params_ty" end)
+
+(* for each logic_info, associate its possible profiles, i.e. the types of its
+ parameters + the generated varinfo for the function *)
+let memo_tbl:
+ kernel_function Params_ty.Hashtbl.t Logic_info.Hashtbl.t
+ = Logic_info.Hashtbl.create 7
+
+let reset () = Logic_info.Hashtbl.clear memo_tbl
+
+let add_generated_functions globals =
+ let rec aux acc = function
+ | [] ->
+ acc
+ | GAnnot(Dfun_or_pred(li, loc), _) as g :: l ->
+ let acc = g :: acc in
+ (try
+ (* add the declarations close to its corresponding logic function or
+ predicate *)
+ let params = Logic_info.Hashtbl.find memo_tbl li in
+ let add_fundecl kf acc =
+ GFunDecl(Cil.empty_funspec (), Kernel_function.get_vi kf, loc)
+ :: acc
+ in
+ aux (Params_ty.Hashtbl.fold (fun _ -> add_fundecl) params acc) l
+ with Not_found ->
+ aux acc l)
+ | g :: l ->
+ aux (g :: acc) l
+ in
+ let rev_globals = aux [] globals in
+ (* add the definitions at the end of [globals] *)
+ let add_fundec kf globals =
+ let fundec =
+ try Kernel_function.get_definition kf
+ with Kernel_function.No_Definition -> assert false
+ in
+ GFun(fundec, Location.unknown) :: globals
+ in
+ let rev_globals =
+ Logic_info.Hashtbl.fold
+ (fun _ -> Params_ty.Hashtbl.fold (fun _ -> add_fundec))
+ memo_tbl
+ rev_globals
+ in
+ List.rev rev_globals
+
+let tapp_to_exp ~loc fname env t li params_ty args =
+ let ret_ty = Typing.get_typ t in
+ let gen tbl =
+ let vi, kf, gen_body = generate_kf fname ~loc env ret_ty params_ty li in
+ Params_ty.Hashtbl.add tbl params_ty kf;
+ vi, gen_body
+ in
+ (* memoise the function's varinfo *)
+ let fvi, gen_body =
+ try
+ let h = Logic_info.Hashtbl.find memo_tbl li in
+ try
+ let kf = Params_ty.Hashtbl.find h params_ty in
+ Kernel_function.get_vi kf,
+ (fun () -> ()) (* body generation already planified *)
+ with Not_found -> gen h
+ with Not_found ->
+ let h = Params_ty.Hashtbl.create 7 in
+ Logic_info.Hashtbl.add memo_tbl li h;
+ gen h
+ in
+ (* the generation of the function body must be performed after memoizing the
+ kernel function in order to handle recursive calls in finite time :-) *)
+ gen_body ();
+ (* create the function call for the tapp *)
+ let mkcall vi =
+ let mk_args types args =
+ match types (* generated by E-ACSL: no need to unroll *) with
+ | TFun(_, Some params, _, _) ->
+ (* additional casts are necessary whenever the argument is GMP and the
+ parameter is a (small) integralType: after handling the context in
+ [Translate] through [add_cast], the GMP has been translated into a
+ [long] (that is what provided the GMP API). This [long] must now be
+ translated to the parameter's type. It cannot be done before since
+ the exact type of the parameter is only computed when the function is
+ generated *)
+ List.map2
+ (fun (_, newt, _) e -> Cil.mkCast ~force:false ~newt ~e)
+ params
+ args
+ | _ -> assert false
+ in
+ if result_as_extra_argument ret_ty then
+ let args = mk_args fvi.vtype (Cil.mkAddrOf ~loc (Cil.var vi) :: args) in
+ Call(None, Cil.evar fvi, args, loc)
+ else
+ let args = mk_args fvi.vtype args in
+ Call(Some (Cil.var vi), Cil.evar fvi, args, loc)
+ in
+ (* generate the varinfo storing the result of the call *)
+ Env.new_var
+ ~loc
+ ~name:li.l_var_info.lv_name
+ env
+ (Some t)
+ ret_ty
+ (fun vi _ -> [ Cil.mkStmtOneInstr ~valid_sid:true (mkcall vi) ])
diff --git a/src/plugins/e-acsl/logic_functions.mli b/src/plugins/e-acsl/logic_functions.mli
new file mode 100644
index 0000000000000000000000000000000000000000..3e2c0d25c90e0714ad4fa660be492725c12359c8
--- /dev/null
+++ b/src/plugins/e-acsl/logic_functions.mli
@@ -0,0 +1,56 @@
+(**************************************************************************)
+(* *)
+(* This file is part of the Frama-C's E-ACSL plug-in. *)
+(* *)
+(* Copyright (C) 2012-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 reset: unit -> unit
+
+val tapp_to_exp:
+ loc:location ->
+ string -> Env.t -> term -> logic_info -> Typing.integer_ty list -> exp list ->
+ varinfo * exp * Env.t
+
+val add_generated_functions: global list -> global list
+(* @return the input list of globals in which the generated functions have been
+ inserted at the right places (both their declaration and their definition) *)
+
+(**************************************************************************)
+(********************** Forward references ********************************)
+(**************************************************************************)
+
+val named_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
diff --git a/src/plugins/e-acsl/loops.ml b/src/plugins/e-acsl/loops.ml
index ea01ce00c635171832c265e10c6286b52b686d36..a6da567257aefb138decb63d0fcbdd37cf3ded15 100644
--- a/src/plugins/e-acsl/loops.ml
+++ b/src/plugins/e-acsl/loops.ml
@@ -297,7 +297,7 @@ let rec mk_nested_loops ~loc mk_innermost_block kf env lscope_vars =
Some break_stmt))
in
(* remove logic binding before returning *)
- let env = Env.Logic_binding.remove env logic_x in
+ Env.Logic_binding.remove env logic_x;
[ start ; stmt ], env
| Lscope.Lvs_let(lv, t) :: lscope_vars' ->
let ty = Typing.get_typ t in
@@ -308,7 +308,7 @@ let rec mk_nested_loops ~loc mk_innermost_block kf env lscope_vars =
mk_nested_loops ~loc mk_innermost_block kf env lscope_vars'
in
(* remove logic binding now that the block is constructed *)
- let env = Env.Logic_binding.remove env lv in
+ Env.Logic_binding.remove env lv;
(* return *)
let_stmt :: stmts, env
| Lscope.Lvs_formal _ :: _ ->
diff --git a/src/plugins/e-acsl/misc.mli b/src/plugins/e-acsl/misc.mli
index 8f12597aa044599b664b993210e6b3d46b9bc53a..3fd7f4c409ccb25804d2f907a0c080be88d81673 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,31 @@ 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 *)
(*
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 15637955c83af4061c768c1c2e6d89f38d503997..827a26321492b61e202620b8b9a693ee43c628ba 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 bfc158802d840c137876975f13346e34b5a2db15..79a76e5072ff36d4a82c3117a1502245997c1ce1 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 72731f940f00df5cf7fccaa6f458428c7b854c64..61c88433a84b1f2c0017dcf6b44e3cf8e7a45164 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 0000000000000000000000000000000000000000..80f796bad6a411b8a1b6a62cec3b07e2d481e244
--- /dev/null
+++ b/src/plugins/e-acsl/tests/gmp/functions.c
@@ -0,0 +1,72 @@
+/* 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 clauses 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);
+
+ // not yet supported
+ /* double d = 2.0; */
+ /* /\*@ assert f2(d) > 0; *\/ ; */
+ /* /\*@ assert p_notyet(27); *\/ ; */
+ /* /\*@ assert f_notyet(27) == 27; *\/ ; */
+}
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 0000000000000000000000000000000000000000..382a1a64b9ef6fd97bc358a2ca031e1238d32935
--- /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 0000000000000000000000000000000000000000..76c60912194b4481bc8e6f06bb94b8f522b6a2d4
--- /dev/null
+++ b/src/plugins/e-acsl/tests/gmp/functions_rec.c
@@ -0,0 +1,31 @@
+/* run.config
+ COMMENT: recursive logic functions
+ STDOPT: +"-eva-ignore-recursive-calls"
+*/
+
+/*@ 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; */ ;
+}
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 0000000000000000000000000000000000000000..b922d39b016f315e1b7441fce2762b8fc579c1b4
--- /dev/null
+++ b/src/plugins/e-acsl/tests/gmp/oracle/functions.0.res.oracle
@@ -0,0 +1,31 @@
+[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]
+ glob ∈ {5}
+ __e_acsl_sound_verdict ∈ [--..--]
+[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_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] using specification for function __gmpz_init_set
+[eva:alarm] tests/gmp/functions.c:48: Warning:
+ function __e_acsl_assert: precondition got status unknown.
+[eva:alarm] tests/gmp/functions.c:49: Warning:
+ function __e_acsl_assert: precondition got status unknown.
+[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 0000000000000000000000000000000000000000..6a88f942fbca56a062bb6516e4b0a01940d1817c
--- /dev/null
+++ b/src/plugins/e-acsl/tests/gmp/oracle/functions.1.res.oracle
@@ -0,0 +1,50 @@
+[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]
+ glob ∈ {5}
+ __e_acsl_sound_verdict ∈ [--..--]
+[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:alarm] tests/gmp/functions.c:44: Warning:
+ function __e_acsl_assert: precondition got status unknown.
+[eva] using specification for function __gmpz_init_set
+[eva:alarm] tests/gmp/functions.c:46: Warning:
+ function __e_acsl_assert: precondition got status unknown.
+[eva:alarm] tests/gmp/functions.c:47: Warning:
+ accessing uninitialized left-value.
+ assert \initialized((__e_acsl_mpz_struct *)__gen_e_acsl_f1_4);
+[eva:alarm] tests/gmp/functions.c:47: Warning:
+ function __e_acsl_assert: precondition got status unknown.
+[eva:alarm] tests/gmp/functions.c:48: Warning:
+ function __e_acsl_assert: precondition got status unknown.
+[eva:alarm] tests/gmp/functions.c:49: Warning:
+ function __e_acsl_assert: precondition got status unknown.
+[eva:alarm] tests/gmp/functions.c:53: Warning:
+ function __e_acsl_assert: precondition got status unknown.
+[eva:alarm] tests/gmp/functions.c:56: Warning:
+ function __e_acsl_assert: precondition got status unknown.
+[eva:alarm] tests/gmp/functions.c:58: Warning:
+ function __e_acsl_assert: precondition got status unknown.
+[eva:alarm] tests/gmp/functions.c:63: Warning:
+ function __e_acsl_assert: precondition got status unknown.
+[eva:alarm] tests/gmp/functions.c:25: Warning:
+ function __e_acsl_assert: precondition got status unknown.
+[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 0000000000000000000000000000000000000000..c46fcfd437fbe80229820a34f46cab9345c29b1e
--- /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 0000000000000000000000000000000000000000..c46fcfd437fbe80229820a34f46cab9345c29b1e
--- /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 0000000000000000000000000000000000000000..cbf74d13ac79e1568bba0f82bc91e82493871cf4
--- /dev/null
+++ b/src/plugins/e-acsl/tests/gmp/oracle/functions_rec.0.res.oracle
@@ -0,0 +1,87 @@
+[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:26:
+ cannot evaluate ACSL term, unsupported ACSL construct: logic function f2
+[eva:alarm] tests/gmp/functions_rec.c:26: Warning: assertion got status unknown.
+[eva] tests/gmp/functions_rec.c:10: Warning:
+ recursive call during value analysis
+ of __gen_e_acsl_f2_2 (__gen_e_acsl_f2_2 <- __gen_e_acsl_f2_2 :: tests/gmp/functions_rec.c:10 <-
+ __gen_e_acsl_f2 :: tests/gmp/functions_rec.c:26 <-
+ main).
+ Assuming the call has no effect. The analysis will be unsound.
+[eva] using specification for function __gen_e_acsl_f2_2
+[eva] tests/gmp/functions_rec.c:10: Warning:
+ recursive call during value analysis
+ of __gen_e_acsl_f2_2 (__gen_e_acsl_f2_2 <- __gen_e_acsl_f2_2 :: tests/gmp/functions_rec.c:10 <-
+ __gen_e_acsl_f2 :: tests/gmp/functions_rec.c:26 <-
+ main).
+ Assuming the call has no effect. The analysis will be unsound.
+[eva] tests/gmp/functions_rec.c:10: Warning:
+ recursive call during value analysis
+ of __gen_e_acsl_f2_2 (__gen_e_acsl_f2_2 <- __gen_e_acsl_f2_2 :: tests/gmp/functions_rec.c:10 <-
+ __gen_e_acsl_f2 :: tests/gmp/functions_rec.c:26 <-
+ main).
+ Assuming the call has no effect. The analysis will be unsound.
+[eva] using specification for function __e_acsl_assert
+[eva:alarm] tests/gmp/functions_rec.c:10: Warning:
+ function __e_acsl_assert: precondition got status unknown.
+[eva:alarm] tests/gmp/functions_rec.c:10: Warning:
+ division by zero. assert __gen_e_acsl_f2_8 ≢ 0;
+[eva:alarm] tests/gmp/functions_rec.c:10: Warning:
+ signed overflow.
+ assert -2147483648 ≤ __gen_e_acsl_f2_4 * __gen_e_acsl_f2_6;
+[eva:alarm] tests/gmp/functions_rec.c:10: Warning:
+ signed overflow. assert __gen_e_acsl_f2_4 * __gen_e_acsl_f2_6 ≤ 2147483647;
+[eva:alarm] tests/gmp/functions_rec.c:10: Warning:
+ signed overflow.
+ assert
+ (int)(__gen_e_acsl_f2_4 * __gen_e_acsl_f2_6) / __gen_e_acsl_f2_8 ≤
+ 2147483647;
+[eva:alarm] tests/gmp/functions_rec.c:10: Warning:
+ division by zero. assert __gen_e_acsl_f2_13 ≢ 0;
+[eva:alarm] tests/gmp/functions_rec.c:10: Warning:
+ signed overflow.
+ assert -2147483648 ≤ __gen_e_acsl_f2_9 * __gen_e_acsl_f2_11;
+[eva:alarm] tests/gmp/functions_rec.c:10: Warning:
+ signed overflow.
+ assert __gen_e_acsl_f2_9 * __gen_e_acsl_f2_11 ≤ 2147483647;
+[eva:alarm] tests/gmp/functions_rec.c:10: Warning:
+ signed overflow.
+ assert
+ (int)(__gen_e_acsl_f2_9 * __gen_e_acsl_f2_11) / __gen_e_acsl_f2_13 ≤
+ 2147483647;
+[eva:alarm] tests/gmp/functions_rec.c:26: Warning:
+ function __e_acsl_assert: precondition got status unknown.
+[eva] tests/gmp/functions_rec.c:28:
+ cannot evaluate ACSL term, unsupported ACSL construct: logic function f3
+[eva:alarm] tests/gmp/functions_rec.c:28: Warning: assertion got status unknown.
+[eva] tests/gmp/functions_rec.c:14: Warning:
+ recursive call during value analysis
+ of __gen_e_acsl_f3_2 (__gen_e_acsl_f3_2 <- __gen_e_acsl_f3_2 :: tests/gmp/functions_rec.c:14 <-
+ __gen_e_acsl_f3 :: tests/gmp/functions_rec.c:28 <-
+ main).
+ Assuming the call has no effect. The analysis will be unsound.
+[eva] using specification for function __gen_e_acsl_f3_2
+[eva] tests/gmp/functions_rec.c:30:
+ cannot evaluate ACSL term, unsupported ACSL construct: logic function f4
+[eva:alarm] tests/gmp/functions_rec.c:30: Warning: assertion got status unknown.
+[eva] tests/gmp/functions_rec.c:17: Warning:
+ recursive call during value analysis
+ of __gen_e_acsl_f4_2 (__gen_e_acsl_f4_2 <- __gen_e_acsl_f4_2 :: tests/gmp/functions_rec.c:17 <-
+ __gen_e_acsl_f4 :: tests/gmp/functions_rec.c:30 <-
+ main).
+ Assuming the call has no effect. The analysis will be unsound.
+[eva] using specification for function __gen_e_acsl_f4_2
+[eva:alarm] tests/gmp/functions_rec.c:30: Warning:
+ function __e_acsl_assert: precondition got status unknown.
+[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 0000000000000000000000000000000000000000..ad15ac476ccad3eb4c1c7c322456de28b5dc3c3f
--- /dev/null
+++ b/src/plugins/e-acsl/tests/gmp/oracle/functions_rec.1.res.oracle
@@ -0,0 +1,116 @@
+[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:26:
+ cannot evaluate ACSL term, unsupported ACSL construct: logic function f2
+[eva:alarm] tests/gmp/functions_rec.c:26: Warning: assertion got status unknown.
+[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_init
+[eva] using specification for function __gmpz_sub
+[eva:alarm] tests/gmp/functions_rec.c:10: Warning:
+ accessing uninitialized left-value.
+ assert \initialized((__e_acsl_mpz_struct *)__gen_e_acsl_sub);
+[eva] tests/gmp/functions_rec.c:10: Warning:
+ recursive call during value analysis
+ of __gen_e_acsl_f2_2 (__gen_e_acsl_f2_2 <- __gen_e_acsl_f2_2 :: tests/gmp/functions_rec.c:10 <-
+ __gen_e_acsl_f2 :: tests/gmp/functions_rec.c:26 <-
+ main).
+ Assuming the call has no effect. The analysis will be unsound.
+[eva:alarm] tests/gmp/functions_rec.c:10: Warning:
+ accessing uninitialized left-value.
+ assert \initialized((__e_acsl_mpz_struct *)__gen_e_acsl_sub_2);
+[eva] using specification for function __gen_e_acsl_f2_2
+[eva] tests/gmp/functions_rec.c:10: Warning:
+ recursive call during value analysis
+ of __gen_e_acsl_f2_2 (__gen_e_acsl_f2_2 <- __gen_e_acsl_f2_2 :: tests/gmp/functions_rec.c:10 <-
+ __gen_e_acsl_f2 :: tests/gmp/functions_rec.c:26 <-
+ main).
+ Assuming the call has no effect. The analysis will be unsound.
+[eva:alarm] tests/gmp/functions_rec.c:10: Warning:
+ accessing uninitialized left-value.
+ assert \initialized((__e_acsl_mpz_struct *)__gen_e_acsl_sub_3);
+[eva] using specification for function __gmpz_mul
+[eva] tests/gmp/functions_rec.c:10: Warning:
+ recursive call during value analysis
+ of __gen_e_acsl_f2_2 (__gen_e_acsl_f2_2 <- __gen_e_acsl_f2_2 :: tests/gmp/functions_rec.c:10 <-
+ __gen_e_acsl_f2 :: tests/gmp/functions_rec.c:26 <-
+ main).
+ Assuming the call has no effect. The analysis will be unsound.
+[eva:alarm] tests/gmp/functions_rec.c:10: Warning:
+ accessing uninitialized left-value.
+ assert \initialized((__e_acsl_mpz_struct *)__gen_e_acsl_sub_4);
+[eva] :0:
+ cannot evaluate ACSL term, unsupported ACSL construct: logic function f2
+[eva:alarm] tests/gmp/functions_rec.c:10: Warning:
+ assertion 'E_ACSL' got status unknown.
+[eva] using specification for function __e_acsl_assert
+[eva:alarm] tests/gmp/functions_rec.c:10: Warning:
+ function __e_acsl_assert: precondition got status unknown.
+[eva] using specification for function __gmpz_tdiv_q
+[eva:alarm] tests/gmp/functions_rec.c:10: Warning:
+ accessing uninitialized left-value.
+ assert \initialized((__e_acsl_mpz_struct *)__gen_e_acsl_sub_5);
+[eva:alarm] tests/gmp/functions_rec.c:10: Warning:
+ accessing uninitialized left-value.
+ assert \initialized((__e_acsl_mpz_struct *)__gen_e_acsl_sub_6);
+[eva:alarm] tests/gmp/functions_rec.c:26: Warning:
+ function __e_acsl_assert: precondition got status unknown.
+[eva] tests/gmp/functions_rec.c:28:
+ cannot evaluate ACSL term, unsupported ACSL construct: logic function f3
+[eva:alarm] tests/gmp/functions_rec.c:28: Warning: assertion got status unknown.
+[eva:alarm] tests/gmp/functions_rec.c:14: Warning:
+ accessing uninitialized left-value.
+ assert \initialized((__e_acsl_mpz_struct *)__gen_e_acsl_sub_7);
+[eva] using specification for function __gmpz_get_si
+[eva] tests/gmp/functions_rec.c:14: Warning:
+ recursive call during value analysis
+ of __gen_e_acsl_f3_2 (__gen_e_acsl_f3_2 <- __gen_e_acsl_f3_2 :: tests/gmp/functions_rec.c:14 <-
+ __gen_e_acsl_f3 :: tests/gmp/functions_rec.c:28 <-
+ main).
+ Assuming the call has no effect. The analysis will be unsound.
+[eva:alarm] tests/gmp/functions_rec.c:14: Warning:
+ accessing uninitialized left-value.
+ assert \initialized((__e_acsl_mpz_struct *)__gen_e_acsl_sub_8);
+[eva] using specification for function __gen_e_acsl_f3_2
+[eva] using specification for function __gmpz_add
+[eva:alarm] tests/gmp/functions_rec.c:14: Warning:
+ accessing uninitialized left-value.
+ assert \initialized((__e_acsl_mpz_struct *)__gen_e_acsl_add);
+[eva:alarm] tests/gmp/functions_rec.c:14: Warning:
+ accessing uninitialized left-value.
+ assert \initialized((__e_acsl_mpz_struct *)__gen_e_acsl_add_2);
+[eva] using specification for function __gmpz_neg
+[eva:alarm] tests/gmp/functions_rec.c:28: Warning:
+ function __e_acsl_assert: precondition got status unknown.
+[eva] tests/gmp/functions_rec.c:30:
+ cannot evaluate ACSL term, unsupported ACSL construct: logic function f4
+[eva:alarm] tests/gmp/functions_rec.c:30: Warning: assertion got status unknown.
+[eva:alarm] tests/gmp/functions_rec.c:17: Warning:
+ accessing uninitialized left-value.
+ assert \initialized((__e_acsl_mpz_struct *)__gen_e_acsl_add_3);
+[eva] tests/gmp/functions_rec.c:17: Warning:
+ recursive call during value analysis
+ of __gen_e_acsl_f4_2 (__gen_e_acsl_f4_2 <- __gen_e_acsl_f4_2 :: tests/gmp/functions_rec.c:17 <-
+ __gen_e_acsl_f4 :: tests/gmp/functions_rec.c:30 <-
+ main).
+ Assuming the call has no effect. The analysis will be unsound.
+[eva:alarm] tests/gmp/functions_rec.c:17: Warning:
+ accessing uninitialized left-value.
+ assert \initialized((__e_acsl_mpz_struct *)__gen_e_acsl_add_4);
+[eva] using specification for function __gen_e_acsl_f4_2
+[eva] using specification for function __gmpz_init_set_ui
+[eva:alarm] tests/gmp/functions_rec.c:30: Warning:
+ function __e_acsl_assert: precondition got status unknown.
+[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 0000000000000000000000000000000000000000..1bf6931b3419cd8216a32e4081f39286c417a3f3
--- /dev/null
+++ b/src/plugins/e-acsl/tests/gmp/oracle/gen_functions.c
@@ -0,0 +1,357 @@
+/* Generated by Frama-C */
+#include "stdio.h"
+#include "stdlib.h"
+extern int __e_acsl_sound_verdict;
+
+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 x, int y);
+
+/*@ predicate p2(ℤ x, ℤ y) = x + y > 0;
+
+*/
+int __gen_e_acsl_p2_3(int x, __e_acsl_mpz_struct * y);
+
+int __gen_e_acsl_p2_5(int x, long y);
+
+int __gen_e_acsl_p2(int x, int y);
+
+/*@ logic ℤ f1(ℤ x, ℤ y) = x + y;
+
+*/
+void __gen_e_acsl_f1_7(__e_acsl_mpz_t *__retres_arg, __e_acsl_mpz_struct * x,
+ __e_acsl_mpz_struct * y);
+
+void __gen_e_acsl_f1_5(__e_acsl_mpz_t *__retres_arg, int x,
+ __e_acsl_mpz_struct * y);
+
+long __gen_e_acsl_f1(int x, int y);
+
+/*@ logic char h_char(char c) = c;
+ */
+char __gen_e_acsl_h_char(int c);
+
+/*@ logic short h_short(short s) = s;
+ */
+short __gen_e_acsl_h_short(int s);
+
+/*@ logic int g_hidden(int x) = x;
+ */
+int __gen_e_acsl_g_hidden(int x);
+
+/*@ logic int g(int x) = g_hidden(x);
+ */
+int __gen_e_acsl_g(int x);
+
+/*@ logic mystruct t1(mystruct m) = m;
+ */
+mystruct __gen_e_acsl_t1(mystruct m);
+
+/*@ logic ℤ t2(mystruct m) = m.k + m.l;
+ */
+long __gen_e_acsl_t2(mystruct m);
+
+/*@ predicate k_pred(ℤ x) = x > 0;
+
+*/
+int __gen_e_acsl_k_pred(int x);
+
+/*@ 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);
+ */
+/*@ 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_2;
+ __gen_e_acsl_p1_2 = __gen_e_acsl_p1(x,y);
+ __e_acsl_assert(__gen_e_acsl_p1_2,(char *)"Assertion",(char *)"main",
+ (char *)"p1(x, y)",42);
+ }
+ /*@ assert p2(3, 4); */
+ {
+ int __gen_e_acsl_p2_2;
+ __gen_e_acsl_p2_2 = __gen_e_acsl_p2(3,4);
+ __e_acsl_assert(__gen_e_acsl_p2_2,(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_4;
+ __gmpz_init_set_str(__gen_e_acsl_,"99999999999999999999999999999",10);
+ __gen_e_acsl_p2_4 = __gen_e_acsl_p2_3(5,
+ (__e_acsl_mpz_struct *)__gen_e_acsl_);
+ __e_acsl_assert(__gen_e_acsl_p2_4,(char *)"Assertion",(char *)"main",
+ (char *)"p2(5, 99999999999999999999999999999)",44);
+ __gmpz_clear(__gen_e_acsl_);
+ }
+ /*@ assert f1(x, y) ≡ 3; */
+ {
+ long __gen_e_acsl_f1_2;
+ __gen_e_acsl_f1_2 = __gen_e_acsl_f1(x,y);
+ __e_acsl_assert(__gen_e_acsl_f1_2 == 3L,(char *)"Assertion",
+ (char *)"main",(char *)"f1(x, y) == 3",46);
+ }
+ /*@ assert p2(x, f1(3, 4)); */
+ {
+ long __gen_e_acsl_f1_4;
+ int __gen_e_acsl_p2_6;
+ __gen_e_acsl_f1_4 = __gen_e_acsl_f1(3,4);
+ __gen_e_acsl_p2_6 = __gen_e_acsl_p2_5(x,__gen_e_acsl_f1_4);
+ __e_acsl_assert(__gen_e_acsl_p2_6,(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_6;
+ __e_acsl_mpz_t __gen_e_acsl__5;
+ int __gen_e_acsl_gt_3;
+ __gmpz_init_set_str(__gen_e_acsl__4,"99999999999999999999999999999",10);
+ __gen_e_acsl_f1_5(& __gen_e_acsl_f1_6,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_6),
+ (__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_6);
+ __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_8;
+ __e_acsl_mpz_t __gen_e_acsl__7;
+ int __gen_e_acsl_eq;
+ __gmpz_init_set_str(__gen_e_acsl__6,"99999999999999999999999999999",10);
+ __gen_e_acsl_f1_7(& __gen_e_acsl_f1_8,
+ (__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_8),
+ (__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_8);
+ __gmpz_clear(__gen_e_acsl__7);
+ }
+ /*@ assert g(x) ≡ x; */
+ {
+ int __gen_e_acsl_g_2;
+ __gen_e_acsl_g_2 = __gen_e_acsl_g(x);
+ __e_acsl_assert(__gen_e_acsl_g_2 == 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_2;
+ __gen_e_acsl_h_char_2 = __gen_e_acsl_h_char((int)c);
+ __e_acsl_assert((int)__gen_e_acsl_h_char_2 == (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_2;
+ __gen_e_acsl_h_short_2 = __gen_e_acsl_h_short((int)s);
+ __e_acsl_assert((int)__gen_e_acsl_h_short_2 == (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_2;
+ long __gen_e_acsl_t2_2;
+ __gen_e_acsl_t1_2 = __gen_e_acsl_t1(m);
+ __gen_e_acsl_t2_2 = __gen_e_acsl_t2(__gen_e_acsl_t1_2);
+ __e_acsl_assert(__gen_e_acsl_t2_2 == 17L,(char *)"Assertion",
+ (char *)"main",(char *)"t2(t1(m)) == 17",63);
+ }
+ __gen_e_acsl_k(9);
+ __retres = 0;
+ return __retres;
+}
+
+/*@ requires k_pred(x); */
+void __gen_e_acsl_k(int x)
+{
+ {
+ int __gen_e_acsl_k_pred_2;
+ __gen_e_acsl_k_pred_2 = __gen_e_acsl_k_pred(x);
+ __e_acsl_assert(__gen_e_acsl_k_pred_2,(char *)"Precondition",(char *)"k",
+ (char *)"k_pred(x)",25);
+ }
+ k(x);
+ return;
+}
+
+char __gen_e_acsl_h_char(int c)
+{
+ char __retres = (char)c;
+ return __retres;
+}
+
+short __gen_e_acsl_h_short(int s)
+{
+ short __retres = (short)s;
+ return __retres;
+}
+
+int __gen_e_acsl_g_hidden(int x)
+{
+ return x;
+}
+
+int __gen_e_acsl_g(int x)
+{
+ int __gen_e_acsl_g_hidden_2;
+ __gen_e_acsl_g_hidden_2 = __gen_e_acsl_g_hidden(x);
+ return __gen_e_acsl_g_hidden_2;
+}
+
+mystruct __gen_e_acsl_t1(mystruct m)
+{
+ return m;
+}
+
+int __gen_e_acsl_p1(int x, int y)
+{
+ int __retres = x + (long)y > 0L;
+ return __retres;
+}
+
+long __gen_e_acsl_t2(mystruct m)
+{
+ long __retres = m.k + (long)m.l;
+ return __retres;
+}
+
+int __gen_e_acsl_p2_3(int x, __e_acsl_mpz_struct * 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_si(__gen_e_acsl_x,(long)x);
+ __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 *)(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));
+ int __retres = __gen_e_acsl_gt > 0;
+ __gmpz_clear(__gen_e_acsl_x);
+ __gmpz_clear(__gen_e_acsl_add);
+ __gmpz_clear(__gen_e_acsl__2);
+ return __retres;
+}
+
+int __gen_e_acsl_p2_5(int x, long y)
+{
+ __e_acsl_mpz_t __gen_e_acsl_x_2;
+ __e_acsl_mpz_t __gen_e_acsl_y;
+ __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)x);
+ __gmpz_init_set_si(__gen_e_acsl_y,y);
+ __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));
+ __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));
+ int __retres = __gen_e_acsl_gt_2 > 0;
+ __gmpz_clear(__gen_e_acsl_x_2);
+ __gmpz_clear(__gen_e_acsl_y);
+ __gmpz_clear(__gen_e_acsl_add_2);
+ __gmpz_clear(__gen_e_acsl__3);
+ return __retres;
+}
+
+int __gen_e_acsl_p2(int x, int y)
+{
+ int __retres = x + (long)y > 0L;
+ return __retres;
+}
+
+int __gen_e_acsl_k_pred(int x)
+{
+ int __retres = x > 0;
+ return __retres;
+}
+
+void __gen_e_acsl_f1_7(__e_acsl_mpz_t *__retres_arg, __e_acsl_mpz_struct * x,
+ __e_acsl_mpz_struct * y)
+{
+ __e_acsl_mpz_t __gen_e_acsl_add_4;
+ __gmpz_init(__gen_e_acsl_add_4);
+ __gmpz_add(__gen_e_acsl_add_4,(__e_acsl_mpz_struct const *)(x),
+ (__e_acsl_mpz_struct const *)(y));
+ __gmpz_init_set(*__retres_arg,
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_add_4));
+ __gmpz_clear(__gen_e_acsl_add_4);
+ return;
+}
+
+void __gen_e_acsl_f1_5(__e_acsl_mpz_t *__retres_arg, int x,
+ __e_acsl_mpz_struct * y)
+{
+ __e_acsl_mpz_t __gen_e_acsl_x_3;
+ __e_acsl_mpz_t __gen_e_acsl_add_3;
+ __gmpz_init_set_si(__gen_e_acsl_x_3,(long)x);
+ __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 *)(y));
+ __gmpz_init_set(*__retres_arg,
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_add_3));
+ __gmpz_clear(__gen_e_acsl_x_3);
+ __gmpz_clear(__gen_e_acsl_add_3);
+ return;
+}
+
+long __gen_e_acsl_f1(int x, int y)
+{
+ long __retres = x + (long)y;
+ 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 0000000000000000000000000000000000000000..9989adf5ca2bee1aad2ee77c8cb647276dbd3573
--- /dev/null
+++ b/src/plugins/e-acsl/tests/gmp/oracle/gen_functions2.c
@@ -0,0 +1,449 @@
+/* Generated by Frama-C */
+#include "stdio.h"
+#include "stdlib.h"
+extern int __e_acsl_sound_verdict;
+
+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 x, int y);
+
+/*@ predicate p2(ℤ x, ℤ y) = x + y > 0;
+
+*/
+int __gen_e_acsl_p2_3(int x, __e_acsl_mpz_struct * y);
+
+int __gen_e_acsl_p2(int x, int y);
+
+/*@ logic ℤ f1(ℤ x, ℤ y) = x + y;
+
+*/
+void __gen_e_acsl_f1_7(__e_acsl_mpz_t *__retres_arg, __e_acsl_mpz_struct * x,
+ __e_acsl_mpz_struct * y);
+
+void __gen_e_acsl_f1_5(__e_acsl_mpz_t *__retres_arg, int x,
+ __e_acsl_mpz_struct * y);
+
+void __gen_e_acsl_f1(__e_acsl_mpz_t *__retres_arg, int x, int y);
+
+/*@ logic char h_char(char c) = c;
+ */
+char __gen_e_acsl_h_char(int c);
+
+/*@ logic short h_short(short s) = s;
+ */
+short __gen_e_acsl_h_short(int s);
+
+/*@ logic int g_hidden(int x) = x;
+ */
+int __gen_e_acsl_g_hidden(int x);
+
+/*@ logic int g(int x) = g_hidden(x);
+ */
+int __gen_e_acsl_g(int x);
+
+/*@ logic mystruct t1(mystruct m) = m;
+ */
+mystruct __gen_e_acsl_t1(mystruct m);
+
+/*@ logic ℤ t2(mystruct m) = m.k + m.l;
+ */
+void __gen_e_acsl_t2(__e_acsl_mpz_t *__retres_arg, mystruct m);
+
+/*@ predicate k_pred(ℤ x) = x > 0;
+
+*/
+int __gen_e_acsl_k_pred(int x);
+
+/*@ 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);
+ */
+/*@ 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_2;
+ __gen_e_acsl_p1_2 = __gen_e_acsl_p1(x,y);
+ __e_acsl_assert(__gen_e_acsl_p1_2,(char *)"Assertion",(char *)"main",
+ (char *)"p1(x, y)",42);
+ }
+ /*@ assert p2(3, 4); */
+ {
+ int __gen_e_acsl_p2_2;
+ __gen_e_acsl_p2_2 = __gen_e_acsl_p2(3,4);
+ __e_acsl_assert(__gen_e_acsl_p2_2,(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_4;
+ __gmpz_init_set_str(__gen_e_acsl__3,"99999999999999999999999999999",10);
+ __gen_e_acsl_p2_4 = __gen_e_acsl_p2_3(5,
+ (__e_acsl_mpz_struct *)__gen_e_acsl__3);
+ __e_acsl_assert(__gen_e_acsl_p2_4,(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_2;
+ __e_acsl_mpz_t __gen_e_acsl__5;
+ int __gen_e_acsl_eq;
+ __gen_e_acsl_f1(& __gen_e_acsl_f1_2,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_2),
+ (__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_2);
+ __gmpz_clear(__gen_e_acsl__5);
+ }
+ /*@ assert p2(x, f1(3, 4)); */
+ {
+ __e_acsl_mpz_t __gen_e_acsl_f1_4;
+ int __gen_e_acsl_p2_6;
+ __gen_e_acsl_f1(& __gen_e_acsl_f1_4,3,4);
+ /*@ assert
+ Eva: initialization:
+ \initialized((__e_acsl_mpz_struct *)__gen_e_acsl_f1_4);
+ */
+ __gen_e_acsl_p2_6 = __gen_e_acsl_p2_3(x,
+ (__e_acsl_mpz_struct *)__gen_e_acsl_f1_4);
+ __e_acsl_assert(__gen_e_acsl_p2_6,(char *)"Assertion",(char *)"main",
+ (char *)"p2(x, f1(3, 4))",47);
+ __gmpz_clear(__gen_e_acsl_f1_4);
+ }
+ /*@ assert f1(9, 99999999999999999999999999999) > 0; */
+ {
+ __e_acsl_mpz_t __gen_e_acsl__6;
+ __e_acsl_mpz_t __gen_e_acsl_f1_6;
+ __e_acsl_mpz_t __gen_e_acsl__7;
+ int __gen_e_acsl_gt_4;
+ __gmpz_init_set_str(__gen_e_acsl__6,"99999999999999999999999999999",10);
+ __gen_e_acsl_f1_5(& __gen_e_acsl_f1_6,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_6),
+ (__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_6);
+ __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_8;
+ __e_acsl_mpz_t __gen_e_acsl__9;
+ int __gen_e_acsl_eq_2;
+ __gmpz_init_set_str(__gen_e_acsl__8,"99999999999999999999999999999",10);
+ __gen_e_acsl_f1_7(& __gen_e_acsl_f1_8,
+ (__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_8),
+ (__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_8);
+ __gmpz_clear(__gen_e_acsl__9);
+ }
+ /*@ assert g(x) ≡ x; */
+ {
+ int __gen_e_acsl_g_2;
+ __e_acsl_mpz_t __gen_e_acsl_app;
+ __e_acsl_mpz_t __gen_e_acsl_x_6;
+ int __gen_e_acsl_eq_3;
+ __gen_e_acsl_g_2 = __gen_e_acsl_g(x);
+ __gmpz_init_set_si(__gen_e_acsl_app,(long)__gen_e_acsl_g_2);
+ __gmpz_init_set_si(__gen_e_acsl_x_6,(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_6));
+ __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_6);
+ }
+ char c = (char)'c';
+ /*@ assert h_char(c) ≡ c; */
+ {
+ char __gen_e_acsl_h_char_2;
+ __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_2 = __gen_e_acsl_h_char((int)c);
+ __gmpz_init_set_si(__gen_e_acsl_app_2,(long)__gen_e_acsl_h_char_2);
+ __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_2;
+ __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_2 = __gen_e_acsl_h_short((int)s);
+ __gmpz_init_set_si(__gen_e_acsl_app_3,(long)__gen_e_acsl_h_short_2);
+ __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_2;
+ __e_acsl_mpz_t __gen_e_acsl_t2_2;
+ __e_acsl_mpz_t __gen_e_acsl__12;
+ int __gen_e_acsl_eq_6;
+ __gen_e_acsl_t1_2 = __gen_e_acsl_t1(m);
+ __gen_e_acsl_t2(& __gen_e_acsl_t2_2,__gen_e_acsl_t1_2);
+ __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_2),
+ (__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_2);
+ __gmpz_clear(__gen_e_acsl__12);
+ }
+ __gen_e_acsl_k(9);
+ __retres = 0;
+ return __retres;
+}
+
+/*@ requires k_pred(x); */
+void __gen_e_acsl_k(int x)
+{
+ {
+ int __gen_e_acsl_k_pred_2;
+ __gen_e_acsl_k_pred_2 = __gen_e_acsl_k_pred(x);
+ __e_acsl_assert(__gen_e_acsl_k_pred_2,(char *)"Precondition",(char *)"k",
+ (char *)"k_pred(x)",25);
+ }
+ k(x);
+ return;
+}
+
+char __gen_e_acsl_h_char(int c)
+{
+ char __retres = (char)c;
+ return __retres;
+}
+
+short __gen_e_acsl_h_short(int s)
+{
+ short __retres = (short)s;
+ return __retres;
+}
+
+int __gen_e_acsl_g_hidden(int x)
+{
+ return x;
+}
+
+int __gen_e_acsl_g(int x)
+{
+ int __gen_e_acsl_g_hidden_2;
+ __gen_e_acsl_g_hidden_2 = __gen_e_acsl_g_hidden(x);
+ return __gen_e_acsl_g_hidden_2;
+}
+
+mystruct __gen_e_acsl_t1(mystruct m)
+{
+ return m;
+}
+
+int __gen_e_acsl_p1(int x, int y)
+{
+ __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)x);
+ __gmpz_init_set_si(__gen_e_acsl_y,(long)y);
+ __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_));
+ int __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;
+}
+
+void __gen_e_acsl_t2(__e_acsl_mpz_t *__retres_arg, mystruct m)
+{
+ __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)m.k);
+ __gmpz_init_set_si(__gen_e_acsl__11,(long)m.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;
+}
+
+int __gen_e_acsl_p2_3(int x, __e_acsl_mpz_struct * y)
+{
+ __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_si(__gen_e_acsl_x_3,(long)x);
+ __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 *)(y));
+ __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));
+ int __retres = __gen_e_acsl_gt_3 > 0;
+ __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_p2(int x, int y)
+{
+ __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)x);
+ __gmpz_init_set_si(__gen_e_acsl_y_2,(long)y);
+ __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));
+ int __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_k_pred(int x)
+{
+ __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)x);
+ __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_));
+ int __retres = __gen_e_acsl_gt > 0;
+ __gmpz_clear(__gen_e_acsl_x);
+ __gmpz_clear(__gen_e_acsl_);
+ return __retres;
+}
+
+void __gen_e_acsl_f1_7(__e_acsl_mpz_t *__retres_arg, __e_acsl_mpz_struct * x,
+ __e_acsl_mpz_struct * y)
+{
+ __e_acsl_mpz_t __gen_e_acsl_add_6;
+ __gmpz_init(__gen_e_acsl_add_6);
+ __gmpz_add(__gen_e_acsl_add_6,(__e_acsl_mpz_struct const *)(x),
+ (__e_acsl_mpz_struct const *)(y));
+ __gmpz_init_set(*__retres_arg,
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_add_6));
+ __gmpz_clear(__gen_e_acsl_add_6);
+ return;
+}
+
+void __gen_e_acsl_f1_5(__e_acsl_mpz_t *__retres_arg, int x,
+ __e_acsl_mpz_struct * y)
+{
+ __e_acsl_mpz_t __gen_e_acsl_x_5;
+ __e_acsl_mpz_t __gen_e_acsl_add_5;
+ __gmpz_init_set_si(__gen_e_acsl_x_5,(long)x);
+ __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 *)(y));
+ __gmpz_init_set(*__retres_arg,
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_add_5));
+ __gmpz_clear(__gen_e_acsl_x_5);
+ __gmpz_clear(__gen_e_acsl_add_5);
+ return;
+}
+
+void __gen_e_acsl_f1(__e_acsl_mpz_t *__retres_arg, int x, int y)
+{
+ __e_acsl_mpz_t __gen_e_acsl_x_4;
+ __e_acsl_mpz_t __gen_e_acsl_y_3;
+ __e_acsl_mpz_t __gen_e_acsl_add_4;
+ __gmpz_init_set_si(__gen_e_acsl_x_4,(long)x);
+ __gmpz_init_set_si(__gen_e_acsl_y_3,(long)y);
+ __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_3));
+ __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_3);
+ __gmpz_clear(__gen_e_acsl_add_4);
+ return;
+}
+
+
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 0000000000000000000000000000000000000000..259afb2e7cf7aff685e3f821c94a0a230968a678
--- /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 0000000000000000000000000000000000000000..259afb2e7cf7aff685e3f821c94a0a230968a678
--- /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 0000000000000000000000000000000000000000..0fa4a22a630c4d80f8f44b38a7c561a6b5e93f13
--- /dev/null
+++ b/src/plugins/e-acsl/tests/gmp/oracle/gen_functions_rec.c
@@ -0,0 +1,208 @@
+/* Generated by Frama-C */
+#include "stdio.h"
+#include "stdlib.h"
+/*@ logic ℤ f1(ℤ n) = n ≤ 0? 0: f1(n - 1) + n;
+ */
+/*@ logic ℤ f2(ℤ n) = n < 0? 1: (f2(n - 1) * f2(n - 2)) / f2(n - 3);
+ */
+int __gen_e_acsl_f2_2(long n);
+
+int __gen_e_acsl_f2(int n);
+
+/*@ logic ℤ g(ℤ n) = 0;
+ */
+int __gen_e_acsl_g_5(long n);
+
+int __gen_e_acsl_g(int n);
+
+/*@ logic ℤ f3(ℤ n) = n > 0? g(n) * f3(n - 1) - 5: g(n + 1);
+ */
+int __gen_e_acsl_f3_2(long n);
+
+int __gen_e_acsl_f3(int n);
+
+/*@
+logic ℤ f4(ℤ n) =
+ n < 100? f4(n + 1): (n < 0x7fffffffffffffffL? 0x7fffffffffffffffL: 6);
+
+*/
+unsigned long __gen_e_acsl_f4_2(long n);
+
+unsigned long __gen_e_acsl_f4(int n);
+
+int main(void)
+{
+ int __retres;
+ __e_acsl_memory_init((int *)0,(char ***)0,(size_t)8);
+ /*@ assert f2(7) ≡ 1; */
+ {
+ int __gen_e_acsl_f2_14;
+ __gen_e_acsl_f2_14 = __gen_e_acsl_f2(7);
+ __e_acsl_assert(__gen_e_acsl_f2_14 == 1,(char *)"Assertion",
+ (char *)"main",(char *)"f2(7) == 1",26);
+ }
+ /*@ assert f3(6) ≡ -5; */
+ {
+ int __gen_e_acsl_f3_6;
+ __gen_e_acsl_f3_6 = __gen_e_acsl_f3(6);
+ __e_acsl_assert(__gen_e_acsl_f3_6 == -5,(char *)"Assertion",
+ (char *)"main",(char *)"f3(6) == -5",28);
+ }
+ /*@ assert f4(9) > 0; */
+ {
+ unsigned long __gen_e_acsl_f4_6;
+ __gen_e_acsl_f4_6 = __gen_e_acsl_f4(9);
+ __e_acsl_assert(__gen_e_acsl_f4_6 > 0UL,(char *)"Assertion",
+ (char *)"main",(char *)"f4(9) > 0",30);
+ }
+ __retres = 0;
+ return __retres;
+}
+
+unsigned long __gen_e_acsl_f4_2(long n)
+{
+ unsigned long __gen_e_acsl_if_6;
+ if (n < 100L) {
+ unsigned long __gen_e_acsl_f4_4;
+ __gen_e_acsl_f4_4 = __gen_e_acsl_f4_2(n + 1L);
+ __gen_e_acsl_if_6 = __gen_e_acsl_f4_4;
+ }
+ else {
+ unsigned long __gen_e_acsl_if_5;
+ if (n < 9223372036854775807L) __gen_e_acsl_if_5 = 9223372036854775807UL;
+ else __gen_e_acsl_if_5 = 6UL;
+ __gen_e_acsl_if_6 = __gen_e_acsl_if_5;
+ }
+ return __gen_e_acsl_if_6;
+}
+
+unsigned long __gen_e_acsl_f4(int n)
+{
+ unsigned long __gen_e_acsl_if_8;
+ if (n < 100) {
+ unsigned long __gen_e_acsl_f4_5;
+ __gen_e_acsl_f4_5 = __gen_e_acsl_f4_2(n + 1L);
+ __gen_e_acsl_if_8 = __gen_e_acsl_f4_5;
+ }
+ else {
+ unsigned long __gen_e_acsl_if_7;
+ if ((long)n < 9223372036854775807L) __gen_e_acsl_if_7 = 9223372036854775807UL;
+ else __gen_e_acsl_if_7 = 6UL;
+ __gen_e_acsl_if_8 = __gen_e_acsl_if_7;
+ }
+ return __gen_e_acsl_if_8;
+}
+
+int __gen_e_acsl_f2_2(long n)
+{
+ int __gen_e_acsl_if;
+ if (n < 0L) __gen_e_acsl_if = 1;
+ else {
+ int __gen_e_acsl_f2_4;
+ int __gen_e_acsl_f2_6;
+ int __gen_e_acsl_f2_8;
+ __gen_e_acsl_f2_4 = __gen_e_acsl_f2_2(n - 1L);
+ __gen_e_acsl_f2_6 = __gen_e_acsl_f2_2(n - 2L);
+ __gen_e_acsl_f2_8 = __gen_e_acsl_f2_2(n - 3L);
+ __e_acsl_assert(__gen_e_acsl_f2_8 != 0,(char *)"RTE",(char *)"f2_2",
+ (char *)"division_by_zero: __gen_e_acsl_f2_8 != 0",10);
+ /*@ assert Eva: division_by_zero: __gen_e_acsl_f2_8 ≢ 0; */
+ /*@ assert
+ Eva: signed_overflow:
+ -2147483648 ≤ __gen_e_acsl_f2_4 * __gen_e_acsl_f2_6;
+ */
+ /*@ assert
+ Eva: signed_overflow:
+ __gen_e_acsl_f2_4 * __gen_e_acsl_f2_6 ≤ 2147483647;
+ */
+ /*@ assert
+ Eva: signed_overflow:
+ (int)(__gen_e_acsl_f2_4 * __gen_e_acsl_f2_6) / __gen_e_acsl_f2_8
+ ≤ 2147483647;
+ */
+ __gen_e_acsl_if = (__gen_e_acsl_f2_4 * __gen_e_acsl_f2_6) / __gen_e_acsl_f2_8;
+ }
+ return __gen_e_acsl_if;
+}
+
+int __gen_e_acsl_f2(int n)
+{
+ int __gen_e_acsl_if_2;
+ if (n < 0) __gen_e_acsl_if_2 = 1;
+ else {
+ int __gen_e_acsl_f2_9;
+ int __gen_e_acsl_f2_11;
+ int __gen_e_acsl_f2_13;
+ __gen_e_acsl_f2_9 = __gen_e_acsl_f2_2(n - 1L);
+ __gen_e_acsl_f2_11 = __gen_e_acsl_f2_2(n - 2L);
+ __gen_e_acsl_f2_13 = __gen_e_acsl_f2_2(n - 3L);
+ __e_acsl_assert(__gen_e_acsl_f2_13 != 0,(char *)"RTE",(char *)"f2",
+ (char *)"division_by_zero: __gen_e_acsl_f2_13 != 0",10);
+ /*@ assert Eva: division_by_zero: __gen_e_acsl_f2_13 ≢ 0; */
+ /*@ assert
+ Eva: signed_overflow:
+ -2147483648 ≤ __gen_e_acsl_f2_9 * __gen_e_acsl_f2_11;
+ */
+ /*@ assert
+ Eva: signed_overflow:
+ __gen_e_acsl_f2_9 * __gen_e_acsl_f2_11 ≤ 2147483647;
+ */
+ /*@ assert
+ Eva: signed_overflow:
+ (int)(__gen_e_acsl_f2_9 * __gen_e_acsl_f2_11) / __gen_e_acsl_f2_13
+ ≤ 2147483647;
+ */
+ __gen_e_acsl_if_2 = (__gen_e_acsl_f2_9 * __gen_e_acsl_f2_11) / __gen_e_acsl_f2_13;
+ }
+ return __gen_e_acsl_if_2;
+}
+
+int __gen_e_acsl_g_5(long n)
+{
+ int __retres = 0;
+ return __retres;
+}
+
+int __gen_e_acsl_g(int n)
+{
+ int __retres = 0;
+ return __retres;
+}
+
+int __gen_e_acsl_f3_2(long n)
+{
+ int __gen_e_acsl_if_3;
+ if (n > 0L) {
+ int __gen_e_acsl_g_4;
+ int __gen_e_acsl_f3_4;
+ __gen_e_acsl_g_4 = __gen_e_acsl_g((int)n);
+ __gen_e_acsl_f3_4 = __gen_e_acsl_f3_2(n - 1L);
+ __gen_e_acsl_if_3 = __gen_e_acsl_g_4 * __gen_e_acsl_f3_4 - 5;
+ }
+ else {
+ int __gen_e_acsl_g_6;
+ __gen_e_acsl_g_6 = __gen_e_acsl_g_5(n + 1L);
+ __gen_e_acsl_if_3 = __gen_e_acsl_g_6;
+ }
+ return __gen_e_acsl_if_3;
+}
+
+int __gen_e_acsl_f3(int n)
+{
+ int __gen_e_acsl_if_4;
+ if (n > 0) {
+ int __gen_e_acsl_g_2;
+ int __gen_e_acsl_f3_5;
+ __gen_e_acsl_g_2 = __gen_e_acsl_g(n);
+ __gen_e_acsl_f3_5 = __gen_e_acsl_f3_2(n - 1L);
+ __gen_e_acsl_if_4 = __gen_e_acsl_g_2 * __gen_e_acsl_f3_5 - 5;
+ }
+ else {
+ int __gen_e_acsl_g_8;
+ __gen_e_acsl_g_8 = __gen_e_acsl_g_5(n + 1L);
+ __gen_e_acsl_if_4 = __gen_e_acsl_g_8;
+ }
+ return __gen_e_acsl_if_4;
+}
+
+
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 0000000000000000000000000000000000000000..c13d6d1e49b1ef2fae4f1c8c5fb0922a23127c3f
--- /dev/null
+++ b/src/plugins/e-acsl/tests/gmp/oracle/gen_functions_rec2.c
@@ -0,0 +1,593 @@
+/* Generated by Frama-C */
+#include "stdio.h"
+#include "stdlib.h"
+/*@ logic ℤ f1(ℤ n) = n ≤ 0? 0: f1(n - 1) + n;
+ */
+/*@ logic ℤ f2(ℤ n) = n < 0? 1: (f2(n - 1) * f2(n - 2)) / f2(n - 3);
+
+*/
+void __gen_e_acsl_f2_2(__e_acsl_mpz_t *__retres_arg, __e_acsl_mpz_struct * n);
+
+void __gen_e_acsl_f2(__e_acsl_mpz_t *__retres_arg, int n);
+
+/*@ logic ℤ g(ℤ n) = 0;
+
+*/
+void __gen_e_acsl_g_5(__e_acsl_mpz_t *__retres_arg, __e_acsl_mpz_struct * n);
+
+void __gen_e_acsl_g(__e_acsl_mpz_t *__retres_arg, int n);
+
+/*@ logic ℤ f3(ℤ n) = n > 0? g(n) * f3(n - 1) - 5: g(n + 1);
+
+*/
+void __gen_e_acsl_f3_2(__e_acsl_mpz_t *__retres_arg, __e_acsl_mpz_struct * n);
+
+void __gen_e_acsl_f3(__e_acsl_mpz_t *__retres_arg, int n);
+
+/*@
+logic ℤ f4(ℤ n) =
+ n < 100? f4(n + 1): (n < 0x7fffffffffffffffL? 0x7fffffffffffffffL: 6);
+
+*/
+void __gen_e_acsl_f4_2(__e_acsl_mpz_t *__retres_arg, __e_acsl_mpz_struct * n);
+
+void __gen_e_acsl_f4(__e_acsl_mpz_t *__retres_arg, int n);
+
+int main(void)
+{
+ int __retres;
+ __e_acsl_memory_init((int *)0,(char ***)0,(size_t)8);
+ /*@ assert f2(7) ≡ 1; */
+ {
+ __e_acsl_mpz_t __gen_e_acsl_f2_14;
+ __e_acsl_mpz_t __gen_e_acsl__13;
+ int __gen_e_acsl_eq;
+ __gen_e_acsl_f2(& __gen_e_acsl_f2_14,7);
+ __gmpz_init_set_si(__gen_e_acsl__13,1L);
+ __gen_e_acsl_eq = __gmpz_cmp((__e_acsl_mpz_struct const *)(__gen_e_acsl_f2_14),
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl__13));
+ __e_acsl_assert(__gen_e_acsl_eq == 0,(char *)"Assertion",(char *)"main",
+ (char *)"f2(7) == 1",26);
+ __gmpz_clear(__gen_e_acsl_f2_14);
+ __gmpz_clear(__gen_e_acsl__13);
+ }
+ /*@ assert f3(6) ≡ -5; */
+ {
+ __e_acsl_mpz_t __gen_e_acsl_f3_6;
+ __e_acsl_mpz_t __gen_e_acsl__23;
+ __e_acsl_mpz_t __gen_e_acsl_neg;
+ int __gen_e_acsl_eq_2;
+ __gen_e_acsl_f3(& __gen_e_acsl_f3_6,6);
+ __gmpz_init_set_si(__gen_e_acsl__23,5L);
+ __gmpz_init(__gen_e_acsl_neg);
+ __gmpz_neg(__gen_e_acsl_neg,
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl__23));
+ __gen_e_acsl_eq_2 = __gmpz_cmp((__e_acsl_mpz_struct const *)(__gen_e_acsl_f3_6),
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_neg));
+ __e_acsl_assert(__gen_e_acsl_eq_2 == 0,(char *)"Assertion",
+ (char *)"main",(char *)"f3(6) == -5",28);
+ __gmpz_clear(__gen_e_acsl_f3_6);
+ __gmpz_clear(__gen_e_acsl__23);
+ __gmpz_clear(__gen_e_acsl_neg);
+ }
+ /*@ assert f4(9) > 0; */
+ {
+ __e_acsl_mpz_t __gen_e_acsl_f4_6;
+ __e_acsl_mpz_t __gen_e_acsl__34;
+ int __gen_e_acsl_gt_3;
+ __gen_e_acsl_f4(& __gen_e_acsl_f4_6,9);
+ __gmpz_init_set_si(__gen_e_acsl__34,0L);
+ __gen_e_acsl_gt_3 = __gmpz_cmp((__e_acsl_mpz_struct const *)(__gen_e_acsl_f4_6),
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl__34));
+ __e_acsl_assert(__gen_e_acsl_gt_3 > 0,(char *)"Assertion",(char *)"main",
+ (char *)"f4(9) > 0",30);
+ __gmpz_clear(__gen_e_acsl_f4_6);
+ __gmpz_clear(__gen_e_acsl__34);
+ }
+ __retres = 0;
+ return __retres;
+}
+
+void __gen_e_acsl_f4_2(__e_acsl_mpz_t *__retres_arg, __e_acsl_mpz_struct * n)
+{
+ __e_acsl_mpz_t __gen_e_acsl__26;
+ int __gen_e_acsl_lt_4;
+ __e_acsl_mpz_t __gen_e_acsl_if_6;
+ __gmpz_init_set_si(__gen_e_acsl__26,100L);
+ __gen_e_acsl_lt_4 = __gmpz_cmp((__e_acsl_mpz_struct const *)(n),
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl__26));
+ if (__gen_e_acsl_lt_4 < 0) {
+ __e_acsl_mpz_t __gen_e_acsl__27;
+ __e_acsl_mpz_t __gen_e_acsl_add_4;
+ __e_acsl_mpz_t __gen_e_acsl_f4_4;
+ __gmpz_init_set_si(__gen_e_acsl__27,1L);
+ __gmpz_init(__gen_e_acsl_add_4);
+ __gmpz_add(__gen_e_acsl_add_4,(__e_acsl_mpz_struct const *)(n),
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl__27));
+ /*@ assert
+ Eva: initialization:
+ \initialized((__e_acsl_mpz_struct *)__gen_e_acsl_add_4);
+ */
+ __gen_e_acsl_f4_2(& __gen_e_acsl_f4_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_f4_4));
+ __gmpz_clear(__gen_e_acsl__27);
+ __gmpz_clear(__gen_e_acsl_add_4);
+ __gmpz_clear(__gen_e_acsl_f4_4);
+ }
+ else {
+ __e_acsl_mpz_t __gen_e_acsl__28;
+ int __gen_e_acsl_lt_5;
+ __e_acsl_mpz_t __gen_e_acsl_if_5;
+ __gmpz_init_set_ui(__gen_e_acsl__28,9223372036854775807UL);
+ __gen_e_acsl_lt_5 = __gmpz_cmp((__e_acsl_mpz_struct const *)(n),
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl__28));
+ if (__gen_e_acsl_lt_5 < 0) {
+ __e_acsl_mpz_t __gen_e_acsl__29;
+ __gmpz_init_set_ui(__gen_e_acsl__29,9223372036854775807UL);
+ __gmpz_init_set(__gen_e_acsl_if_5,
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl__29));
+ __gmpz_clear(__gen_e_acsl__29);
+ }
+ else {
+ __e_acsl_mpz_t __gen_e_acsl__30;
+ __gmpz_init_set_si(__gen_e_acsl__30,6L);
+ __gmpz_init_set(__gen_e_acsl_if_5,
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl__30));
+ __gmpz_clear(__gen_e_acsl__30);
+ }
+ __gmpz_init_set(__gen_e_acsl_if_6,
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_if_5));
+ __gmpz_clear(__gen_e_acsl__28);
+ __gmpz_clear(__gen_e_acsl_if_5);
+ }
+ __gmpz_init_set(*__retres_arg,
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_if_6));
+ __gmpz_clear(__gen_e_acsl__26);
+ __gmpz_clear(__gen_e_acsl_if_6);
+ return;
+}
+
+void __gen_e_acsl_f4(__e_acsl_mpz_t *__retres_arg, int n)
+{
+ __e_acsl_mpz_t __gen_e_acsl_n_6;
+ __e_acsl_mpz_t __gen_e_acsl__24;
+ int __gen_e_acsl_lt_3;
+ __e_acsl_mpz_t __gen_e_acsl_if_8;
+ __gmpz_init_set_si(__gen_e_acsl_n_6,(long)n);
+ __gmpz_init_set_si(__gen_e_acsl__24,100L);
+ __gen_e_acsl_lt_3 = __gmpz_cmp((__e_acsl_mpz_struct const *)(__gen_e_acsl_n_6),
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl__24));
+ if (__gen_e_acsl_lt_3 < 0) {
+ __e_acsl_mpz_t __gen_e_acsl_n_7;
+ __e_acsl_mpz_t __gen_e_acsl__25;
+ __e_acsl_mpz_t __gen_e_acsl_add_3;
+ __e_acsl_mpz_t __gen_e_acsl_f4_5;
+ __gmpz_init_set_si(__gen_e_acsl_n_7,(long)n);
+ __gmpz_init_set_si(__gen_e_acsl__25,1L);
+ __gmpz_init(__gen_e_acsl_add_3);
+ __gmpz_add(__gen_e_acsl_add_3,
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_n_7),
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl__25));
+ /*@ assert
+ Eva: initialization:
+ \initialized((__e_acsl_mpz_struct *)__gen_e_acsl_add_3);
+ */
+ __gen_e_acsl_f4_2(& __gen_e_acsl_f4_5,
+ (__e_acsl_mpz_struct *)__gen_e_acsl_add_3);
+ __gmpz_init_set(__gen_e_acsl_if_8,
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_f4_5));
+ __gmpz_clear(__gen_e_acsl_n_7);
+ __gmpz_clear(__gen_e_acsl__25);
+ __gmpz_clear(__gen_e_acsl_add_3);
+ __gmpz_clear(__gen_e_acsl_f4_5);
+ }
+ else {
+ __e_acsl_mpz_t __gen_e_acsl_n_8;
+ __e_acsl_mpz_t __gen_e_acsl__31;
+ int __gen_e_acsl_lt_6;
+ __e_acsl_mpz_t __gen_e_acsl_if_7;
+ __gmpz_init_set_si(__gen_e_acsl_n_8,(long)n);
+ __gmpz_init_set_ui(__gen_e_acsl__31,9223372036854775807UL);
+ __gen_e_acsl_lt_6 = __gmpz_cmp((__e_acsl_mpz_struct const *)(__gen_e_acsl_n_8),
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl__31));
+ if (__gen_e_acsl_lt_6 < 0) {
+ __e_acsl_mpz_t __gen_e_acsl__32;
+ __gmpz_init_set_ui(__gen_e_acsl__32,9223372036854775807UL);
+ __gmpz_init_set(__gen_e_acsl_if_7,
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl__32));
+ __gmpz_clear(__gen_e_acsl__32);
+ }
+ else {
+ __e_acsl_mpz_t __gen_e_acsl__33;
+ __gmpz_init_set_si(__gen_e_acsl__33,6L);
+ __gmpz_init_set(__gen_e_acsl_if_7,
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl__33));
+ __gmpz_clear(__gen_e_acsl__33);
+ }
+ __gmpz_init_set(__gen_e_acsl_if_8,
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_if_7));
+ __gmpz_clear(__gen_e_acsl_n_8);
+ __gmpz_clear(__gen_e_acsl__31);
+ __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_6);
+ __gmpz_clear(__gen_e_acsl__24);
+ __gmpz_clear(__gen_e_acsl_if_8);
+ return;
+}
+
+void __gen_e_acsl_f2_2(__e_acsl_mpz_t *__retres_arg, __e_acsl_mpz_struct * n)
+{
+ __e_acsl_mpz_t __gen_e_acsl__4;
+ int __gen_e_acsl_lt_2;
+ __e_acsl_mpz_t __gen_e_acsl_if;
+ __gmpz_init_set_si(__gen_e_acsl__4,0L);
+ __gen_e_acsl_lt_2 = __gmpz_cmp((__e_acsl_mpz_struct const *)(n),
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl__4));
+ if (__gen_e_acsl_lt_2 < 0) {
+ __e_acsl_mpz_t __gen_e_acsl__5;
+ __gmpz_init_set_si(__gen_e_acsl__5,1L);
+ __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_f2_4;
+ __e_acsl_mpz_t __gen_e_acsl__7;
+ __e_acsl_mpz_t __gen_e_acsl_sub_3;
+ __e_acsl_mpz_t __gen_e_acsl_f2_6;
+ __e_acsl_mpz_t __gen_e_acsl_mul;
+ __e_acsl_mpz_t __gen_e_acsl__8;
+ __e_acsl_mpz_t __gen_e_acsl_sub_4;
+ __e_acsl_mpz_t __gen_e_acsl_f2_8;
+ __e_acsl_mpz_t __gen_e_acsl__9;
+ int __gen_e_acsl_div_guard;
+ __e_acsl_mpz_t __gen_e_acsl_div;
+ __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 *)(n),
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl__6));
+ /*@ assert
+ Eva: initialization:
+ \initialized((__e_acsl_mpz_struct *)__gen_e_acsl_sub_2);
+ */
+ __gen_e_acsl_f2_2(& __gen_e_acsl_f2_4,
+ (__e_acsl_mpz_struct *)__gen_e_acsl_sub_2);
+ __gmpz_init_set_si(__gen_e_acsl__7,2L);
+ __gmpz_init(__gen_e_acsl_sub_3);
+ __gmpz_sub(__gen_e_acsl_sub_3,(__e_acsl_mpz_struct const *)(n),
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl__7));
+ /*@ assert
+ Eva: initialization:
+ \initialized((__e_acsl_mpz_struct *)__gen_e_acsl_sub_3);
+ */
+ __gen_e_acsl_f2_2(& __gen_e_acsl_f2_6,
+ (__e_acsl_mpz_struct *)__gen_e_acsl_sub_3);
+ __gmpz_init(__gen_e_acsl_mul);
+ __gmpz_mul(__gen_e_acsl_mul,
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_f2_4),
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_f2_6));
+ __gmpz_init_set_si(__gen_e_acsl__8,3L);
+ __gmpz_init(__gen_e_acsl_sub_4);
+ __gmpz_sub(__gen_e_acsl_sub_4,(__e_acsl_mpz_struct const *)(n),
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl__8));
+ /*@ assert
+ Eva: initialization:
+ \initialized((__e_acsl_mpz_struct *)__gen_e_acsl_sub_4);
+ */
+ __gen_e_acsl_f2_2(& __gen_e_acsl_f2_8,
+ (__e_acsl_mpz_struct *)__gen_e_acsl_sub_4);
+ __gmpz_init_set_si(__gen_e_acsl__9,0L);
+ __gen_e_acsl_div_guard = __gmpz_cmp((__e_acsl_mpz_struct const *)(__gen_e_acsl_f2_8),
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl__9));
+ __gmpz_init(__gen_e_acsl_div);
+ /*@ assert E_ACSL: f2(n - 3) ≢ 0; */
+ __e_acsl_assert(! (__gen_e_acsl_div_guard == 0),(char *)"Assertion",
+ (char *)"f2_2",(char *)"f2(n - 3) == 0",10);
+ __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_8));
+ __gmpz_init_set(__gen_e_acsl_if,
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_div));
+ __gmpz_clear(__gen_e_acsl__6);
+ __gmpz_clear(__gen_e_acsl_sub_2);
+ __gmpz_clear(__gen_e_acsl_f2_4);
+ __gmpz_clear(__gen_e_acsl__7);
+ __gmpz_clear(__gen_e_acsl_sub_3);
+ __gmpz_clear(__gen_e_acsl_f2_6);
+ __gmpz_clear(__gen_e_acsl_mul);
+ __gmpz_clear(__gen_e_acsl__8);
+ __gmpz_clear(__gen_e_acsl_sub_4);
+ __gmpz_clear(__gen_e_acsl_f2_8);
+ __gmpz_clear(__gen_e_acsl__9);
+ __gmpz_clear(__gen_e_acsl_div);
+ }
+ __gmpz_init_set(*__retres_arg,
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_if));
+ __gmpz_clear(__gen_e_acsl__4);
+ __gmpz_clear(__gen_e_acsl_if);
+ return;
+}
+
+void __gen_e_acsl_f2(__e_acsl_mpz_t *__retres_arg, int n)
+{
+ __e_acsl_mpz_t __gen_e_acsl_n;
+ __e_acsl_mpz_t __gen_e_acsl_;
+ int __gen_e_acsl_lt;
+ __e_acsl_mpz_t __gen_e_acsl_if_2;
+ __gmpz_init_set_si(__gen_e_acsl_n,(long)n);
+ __gmpz_init_set_si(__gen_e_acsl_,0L);
+ __gen_e_acsl_lt = __gmpz_cmp((__e_acsl_mpz_struct const *)(__gen_e_acsl_n),
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_));
+ if (__gen_e_acsl_lt < 0) {
+ __e_acsl_mpz_t __gen_e_acsl__2;
+ __gmpz_init_set_si(__gen_e_acsl__2,1L);
+ __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_f2_9;
+ __e_acsl_mpz_t __gen_e_acsl__10;
+ __e_acsl_mpz_t __gen_e_acsl_sub_5;
+ __e_acsl_mpz_t __gen_e_acsl_f2_11;
+ __e_acsl_mpz_t __gen_e_acsl_mul_2;
+ __e_acsl_mpz_t __gen_e_acsl__11;
+ __e_acsl_mpz_t __gen_e_acsl_sub_6;
+ __e_acsl_mpz_t __gen_e_acsl_f2_13;
+ __e_acsl_mpz_t __gen_e_acsl__12;
+ int __gen_e_acsl_div_guard_2;
+ __e_acsl_mpz_t __gen_e_acsl_div_2;
+ __gmpz_init_set_si(__gen_e_acsl_n_2,(long)n);
+ __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));
+ /*@ assert
+ Eva: initialization:
+ \initialized((__e_acsl_mpz_struct *)__gen_e_acsl_sub);
+ */
+ __gen_e_acsl_f2_2(& __gen_e_acsl_f2_9,
+ (__e_acsl_mpz_struct *)__gen_e_acsl_sub);
+ __gmpz_init_set_si(__gen_e_acsl__10,2L);
+ __gmpz_init(__gen_e_acsl_sub_5);
+ __gmpz_sub(__gen_e_acsl_sub_5,
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_n_2),
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl__10));
+ /*@ assert
+ Eva: initialization:
+ \initialized((__e_acsl_mpz_struct *)__gen_e_acsl_sub_5);
+ */
+ __gen_e_acsl_f2_2(& __gen_e_acsl_f2_11,
+ (__e_acsl_mpz_struct *)__gen_e_acsl_sub_5);
+ __gmpz_init(__gen_e_acsl_mul_2);
+ __gmpz_mul(__gen_e_acsl_mul_2,
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_f2_9),
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_f2_11));
+ __gmpz_init_set_si(__gen_e_acsl__11,3L);
+ __gmpz_init(__gen_e_acsl_sub_6);
+ __gmpz_sub(__gen_e_acsl_sub_6,
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_n_2),
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl__11));
+ /*@ assert
+ Eva: initialization:
+ \initialized((__e_acsl_mpz_struct *)__gen_e_acsl_sub_6);
+ */
+ __gen_e_acsl_f2_2(& __gen_e_acsl_f2_13,
+ (__e_acsl_mpz_struct *)__gen_e_acsl_sub_6);
+ __gmpz_init_set_si(__gen_e_acsl__12,0L);
+ __gen_e_acsl_div_guard_2 = __gmpz_cmp((__e_acsl_mpz_struct const *)(__gen_e_acsl_f2_13),
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl__12));
+ __gmpz_init(__gen_e_acsl_div_2);
+ /*@ assert E_ACSL: f2(n - 3) ≢ 0; */
+ __e_acsl_assert(! (__gen_e_acsl_div_guard_2 == 0),(char *)"Assertion",
+ (char *)"f2",(char *)"f2(n - 3) == 0",10);
+ __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_13));
+ __gmpz_init_set(__gen_e_acsl_if_2,
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_div_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_f2_9);
+ __gmpz_clear(__gen_e_acsl__10);
+ __gmpz_clear(__gen_e_acsl_sub_5);
+ __gmpz_clear(__gen_e_acsl_f2_11);
+ __gmpz_clear(__gen_e_acsl_mul_2);
+ __gmpz_clear(__gen_e_acsl__11);
+ __gmpz_clear(__gen_e_acsl_sub_6);
+ __gmpz_clear(__gen_e_acsl_f2_13);
+ __gmpz_clear(__gen_e_acsl__12);
+ __gmpz_clear(__gen_e_acsl_div_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;
+}
+
+void __gen_e_acsl_g_5(__e_acsl_mpz_t *__retres_arg, __e_acsl_mpz_struct * n)
+{
+ __gmpz_init_set_si(*__retres_arg,0L);
+ return;
+}
+
+void __gen_e_acsl_g(__e_acsl_mpz_t *__retres_arg, int n)
+{
+ __gmpz_init_set_si(*__retres_arg,0L);
+ return;
+}
+
+void __gen_e_acsl_f3_2(__e_acsl_mpz_t *__retres_arg, __e_acsl_mpz_struct * n)
+{
+ __e_acsl_mpz_t __gen_e_acsl__16;
+ int __gen_e_acsl_gt_2;
+ __e_acsl_mpz_t __gen_e_acsl_if_3;
+ __gmpz_init_set_si(__gen_e_acsl__16,0L);
+ __gen_e_acsl_gt_2 = __gmpz_cmp((__e_acsl_mpz_struct const *)(n),
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl__16));
+ if (__gen_e_acsl_gt_2 > 0) {
+ long __gen_e_acsl__17;
+ __e_acsl_mpz_t __gen_e_acsl_g_4;
+ __e_acsl_mpz_t __gen_e_acsl__18;
+ __e_acsl_mpz_t __gen_e_acsl_sub_8;
+ __e_acsl_mpz_t __gen_e_acsl_f3_4;
+ __e_acsl_mpz_t __gen_e_acsl_mul_3;
+ __e_acsl_mpz_t __gen_e_acsl__19;
+ __e_acsl_mpz_t __gen_e_acsl_sub_9;
+ __gen_e_acsl__17 = __gmpz_get_si((__e_acsl_mpz_struct const *)(n));
+ __gen_e_acsl_g(& __gen_e_acsl_g_4,(int)__gen_e_acsl__17);
+ __gmpz_init_set_si(__gen_e_acsl__18,1L);
+ __gmpz_init(__gen_e_acsl_sub_8);
+ __gmpz_sub(__gen_e_acsl_sub_8,(__e_acsl_mpz_struct const *)(n),
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl__18));
+ /*@ assert
+ Eva: initialization:
+ \initialized((__e_acsl_mpz_struct *)__gen_e_acsl_sub_8);
+ */
+ __gen_e_acsl_f3_2(& __gen_e_acsl_f3_4,
+ (__e_acsl_mpz_struct *)__gen_e_acsl_sub_8);
+ __gmpz_init(__gen_e_acsl_mul_3);
+ __gmpz_mul(__gen_e_acsl_mul_3,
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_g_4),
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_f3_4));
+ __gmpz_init_set_si(__gen_e_acsl__19,5L);
+ __gmpz_init(__gen_e_acsl_sub_9);
+ __gmpz_sub(__gen_e_acsl_sub_9,
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_mul_3),
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl__19));
+ __gmpz_init_set(__gen_e_acsl_if_3,
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_sub_9));
+ __gmpz_clear(__gen_e_acsl_g_4);
+ __gmpz_clear(__gen_e_acsl__18);
+ __gmpz_clear(__gen_e_acsl_sub_8);
+ __gmpz_clear(__gen_e_acsl_f3_4);
+ __gmpz_clear(__gen_e_acsl_mul_3);
+ __gmpz_clear(__gen_e_acsl__19);
+ __gmpz_clear(__gen_e_acsl_sub_9);
+ }
+ else {
+ __e_acsl_mpz_t __gen_e_acsl__20;
+ __e_acsl_mpz_t __gen_e_acsl_add;
+ __e_acsl_mpz_t __gen_e_acsl_g_6;
+ __gmpz_init_set_si(__gen_e_acsl__20,1L);
+ __gmpz_init(__gen_e_acsl_add);
+ __gmpz_add(__gen_e_acsl_add,(__e_acsl_mpz_struct const *)(n),
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl__20));
+ /*@ assert
+ Eva: initialization:
+ \initialized((__e_acsl_mpz_struct *)__gen_e_acsl_add);
+ */
+ __gen_e_acsl_g_5(& __gen_e_acsl_g_6,
+ (__e_acsl_mpz_struct *)__gen_e_acsl_add);
+ __gmpz_init_set(__gen_e_acsl_if_3,
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_g_6));
+ __gmpz_clear(__gen_e_acsl__20);
+ __gmpz_clear(__gen_e_acsl_add);
+ __gmpz_clear(__gen_e_acsl_g_6);
+ }
+ __gmpz_init_set(*__retres_arg,
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_if_3));
+ __gmpz_clear(__gen_e_acsl__16);
+ __gmpz_clear(__gen_e_acsl_if_3);
+ return;
+}
+
+void __gen_e_acsl_f3(__e_acsl_mpz_t *__retres_arg, int n)
+{
+ __e_acsl_mpz_t __gen_e_acsl_n_3;
+ __e_acsl_mpz_t __gen_e_acsl__14;
+ int __gen_e_acsl_gt;
+ __e_acsl_mpz_t __gen_e_acsl_if_4;
+ __gmpz_init_set_si(__gen_e_acsl_n_3,(long)n);
+ __gmpz_init_set_si(__gen_e_acsl__14,0L);
+ __gen_e_acsl_gt = __gmpz_cmp((__e_acsl_mpz_struct const *)(__gen_e_acsl_n_3),
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl__14));
+ if (__gen_e_acsl_gt > 0) {
+ __e_acsl_mpz_t __gen_e_acsl_g_2;
+ __e_acsl_mpz_t __gen_e_acsl_n_4;
+ __e_acsl_mpz_t __gen_e_acsl__15;
+ __e_acsl_mpz_t __gen_e_acsl_sub_7;
+ __e_acsl_mpz_t __gen_e_acsl_f3_5;
+ __e_acsl_mpz_t __gen_e_acsl_mul_4;
+ __e_acsl_mpz_t __gen_e_acsl__21;
+ __e_acsl_mpz_t __gen_e_acsl_sub_10;
+ __gen_e_acsl_g(& __gen_e_acsl_g_2,n);
+ __gmpz_init_set_si(__gen_e_acsl_n_4,(long)n);
+ __gmpz_init_set_si(__gen_e_acsl__15,1L);
+ __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));
+ /*@ assert
+ Eva: initialization:
+ \initialized((__e_acsl_mpz_struct *)__gen_e_acsl_sub_7);
+ */
+ __gen_e_acsl_f3_2(& __gen_e_acsl_f3_5,
+ (__e_acsl_mpz_struct *)__gen_e_acsl_sub_7);
+ __gmpz_init(__gen_e_acsl_mul_4);
+ __gmpz_mul(__gen_e_acsl_mul_4,
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_g_2),
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_f3_5));
+ __gmpz_init_set_si(__gen_e_acsl__21,5L);
+ __gmpz_init(__gen_e_acsl_sub_10);
+ __gmpz_sub(__gen_e_acsl_sub_10,
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_mul_4),
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl__21));
+ __gmpz_init_set(__gen_e_acsl_if_4,
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_sub_10));
+ __gmpz_clear(__gen_e_acsl_g_2);
+ __gmpz_clear(__gen_e_acsl_n_4);
+ __gmpz_clear(__gen_e_acsl__15);
+ __gmpz_clear(__gen_e_acsl_sub_7);
+ __gmpz_clear(__gen_e_acsl_f3_5);
+ __gmpz_clear(__gen_e_acsl_mul_4);
+ __gmpz_clear(__gen_e_acsl__21);
+ __gmpz_clear(__gen_e_acsl_sub_10);
+ }
+ else {
+ __e_acsl_mpz_t __gen_e_acsl_n_5;
+ __e_acsl_mpz_t __gen_e_acsl__22;
+ __e_acsl_mpz_t __gen_e_acsl_add_2;
+ __e_acsl_mpz_t __gen_e_acsl_g_8;
+ __gmpz_init_set_si(__gen_e_acsl_n_5,(long)n);
+ __gmpz_init_set_si(__gen_e_acsl__22,1L);
+ __gmpz_init(__gen_e_acsl_add_2);
+ __gmpz_add(__gen_e_acsl_add_2,
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_n_5),
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl__22));
+ /*@ assert
+ Eva: initialization:
+ \initialized((__e_acsl_mpz_struct *)__gen_e_acsl_add_2);
+ */
+ __gen_e_acsl_g_5(& __gen_e_acsl_g_8,
+ (__e_acsl_mpz_struct *)__gen_e_acsl_add_2);
+ __gmpz_init_set(__gen_e_acsl_if_4,
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_g_8));
+ __gmpz_clear(__gen_e_acsl_n_5);
+ __gmpz_clear(__gen_e_acsl__22);
+ __gmpz_clear(__gen_e_acsl_add_2);
+ __gmpz_clear(__gen_e_acsl_g_8);
+ }
+ __gmpz_init_set(*__retres_arg,
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_if_4));
+ __gmpz_clear(__gen_e_acsl_n_3);
+ __gmpz_clear(__gen_e_acsl__14);
+ __gmpz_clear(__gen_e_acsl_if_4);
+ 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 bdfaabe9c323f09e3c163d96e851403d33d8eadd..a2e7e709cc1b03f77f747ddda9fc902b26666500 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 f0225cf73e6ea678bbedc61ba28b397db2e9c357..bb9147c4b0e9addaee53ab74367d4c34a7e0a0a4 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 1b9876f5a9b0ea065f5db53858f36cf1c2d406a1..da6d987808fe99b9e725f20de1b03ab078b3b785 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
@@ -3,7 +3,7 @@
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 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 dfe484df046029c67a10781f25849678644e64e8..1b8c383a119177d8b45eac1037821eb6692704a7 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 70f435a9631d2c926ac0ed8d94b3e1189c4b8a64..66c2b5ac9dd0f05ecc77980ee35731fba9263872 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,7 +8,7 @@
[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.
@@ -17,10 +17,10 @@
E-ACSL construct `user-defined logic type' 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 +28,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 60bc68beda0ca390195bc892aa0fa0b579b95a1a..11a872659cbee2627db6282016bae368b9f1651b 100644
--- a/src/plugins/e-acsl/translate.ml
+++ b/src/plugins/e-acsl/translate.ml
@@ -448,36 +448,60 @@ 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
- List.fold_left
- (fun (l, env) a ->
- let e, env = term_to_exp kf env a in
- e :: l, env)
- ([], env)
- args
- with Invalid_argument _ ->
- Options.fatal "[Tapp] unexpected number of arguments when calling %s"
- fname
- in
(* build the varinfo (as an expression) which stores the result of the
function call. *)
let _, e, env =
- Env.new_var
- ~loc
- ~name:(fname ^ "_app")
- env
- (Some t)
- (Misc.cty (Extlib.the li.l_type))
- (fun vi _ ->
- [ Misc.mk_call ~loc ~result:(Cil.var vi) fname (List.rev args) ])
+ if Builtins.mem li.l_var_info.lv_name then
+ (* E-ACSL built-in function call *)
+ let args, env =
+ try
+ List.fold_right
+ (fun targ (l, env) ->
+ let e, env = term_to_exp kf env targ in
+ e :: l, env)
+ targs
+ ([], env)
+ with Invalid_argument _ ->
+ Options.fatal
+ "[Tapp] unexpected number of arguments when calling %s"
+ fname
+ in
+ Env.new_var
+ ~loc
+ ~name:(fname ^ "_app")
+ env
+ (Some t)
+ (Misc.cty (Extlib.the li.l_type))
+ (fun vi _ ->
+ [ Misc.mk_call ~loc ~result:(Cil.var vi) fname args ])
+ else
+ (* build the arguments and compute the integer_ty of the parameters *)
+ let params_ty, args, env =
+ List.fold_right
+ (fun targ (params_ty, args, env) ->
+ let e, env = term_to_exp kf env targ in
+ let param_ty = Typing.get_integer_ty targ in
+ let e, env =
+ try
+ let ty = Typing.typ_of_integer_ty param_ty in
+ add_cast loc env (Some ty) false (Some targ) e
+ with Typing.Not_an_integer ->
+ e, env
+ in
+ param_ty :: params_ty, e :: args, env)
+ targs
+ ([], [], env)
+ in
+ let gen_fname =
+ Env.Varname.get ~scope:Env.Global (Functions.RTL.mk_gen_name fname)
+ in
+ Logic_functions.tapp_to_exp ~loc gen_fname env t li params_ty args
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 +672,20 @@ 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). *)
+ 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"
@@ -845,7 +882,9 @@ 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;
+ Logic_functions.term_to_exp_ref := term_to_exp;
+ Logic_functions.named_predicate_to_exp_ref := named_predicate_to_exp
(* 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 ee2dcb2ffe54c50e7911dd7d475c7a66052e2669..5c0d16ac021e9b832383fe90e34bf566afab555e 100644
--- a/src/plugins/e-acsl/typing.ml
+++ b/src/plugins/e-acsl/typing.ml
@@ -46,28 +46,34 @@ let c_int = C_type IInt
let ikind ik = C_type ik
let other = Other
-include Datatype.Make
-(struct
- type t = integer_ty
- let name = "E_ACSL.New_typing.t"
- let reprs = [ Gmp; c_int ]
- include Datatype.Undefined
-
- let compare ty1 ty2 = match ty1, ty2 with
- | C_type i1, C_type i2 ->
- if i1 = i2 then 0
- else if Cil.intTypeIncluded i1 i2 then -1 else 1
- | (Other | C_type _), Gmp | Other, C_type _ -> -1
- | Gmp, (C_type _ | Other) | C_type _, Other -> 1
- | Gmp, Gmp | Other, Other -> 0
-
- let equal = Datatype.from_compare
-
- let pretty fmt = function
- | Gmp -> Format.pp_print_string fmt "GMP"
- | C_type k -> Printer.pp_ikind fmt k
- | Other -> Format.pp_print_string fmt "OTHER"
- end)
+module D =
+ Datatype.Make_with_collections
+ (struct
+ type t = integer_ty
+ let name = "E_ACSL.New_typing.t"
+ let reprs = [ Gmp; c_int ]
+ include Datatype.Undefined
+
+ let compare ty1 ty2 = match ty1, ty2 with
+ | C_type i1, C_type i2 ->
+ if i1 = i2 then 0
+ else if Cil.intTypeIncluded i1 i2 then -1 else 1
+ | (Other | C_type _), Gmp | Other, C_type _ -> -1
+ | Gmp, (C_type _ | Other) | C_type _, Other -> 1
+ | Gmp, Gmp | Other, Other -> 0
+
+ let equal = Datatype.from_compare
+
+ let hash = function
+ | Gmp -> 787
+ | Other -> 1011
+ | C_type ik -> Hashtbl.hash ik
+
+ let pretty fmt = function
+ | Gmp -> Format.pp_print_string fmt "GMP"
+ | C_type k -> Printer.pp_ikind fmt k
+ | Other -> Format.pp_print_string fmt "OTHER"
+ end)
(******************************************************************************)
(** Basic operations *)
@@ -94,14 +100,20 @@ 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 *)
(******************************************************************************)
type computed_info =
- { ty: t; (* type required for the term *)
- op: t; (* type required for the operation *)
- cast: t option; (* if not [None], type of the context which the term
+ { ty: D.t; (* type required for the term *)
+ op: D.t; (* type required for the operation *)
+ cast: D.t option; (* if not [None], type of the context which the term
must be casted to. If [None], no cast needed. *)
}
@@ -171,38 +183,24 @@ 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
- (* convert the kind to [IInt] whenever smaller. *)
- let kind = if Cil.intTypeIncluded itv_kind IInt then IInt else itv_kind in
+ let kind = Interval.ikind_of_interv i in
(* ctx type whenever possible to prevent superfluous casts in the generated
code *)
(match ctx with
| None | Some (Gmp | Other) -> C_type kind
| Some (C_type ik as ctx) ->
- if Cil.intTypeIncluded itv_kind ik then ctx else C_type kind)
+ if Cil.intTypeIncluded kind ik then ctx else C_type kind)
with Cil.Not_representable ->
Gmp
(* compute a new {!computed_info} by coercing the given type [ty] to the given
context [ctx]. [op] is the type for the operator. *)
let coerce ~arith_operand ~ctx ~op ty =
- if compare ty ctx = 1 then begin
+ if D.compare ty ctx = 1 then
(* type larger than the expected context,
so we must introduce an explicit cast *)
{ ty; op; cast = Some ctx }
- end else
+ else
(* only add an explicit cast if the context is [Gmp] and [ty] is not;
or if the term corresponding to [ty] is an operand of an arithmetic
operation which must be explicitly coerced in order to force the
@@ -356,7 +354,7 @@ let rec type_term ~use_gmp_opt ?(arith_operand=false) ?ctx t =
dup ctx_res
| TBinOp ((Lt | Gt | Le | Ge | Eq | Ne), t1, t2) ->
- assert (match ctx with None -> true | Some c -> compare c c_int >= 0);
+ assert (match ctx with None -> true | Some c -> D.compare c c_int >= 0);
let ctx =
try
let i1 = Interval.infer t1 in
@@ -462,14 +460,55 @@ 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))
+ if Builtins.mem li.l_var_info.lv_name then
+ let typ_arg lvi arg =
+ (* a built-in is a C function, so the context is necessarily a C
+ type. *)
+ 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))
+ else begin
+ (* TODO: what if the type of the parameter is smaller than the infered
+ type of the argument? For now, it is silently ignored (both
+ statically and at runtime)... *)
+ List.iter (fun arg -> ignore (type_term ~use_gmp_opt:true arg)) args;
+ (* TODO: recursive call in arguments of function call *)
+ match li.l_body with
+ | LBpred _ ->
+ (* possible to 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 ->
+ 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
+ | 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 +567,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) ->
@@ -637,7 +687,7 @@ let rec type_predicate p =
let type_term ~use_gmp_opt ?ctx t =
Options.feedback ~dkey ~level:4 "typing term '%a' in ctx '%a'."
- Printer.pp_term t (Pretty_utils.pp_opt pretty) ctx;
+ Printer.pp_term t (Pretty_utils.pp_opt D.pretty) ctx;
ignore (type_term ~use_gmp_opt ?ctx t)
let type_named_predicate ?(must_clear=true) p =
@@ -694,6 +744,8 @@ let get_cast_of_predicate p =
let clear = Memo.clear
+module Datatype = D
+
(*
Local Variables:
compile-command: "make"
diff --git a/src/plugins/e-acsl/typing.mli b/src/plugins/e-acsl/typing.mli
index 8182360e77e376bfb86627f152fc2e3377706b13..a6387e848d2822859c11a1c63f269b19890f3e0d 100644
--- a/src/plugins/e-acsl/typing.mli
+++ b/src/plugins/e-acsl/typing.mli
@@ -56,7 +56,7 @@ type integer_ty = private
| C_type of ikind
| Other (** Any non-integral type *)
-val pretty: Format.formatter -> integer_ty -> unit
+module Datatype: Datatype.S_with_collections with type t = integer_ty
(** {3 Smart constructors} *)
@@ -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
@@ -88,8 +91,8 @@ val join: integer_ty -> integer_ty -> integer_ty
val type_term: use_gmp_opt:bool -> ?ctx:integer_ty -> term -> unit
(** Compute the type of each subterm of the given term in the given context. If
- [use_gmp_opt] is false, then the conversion to the given context is done even if
- -e-acsl-gmp-only is set. *)
+ [use_gmp_opt] is false, then the conversion to the given context is done
+ even if -e-acsl-gmp-only is set. *)
val type_named_predicate: ?must_clear:bool -> predicate -> unit
(** Compute the type of each term of the given predicate.
@@ -132,15 +135,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 a512b5eb8e5a89bf17ffd6b3810e578e8cc625dc..077f9360eb9db2b22253a05fcfdac5907a7aedcb 100644
--- a/src/plugins/e-acsl/visit.ml
+++ b/src/plugins/e-acsl/visit.ml
@@ -453,7 +453,12 @@ you must call function `%s' and `__e_acsl_memory_clean by yourself.@]"
in
Extlib.may handle_main main_fct
in
- Project.on prj build_mmodel_initializer ();
+ Project.on
+ prj
+ (fun () ->
+ f.globals <- Logic_functions.add_generated_functions f.globals;
+ build_mmodel_initializer ())
+ ();
(* reset copied states at the end to be observationally
equivalent to a standard visitor. *)
Project.clear ~selection ~project:prj ();
@@ -468,8 +473,9 @@ you must call function `%s' and `__e_acsl_memory_clean by yourself.@]"
Cil.JustCopyPost
(fun l ->
let new_vi = Cil.get_varinfo self#behavior vi in
- Misc.register_library_function new_vi;
- Builtins.update vi.vname new_vi;
+ if Misc.is_library_loc vi.vdecl then
+ Misc.register_library_function new_vi;
+ if Builtins.mem vi.vname then Builtins.update vi.vname new_vi;
l)
else begin
Misc.register_library_function vi;
@@ -561,9 +567,10 @@ you must call function `%s' and `__e_acsl_memory_clean by yourself.@]"
let locals, blocks =
List.fold_left
(fun (local_vars, block_vars as acc) (v, scope) -> match scope with
- | Env.Global -> acc
- | Env.Function -> v :: local_vars, v :: block_vars
- | Env.Local_block -> v :: local_vars, block_vars)
+ (* TODO: [kf] assumed to be consistent. Should be asserted. *)
+ | Env.LFunction _kf -> v :: local_vars, v :: block_vars
+ | Env.LLocal_block _kf -> v :: local_vars, block_vars
+ | _ -> acc)
(f.slocals, f.sbody.blocals)
vars
in
@@ -1020,6 +1027,7 @@ you must call function `%s' and `__e_acsl_memory_clean by yourself.@]"
initializer
Misc.reset ();
+ Logic_functions.reset ();
Literal_strings.reset ();
Global_observer.reset ();
Keep_status.before_translation ();