Commit 3e1613da authored by Julien Signoles's avatar Julien Signoles
Browse files

[translate] better code generation for logic function calls

parent 9754ec52
......@@ -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
......@@ -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
......
......@@ -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
......@@ -299,8 +320,7 @@ module Logic_binding = struct
| 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
Format.asprintf "logic variable of type %a" Logic_type.pretty lty
in
Error.not_yet msg
in
......@@ -324,26 +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 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
module Logic_scope = struct
let get env = env.lscope
let extend env lvs = { env with lscope = Lscope.add lvs env.lscope }
......@@ -512,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 }
......
......@@ -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
......@@ -75,8 +80,9 @@ module Logic_binding: sig
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
......@@ -115,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
......
......@@ -54,7 +54,8 @@ let t_ptr () = TNamed(
},
[])
let is_t ty = Cil_datatype.Typ.equal ty (t ())
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
......
......@@ -348,7 +348,7 @@ and infer_term_lval (host, offset as tlv) =
let ty = Logic_utils.logicCType (Cil.typeOfTermLval tlv) in
interv_of_typ ty
and infer_term_host h = match h with
and infer_term_host = function
| TVar v ->
(try Env.find v
with Not_found ->
......
......@@ -131,10 +131,11 @@ 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 ->
Options.fatal "[keep_status] unbound function" Datatype.String.pretty kf
(* try*) Datatype.String.Hashtbl.find keep_status name
(* with Not_found ->
Options.fatal "[keep_status] unbound function" Datatype.String.pretty kf*)
in
info.cpt <- info.cpt + 1;
let kind', keep =
......@@ -148,3 +149,4 @@ let must_translate kf kind =
pretty_kind kind
pretty_kind kind';
keep
with Not_found -> true
This diff is collapsed.
......@@ -34,25 +34,23 @@ open Cil_types
(************** Logic functions without labels ****************************)
(**************************************************************************)
val generate: loc:location -> Env.t -> term -> logic_info ->
exp list -> logic_type list -> varinfo * exp * Env.t
(** [generate ~loc env t_app li args_exp args_lty] generates the C function
corresponding to [t_app] and returns the associated call. *)
val reset: unit -> unit
val do_visit: Cil_types.file -> unit
(** Put declarations and definitions of the generated functions in the AST. *)
val tapp_to_exp:
loc:location ->
string -> Env.t -> term -> logic_info -> Typing.integer_ty list -> exp list ->
varinfo * exp * Env.t
val reset: unit -> unit
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 predicate_to_exp_ref:
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
val add_cast_ref:
(location -> Env.t -> typ option -> bool -> exp -> exp * Env.t) ref
......@@ -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 _ :: _ ->
......
......@@ -18,13 +18,13 @@
6; */
int main (void) {
/*@ assert f1(0) == 0; */ ;
/*@ assert f1(1) == 1; */ ;
/*@ assert f1(100) == 5050; */ ;
// /*@ assert f1(0) == 0; */ ;
// /*@ assert f1(1) == 1; */ ;
// /*@ assert f1(100) == 5050; */ ;
/*@ assert f2(7) == 1; */ ;
/*@ assert f2(7) == 1; */ ;
/*@ assert f3(6) == -5; */ ;
/*@assert f4(9) > 0; */ ;
/*@ assert f4(9) > 0; */ ;
}
......@@ -14,7 +14,6 @@
[eva] using specification for function __e_acsl_memory_init
[eva] using specification for function __e_acsl_assert
[eva] using specification for function __gmpz_init_set_str
[eva] using specification for function __gmpz_init_set
[eva] using specification for function __gmpz_init_set_si
[eva] using specification for function __gmpz_init
[eva] using specification for function __gmpz_add
......@@ -24,9 +23,9 @@
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:
accessing uninitialized left-value.
assert \initialized((__e_acsl_mpz_struct *)__gen_e_acsl_f1_tapp_3);
[eva:alarm] :0: Warning:
function __gmpz_init_set: precondition ¬\initialized(z) got status invalid.
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
......@@ -23,12 +23,28 @@
[eva:alarm] tests/gmp/functions.c:43: Warning:
function __e_acsl_assert: precondition got status unknown.
[eva] using specification for function __gmpz_init_set_str
[eva] using specification for function __gmpz_init_set
[eva:alarm] tests/gmp/functions.c:44: Warning:
function __e_acsl_assert: precondition got status unknown.
[eva] 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_tapp);
[eva:alarm] :0: Warning:
function __gmpz_init_set: precondition ¬\initialized(z) got status invalid.
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
......@@ -10,16 +10,78 @@
__e_acsl_math_HUGE_VALF ∈ [-3.40282346639e+38 .. 3.40282346639e+38]
__e_acsl_math_INFINITY ∈ [-1.79769313486e+308 .. 1.79769313486e+308]
[eva] using specification for function __e_acsl_memory_init
[eva] tests/gmp/functions_rec.c:21:
cannot evaluate ACSL term, unsupported ACSL construct: logic function f1
[eva:alarm] tests/gmp/functions_rec.c:21: Warning: assertion got status unknown.
[eva] using specification for function __gmpz_init
[eva:alarm] tests/gmp/functions_rec.c:21: Warning:
accessing uninitialized left-value.
assert \initialized((__e_acsl_mpz_struct *)__gen_e_acsl_f1_tapp);
[eva] using specification for function __gmpz_init_set_si
[eva] using specification for function __gmpz_init_set
[eva] using specification for function __gmpz_clear
[eva:alarm] :0: Warning:
function __gmpz_init_set: precondition ¬\initialized(z) got status invalid.
[eva] tests/gmp/functions_rec.c:25:
cannot evaluate ACSL term, unsupported ACSL construct: logic function f2
[eva:alarm] tests/gmp/functions_rec.c:25: Warning: assertion got status unknown.
[eva] tests/gmp/functions_rec.c:9: 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:9 <-
__gen_e_acsl_f2 :: tests/gmp/functions_rec.c:25 <-
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:9: 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:9 <-
__gen_e_acsl_f2 :: tests/gmp/functions_rec.c:25 <-
main).
Assuming the call has no effect. The analysis will be unsound.
[eva] tests/gmp/functions_rec.c:9: 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:9 <-
__gen_e_acsl_f2 :: tests/gmp/functions_rec.c:25 <-
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:9: Warning:
function __e_acsl_assert: precondition got status unknown.
[eva:alarm] tests/gmp/functions_rec.c:9: Warning:
division by zero. assert __gen_e_acsl_f2_8 ≢ 0;
[eva:alarm] tests/gmp/functions_rec.c:9: Warning:
signed overflow.
assert -2147483648 ≤ __gen_e_acsl_f2_4 * __gen_e_acsl_f2_6;
[eva:alarm] tests/gmp/functions_rec.c:9: Warning:
signed overflow. assert __gen_e_acsl_f2_4 * __gen_e_acsl_f2_6 ≤ 2147483647;
[eva:alarm] tests/gmp/functions_rec.c:9: 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:9: Warning:
division by zero. assert __gen_e_acsl_f2_13 ≢ 0;
[eva:alarm] tests/gmp/functions_rec.c:9: Warning:
signed overflow.
assert -2147483648 ≤ __gen_e_acsl_f2_9 * __gen_e_acsl_f2_11;
[eva:alarm] tests/gmp/functions_rec.c:9: Warning:
signed overflow.
assert __gen_e_acsl_f2_9 * __gen_e_acsl_f2_11 ≤ 2147483647;
[eva:alarm] tests/gmp/functions_rec.c:9: 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:25: Warning:
function __e_acsl_assert: precondition got status unknown.
[eva] tests/gmp/functions_rec.c:27:
cannot evaluate ACSL term, unsupported ACSL construct: logic function f3
[eva:alarm] tests/gmp/functions_rec.c:27: Warning: assertion got status unknown.
[eva] tests/gmp/functions_rec.c:13: 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:13 <-
__gen_e_acsl_f3 :: tests/gmp/functions_rec.c:27 <-
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:29:
cannot evaluate ACSL term, unsupported ACSL construct: logic function f4
[eva:alarm] tests/gmp/functions_rec.c:29: Warning: assertion got status unknown.
[eva] tests/gmp/functions_rec.c:16: 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:16 <-
__gen_e_acsl_f4 :: tests/gmp/functions_rec.c:29 <-
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:29: Warning:
function __e_acsl_assert: precondition got status unknown.
[eva] done for function main
......@@ -10,38 +10,107 @@
__e_acsl_math_HUGE_VALF ∈ [-3.40282346639e+38 .. 3.40282346639e+38]
__e_acsl_math_INFINITY ∈ [-1.79769313486e+308 .. 1.79769313486e+308]
[eva] using specification for function __e_acsl_memory_init
[eva] tests/gmp/functions_rec.c:21:
cannot evaluate ACSL term, unsupported ACSL construct: logic function f1
[eva:alarm] tests/gmp/functions_rec.c:21: Warning: assertion got status unknown.
[eva] using specification for function __gmpz_init
[eva:alarm] tests/gmp/functions_rec.c:21: Warning:
accessing uninitialized left-value.
assert \initialized((__e_acsl_mpz_struct *)__gen_e_acsl_f1_tapp);
[eva] tests/gmp/functions_rec.c:25:
cannot evaluate ACSL term, unsupported ACSL construct: logic function f2
[eva:alarm] tests/gmp/functions_rec.c:25: 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:6: Warning:
[eva:alarm] tests/gmp/functions_rec.c:9: Warning:
accessing uninitialized left-value.
assert \initialized((__e_acsl_mpz_struct *)__gen_e_acsl_sub);
[eva:alarm] tests/gmp/functions_rec.c:6: Warning:
accessing uninitialized left-value.
assert \initialized((__e_acsl_mpz_struct *)__gen_e_acsl_f1_tapp_2);
[eva] tests/gmp/functions_rec.c:6: Warning:
[eva] tests/gmp/functions_rec.c:9: Warning:
recursive call during value analysis
of __gen_e_acsl_f1_2 (__gen_e_acsl_f1_2 <- __gen_e_acsl_f1_2 :: tests/gmp/functions_rec.c:6 <-
__gen_e_acsl_f1 :: tests/gmp/functions_rec.c:21 <-
of __gen_e_acsl_f2_2 (__gen_e_acsl_f2_2 <- __gen_e_acsl_f2_2 :: tests/gmp/functions_rec.c:9 <-
__gen_e_acsl_f2 :: tests/gmp/functions_rec.c:25 <-
main).
Assuming the call has no effect. The analysis will be unsound.
[eva:alarm] tests/gmp/functions_rec.c:6: Warning:
[eva:alarm] tests/gmp/functions_rec.c:9: Warning:
accessing uninitialized left-value.
assert \initialized((__e_acsl_mpz_struct *)__gen_e_acsl_sub_2);
[eva:alarm] tests/gmp/functions_rec.c:6: Warning:
[eva] using specification for function __gen_e_acsl_f2_2
[eva] tests/gmp/functions_rec.c:9: 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:9 <-
__gen_e_acsl_f2 :: tests/gmp/functions_rec.c:25 <-
main).
Assuming the call has no effect. The analysis will be unsound.
[eva:alarm] tests/gmp/functions_rec.c:9: 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:9: 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:9 <-
__gen_e_acsl_f2 :: tests/gmp/functions_rec.c:25 <-
main).
Assuming the call has no effect. The analysis will be unsound.
[eva:alarm] tests/gmp/functions_rec.c:9: 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:9: Warning:
assertion 'E_ACSL' got status unknown.
[eva] using specification for function __e_acsl_assert
[eva:alarm] tests/gmp/functions_rec.c:9: Warning:
function __e_acsl_assert: precondition got status unknown.
[eva] using specification for function __gmpz_tdiv_q
[eva:alarm] tests/gmp/functions_rec.c:9: Warning:
accessing uninitialized left-value.
assert \initialized((__e_acsl_mpz_struct *)__gen_e_acsl_sub_5);
[eva:alarm] tests/gmp/functions_rec.c:9: Warning:
accessing uninitialized left-v