Commit 74c8f25f authored by Fonenantsoa Maurica 's avatar Fonenantsoa Maurica
Browse files

Addresses Julien's review no.3 (part 1/2):

 - Sad goodbye to insert_before_element_under_condition
 - ~label instead of ~pre
 - No superfluous Env.Varname.get
 - Gmp only allowed
 - Dataflow analysis allowed
 - Using exception for term_has_lv_from_vi
 - Fix incorrect assert false from effective_lscope_from_pred_or_term
 - fold_left for index_from_sizes_and_shifts
parent 78f9aaab
......@@ -38,33 +38,31 @@ let term_to_exp_ref
(**************************** Handling memory ********************************)
(*****************************************************************************)
let tbl_malloc: stmt Cil_datatype.Kf.Hashtbl.t =
Cil_datatype.Kf.Hashtbl.create 7
let tbl_free: stmt Cil_datatype.Kf.Hashtbl.t =
Cil_datatype.Kf.Hashtbl.create 7
let add_malloc kf stmt = Cil_datatype.Kf.Hashtbl.add tbl_malloc kf stmt
let add_free kf stmt = Cil_datatype.Kf.Hashtbl.add tbl_free kf stmt
let get_mallocs kf = Cil_datatype.Kf.Hashtbl.find_all tbl_malloc kf
let get_frees kf = Cil_datatype.Kf.Hashtbl.find_all tbl_free kf
(* Remove all the bindings for [kf]. [Cil_datatype.Kf.Hashtbl] does not
provide the [remove_all] function. Thus we need to keep calling [remove]
until all entries are removed. *)
let rec remove_mallocs_and_frees kf =
let rec remove_all tbl kf =
try
ignore
(Cil_datatype.Kf.Hashtbl.find tbl_malloc kf); (* [tbl_free] is also ok *)
Cil_datatype.Kf.Hashtbl.remove tbl_malloc kf;
Cil_datatype.Kf.Hashtbl.remove tbl_free kf;
remove_mallocs_and_frees kf;
ignore(Cil_datatype.Kf.Hashtbl.find tbl kf);
Cil_datatype.Kf.Hashtbl.remove tbl kf;
remove_all tbl kf;
with Not_found ->
()
module Malloc = struct
let tbl = Cil_datatype.Kf.Hashtbl.create 7
let add kf stmt = Cil_datatype.Kf.Hashtbl.add tbl kf stmt
let find_all kf = Cil_datatype.Kf.Hashtbl.find_all tbl kf
let remove_all kf = remove_all tbl kf
end
module Free = struct
let tbl = Cil_datatype.Kf.Hashtbl.create 7
let add kf stmt = Cil_datatype.Kf.Hashtbl.add tbl kf stmt
let find_all kf = Cil_datatype.Kf.Hashtbl.find_all tbl kf
let remove_all kf = remove_all tbl kf
end
(**************************************************************************)
(*************************** Translation **********************************)
(**************************************************************************)
......@@ -83,8 +81,8 @@ let rec sizes_and_shifts_from_quantifs ~loc kf lscope sizes_and_shifts =
Error.not_yet "\\at with logic variable linked to C variable"
| Lscope.Lvs_quantif(tmin, lv, tmax) :: lscope' ->
let t_size = Logic_const.term ~loc (TBinOp(MinusA, tmax, tmin)) Linteger in
let t_size = Logic_const.term
~loc (TBinOp(PlusA, t_size, Cil.lone ~loc ())) Linteger
let t_size =
Logic_const.term ~loc (TBinOp(PlusA, t_size, Cil.lone ~loc ())) Linteger
in
let i = Interval.infer t_size in
(* The EXACT amount of memory that is needed can be known at runtime. This
......@@ -115,8 +113,8 @@ let rec sizes_and_shifts_from_quantifs ~loc kf lscope sizes_and_shifts =
in
(* Index *)
let t_lv = Logic_const.tvar ~loc lv in
let t_shifted = Logic_const.term
~loc (TBinOp(MinusA, t_lv, tmin)) Linteger
let t_shifted =
Logic_const.term ~loc (TBinOp(MinusA, t_lv, tmin)) Linteger
in
(* Returning *)
let sizes_and_shifts = (t_size, t_shifted) :: sizes_and_shifts in
......@@ -146,8 +144,8 @@ let size_from_sizes_and_shifts ~loc = function
let append_block_of_env_to_block env block =
let block_stmt = Cil.mkStmt ~valid_sid:true (Block block) in
let block, env = Env.pop_and_get
env block_stmt ~global_clear:false Env.After
let block, env =
Env.pop_and_get env block_stmt ~global_clear:false Env.After
in
block, env
......@@ -179,8 +177,8 @@ let rec mk_storing_loops ~loc kf env lscope (e_at, vi_at, t_index) pot =
let storing_stmt =
Cil.mkStmtOneInstr ~valid_sid:true (Set(lval, e, loc))
in
let block, env = Env.pop_and_get
env storing_stmt ~global_clear:false Env.After
let block, env =
Env.pop_and_get env storing_stmt ~global_clear:false Env.After
in
block, env
| [], Misc.PoT_term t ->
......@@ -192,8 +190,8 @@ let rec mk_storing_loops ~loc kf env lscope (e_at, vi_at, t_index) pot =
let storing_stmt =
Cil.mkStmtOneInstr ~valid_sid:true (Set(lval, e, loc))
in
let block, env = Env.pop_and_get
env storing_stmt ~global_clear:false Env.After
let block, env =
Env.pop_and_get env storing_stmt ~global_clear:false Env.After
in
block, env
| Typing.Gmp ->
......@@ -209,8 +207,8 @@ let rec mk_storing_loops ~loc kf env lscope (e_at, vi_at, t_index) pot =
in
let t_lv = Logic_const.tvar ~loc lv in
(* Guard *)
let guard = Logic_const.term
~loc (TBinOp(Le, t_lv, tmax)) (Ctype Cil.intType)
let guard =
Logic_const.term ~loc (TBinOp(Le, t_lv, tmax)) (Ctype Cil.intType)
in
Typing.type_term ~use_gmp_opt:false ~ctx:Typing.c_int guard;
let guard_exp, env = term_to_exp kf env guard in
......@@ -230,16 +228,16 @@ let rec mk_storing_loops ~loc kf env lscope (e_at, vi_at, t_index) pot =
Typing.type_term ~use_gmp_opt:true plus_one_term;
let plus_one_exp, env = term_to_exp kf env plus_one_term in
let plus_one_stmt = match Typing.get_integer_ty plus_one_term with
| Typing.C_type _ | Typing.Gmp->
Gmpz.init_set ~loc (Cil.var vi_of_lv) (Cil.evar vi_of_lv) plus_one_exp
| Typing.Other ->
assert false
| Typing.C_type _ | Typing.Gmp ->
Gmpz.init_set ~loc (Cil.var vi_of_lv) (Cil.evar vi_of_lv) plus_one_exp
| Typing.Other ->
assert false
in
(* If guard is satisfiable then inner loop, else break *)
let if_stmt = Cil.mkStmt
~valid_sid:true
(If(guard_exp,
Cil.mkBlock [loop'; plus_one_stmt],
Cil.mkBlock [ loop'; plus_one_stmt ],
Cil.mkBlock [ break_stmt ],
guard_exp.eloc))
in
......@@ -254,10 +252,10 @@ let rec mk_storing_loops ~loc kf env lscope (e_at, vi_at, t_index) pot =
(* Init lv *)
let tmin_exp, env = term_to_exp kf env tmin in
let set_tmin = match Typing.get_integer_ty plus_one_term with
| Typing.C_type _ | Typing.Gmp ->
Gmpz.init_set ~loc (Cil.var vi_of_lv) (Cil.evar vi_of_lv) tmin_exp
| Typing.Other ->
assert false
| Typing.C_type _ | Typing.Gmp ->
Gmpz.init_set ~loc (Cil.var vi_of_lv) (Cil.evar vi_of_lv) tmin_exp
| Typing.Other ->
assert false
in
(* The whole block *)
let block = Cil.mkBlock [set_tmin; loop] in
......@@ -272,9 +270,7 @@ let rec mk_storing_loops ~loc kf env lscope (e_at, vi_at, t_index) pot =
Env.Logic_binding.add ~ty:vi_of_lv_old.vtype env lv
in
let e, env = term_to_exp kf env t in
let let_stmt = Gmpz.init_set
~loc (Cil.var vi_of_lv) exp_of_lv e
in
let let_stmt = Gmpz.init_set ~loc (Cil.var vi_of_lv) exp_of_lv e in
let block, env =
mk_storing_loops ~loc kf env lscope' (e_at, vi_at, t_index) pot
in
......@@ -297,23 +293,29 @@ let rec mk_storing_loops ~loc kf env lscope (e_at, vi_at, t_index) pot =
To (t_shifted_n, t_shifted_n-1, ..., t_shifted_1)
where 0 <= t_shifted_i < beta_i
corresponds: \sum_{i=1}^n( t_shifted_i * \pi_{j=1}^{i-1}(beta_j) ) *)
let rec index_from_sizes_and_shifts ~loc sizes_and_shifts =
match sizes_and_shifts with
| [] ->
Cil.lzero ~loc ()
| (_, t_shifted) :: sizes_and_shifts' ->
let index' = index_from_sizes_and_shifts ~loc sizes_and_shifts' in
let pi_beta_j sizes_and_shifts = List.fold_left
(fun pi_beta_j (t_size, _) ->
Logic_const.term ~loc (TBinOp(Mult, pi_beta_j, t_size)) Linteger)
(Cil.lone ~loc ())
sizes_and_shifts
in
let pi_beta_j = pi_beta_j sizes_and_shifts' in
let bi_mult_pi_beta_j = Logic_const.term ~loc
(TBinOp(Mult, t_shifted, pi_beta_j)) Linteger
in
Logic_const.term ~loc (TBinOp(PlusA, bi_mult_pi_beta_j, index')) Linteger
let index_from_sizes_and_shifts ~loc sizes_and_shifts =
let sum, _ = List.fold_left
(fun (index, sizes) (t_size, t_shifted) ->
let pi_beta_j sizes = List.fold_left
(fun pi_beta_j t_size ->
Logic_const.term ~loc (TBinOp(Mult, pi_beta_j, t_size)) Linteger)
(Cil.lone ~loc ())
sizes
in
let pi_beta_j = pi_beta_j sizes in
let bi_mult_pi_beta_j =
Logic_const.term ~loc (TBinOp(Mult, t_shifted, pi_beta_j)) Linteger
in
let sum = Logic_const.term
~loc
(TBinOp(PlusA, bi_mult_pi_beta_j, index))
Linteger
in
sum, t_size :: sizes)
(Cil.lzero ~loc (), [])
sizes_and_shifts
in
sum
let put_block_at_label env block label =
let stmt = Label.get_stmt (Env.get_visitor env) label in
......@@ -322,21 +324,15 @@ let put_block_at_label env block label =
inherit Visitor.frama_c_inplace
method !vstmt_aux stmt =
assert (!env_ref == env);
let pre = Env.pre_from_label label in
env_ref := Env.extend_stmt_in_place env stmt ~pre block;
env_ref := Env.extend_stmt_in_place env stmt ~label block;
Cil.ChangeTo stmt
end
in
let bhv = Env.get_behavior env in
ignore( Visitor.visitFramacStmt o (Cil.get_stmt bhv stmt));
ignore(Visitor.visitFramacStmt o (Cil.get_stmt bhv stmt));
!env_ref
let to_exp ~loc kf env pot label =
if not (Options.Full_mmodel.get ()) then
Error.not_yet
"\\at on purely logic variables but without full memory model";
if Options.Gmp_only.get () then
Error.not_yet "\\at on purely logic variables and with gmp only";
let term_to_exp = !term_to_exp_ref in
let lscope_vars = Lscope.get_all (Env.Logic_scope.get env) in
let sizes_and_shifts =
......@@ -355,10 +351,9 @@ let to_exp ~loc kf env pot label =
end
in
let ty_ptr = TPtr(ty, []) in
let name = Env.Varname.get ~scope:Env.Function "at" in
let vi_at, e_at, env = Env.new_var
~loc
~name
~name:"at"
~scope:Env.Function
env
None
......@@ -368,10 +363,10 @@ let to_exp ~loc kf env pot label =
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
let t_size =
Logic_const.term ~loc (TBinOp(Mult, t_sizeof, t_size)) lty_sizeof
in
Typing.type_term ~use_gmp_opt:true t_size;
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
......@@ -385,15 +380,16 @@ let to_exp ~loc kf env pot label =
("\\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"
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. *)
add_malloc kf malloc_stmt;
add_free kf free_stmt;
Malloc.add kf malloc_stmt;
Free.add kf free_stmt;
[])
in
(* Index *)
......
......@@ -42,14 +42,21 @@ val to_exp:
stored in a memory location that needs to be alloted then freed.
This part is designed for that purpose. *)
val get_mallocs: kernel_function -> stmt list
(* Get the list of [malloc] stmts that need to be inserted into [kf]. *)
module Malloc: sig
val find_all: kernel_function -> stmt list
(* Return the list of [malloc] stmts that need to be inserted into [kf]. *)
val get_frees: kernel_function -> stmt list
(* Get the list of [malloc] stmts that need to be inserted into [kf]. *)
val remove_all: kernel_function -> unit
(* Remove all [malloc] stmts for [kf] from the internal table. *)
end
val remove_mallocs_and_frees: kernel_function -> unit
(* Remove all [malloc] and [free] stmts for [kf] from the internal table. *)
module Free: sig
val find_all: kernel_function -> stmt list
(* Return the list of [free] stmts that need to be inserted into [kf]. *)
val remove_all: kernel_function -> unit
(* Remove all [free] stmts for [kf] from the internal table. *)
end
(**************************************************************************)
(********************** Forward references ********************************)
......
......@@ -364,12 +364,17 @@ let add_stmt ?(post=false) ?(init=false) ?before env stmt =
init_env = if init then local_env else env.init_env;
env_stack = if init then env.env_stack else local_env :: tl }
let extend_stmt_in_place env stmt ~pre block =
let extend_stmt_in_place env stmt ~label block =
let new_stmt = Cil.mkStmt ~valid_sid:true (Block block) in
let sk = stmt.skind in
stmt.skind <-
stmt.skind <-
Block (Cil.mkBlock [ new_stmt; Cil.mkStmt ~valid_sid:true sk ]);
if pre then
let pre = match label with
| BuiltinLabel(Here | Post) -> true
| BuiltinLabel(Old | Pre | LoopEntry | LoopCurrent | Init)
| FormalLabel _ | StmtLabel _ -> false
in
if pre then
let local_env, tl_env = top false env in
let b_info = local_env.block_info in
let b_info = { b_info with pre_stmts = new_stmt :: b_info.pre_stmts } in
......@@ -377,11 +382,6 @@ let extend_stmt_in_place env stmt ~pre block =
else
env
let pre_from_label = function
| BuiltinLabel(Here | Post) -> true
| BuiltinLabel(Old | Pre | LoopEntry | LoopCurrent | Init)
| FormalLabel _ | StmtLabel _ -> false
let push env =
(* Options.feedback "push (was %d)" (List.length env.env_stack);*)
{ env with env_stack = empty_local_env :: env.env_stack }
......
......@@ -81,15 +81,11 @@ val add_stmt: ?post:bool -> ?init:bool -> ?before:stmt -> t -> stmt -> t
say that any labels attached to [before] are moved to [stmt]. [post]
indicates that [stmt] should be added after the target statement. *)
val extend_stmt_in_place: t -> stmt -> pre:bool -> block -> t
(** [extend_stmt_in_place env stmt ~pre b] modifies [stmt] in place in order to
add the given [block]. If [pre] is [true], then this block is guaranteed
to be at the first place of the resulting [stmt] whatever modification
will be done by the visitor later. *)
val pre_from_label: logic_label -> bool
(** Computes the value of [pre] to provide to [extend_stmt_in_place] from
the given logic label. *)
val extend_stmt_in_place: t -> stmt -> label:logic_label -> block -> t
(** [extend_stmt_in_place env stmt ~label b] modifies [stmt] in place in
order to add the given [block]. If [pre] is [Here] or [Post],
then this block is guaranteed to be at the first place of the resulting
[stmt] whatever modification will be done by the visitor later. *)
val push: t -> t
(** Push a new local context in the environment *)
......
......@@ -39,13 +39,13 @@ let add lscope_var t = lscope_var :: t
let get_all t = List.rev t
let get_lscope_var lv t =
let find lv t =
let is_lv = function
| Lvs_let(lv', _) | Lvs_quantif(_, lv', _) | Lvs_formal(lv', _)
| Lvs_global(lv', _) ->
Cil_datatype.Logic_var.equal lv lv'
in
try List.find is_lv t with Not_found -> assert false
List.find is_lv t
let effective_lscope_from_pred_or_term pot potential_lscope =
let effective_lscope = ref empty in
......@@ -57,8 +57,11 @@ let effective_lscope_from_pred_or_term pot potential_lscope =
[effective_lscope] which only tracks purely logic variables. *)
()
| None ->
let lscope_var = get_lscope_var lv potential_lscope in
effective_lscope := add lscope_var !effective_lscope
try
let lscope_var = find lv potential_lscope in
effective_lscope := add lscope_var !effective_lscope
with Not_found ->
()
end;
Cil.DoChildren
end
......
......@@ -290,39 +290,22 @@ let is_bitfield_pointers lty =
else
is_bitfield_pointer lty
exception Lv_from_vi_found
let term_has_lv_from_vi t =
let res_ref = ref false in
let o = object inherit Visitor.frama_c_inplace
method !vlogic_var_use lv =
match lv.lv_origin with
| None ->
Cil.DoChildren
| Some _ ->
res_ref := true;
Cil.SkipChildren
end
in
ignore (Visitor.visitFramacTerm o t);
!res_ref
try
let o = object inherit Visitor.frama_c_inplace
method !vlogic_var_use lv = match lv.lv_origin with
| None -> Cil.DoChildren
| Some _ -> raise Lv_from_vi_found
end
in
ignore (Visitor.visitFramacTerm o t);
false
with Lv_from_vi_found ->
true
type pred_or_term = PoT_pred of predicate | PoT_term of term
let insert_before_element_under_condition elements to_insert condition =
let elements_with_insertions_rev = List.fold_left
(fun elements element ->
if condition element then
element :: List.fold_left
(fun elements_with_insertions element_to_insert ->
element_to_insert :: elements_with_insertions)
elements
to_insert
else
element :: elements)
[]
elements
in
List.rev elements_with_insertions_rev
(*
Local Variables:
compile-command: "make"
......
......@@ -115,21 +115,11 @@ val is_bitfield_pointers: logic_type -> bool
set of bitfield pointers. *)
val term_has_lv_from_vi: term -> bool
(* Return [true] iff the given term contains a variables that originated 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 insert_before_element_under_condition:
'a list -> 'a list -> ('a -> bool) -> 'a list
(* [insert_before_element_under_condition elements to_insert condition]
returns [elements] in which [to_insert] have been inserted before each
element of [elements] satisfying [condition].
Its complexity is such that if [N1] is the size of [elements], [N2] that of
[to_insert] and [M] the number of elements satisfying [condition] then
[insert_before_element_under_condition] performs [T=2*(N1+M*N2)] prepends.
Since [T] is also the size of the resulting list, it cannot be lowered. *)
(*
Local Variables:
compile-command: "make"
......
/* run.config
COMMENT: \at with logic variables
COMMENT: For now, only works with full memory model,
and without --gmp-only
COMMENT: \at on purely logic variables
COMMENT:
*/
/*@ ensures \forall integer n; 1 < n <= 3 ==>
......@@ -9,6 +8,14 @@
ensures \let m = 4; \old(t[m] == -4) && \old(t[m - 4]) == 9; */
void f(int *t) {}
void g() {
int m;
m = 8;
Q: ;
m = 10;
/*@ assert \exists integer w; 3 <= w < 6 && \at(m + w == 12, Q); */ ;
}
int main(void) {
int n;
n = 7;
......@@ -37,9 +44,10 @@ int main(void) {
\forall integer v; -5 < v <= (u < 15 ? u + 6 : 3) ==>
\at(n + u + n > 0, K); */ ;
// Function contracts:
// Function calls:
int t[5] = {9, 12, 12, 12, -4};
f(t);
g();
// Not yet:
/*@ assert
......
[e-acsl] beginning translation.
[e-acsl] tests/full-mmodel-only/at_logic-variables.c:47: Warning:
[e-acsl] tests/gmp/at_on-purely-logic-variables.c:55: Warning:
E-ACSL construct
`\at on purely logic variables that needs to allocate too much memory (bigger than int_max bytes)'
is not yet supported.
Ignoring annotation.
[e-acsl] tests/full-mmodel-only/at_logic-variables.c:49: Warning:
[e-acsl] tests/gmp/at_on-purely-logic-variables.c:56: Warning:
E-ACSL construct `\at with logic variable linked to C variable'
is not yet supported.
Ignoring annotation.
......@@ -19,175 +19,194 @@
__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/at_on-purely-logic-variables.c:45:
allocating variable __malloc_main_l45
[eva] tests/gmp/at_on-purely-logic-variables.c:41:
allocating variable __malloc_main_l41
[eva] tests/gmp/at_on-purely-logic-variables.c:37:
allocating variable __malloc_main_l37
[eva] tests/gmp/at_on-purely-logic-variables.c:34:
allocating variable __malloc_main_l34
[eva] tests/gmp/at_on-purely-logic-variables.c:29:
allocating variable __malloc_main_l29
[eva] tests/gmp/at_on-purely-logic-variables.c:28:
allocating variable __malloc_main_l28
[eva] using specification for function __e_acsl_store_block
[eva] using specification for function __e_acsl_full_init
[eva] tests/full-mmodel-only/at_logic-variables.c:38:
allocating variable __malloc_main_l38
[eva] tests/full-mmodel-only/at_logic-variables.c:34:
allocating variable __malloc_main_l34
[eva] tests/full-mmodel-only/at_logic-variables.c:30:
allocating variable __malloc_main_l30
[eva] tests/full-mmodel-only/at_logic-variables.c:27:
allocating variable __malloc_main_l27
[eva] tests/full-mmodel-only/at_logic-variables.c:22:
allocating variable __malloc_main_l22
[eva] tests/full-mmodel-only/at_logic-variables.c:21:
allocating variable __malloc_main_l21
[eva:alarm] tests/full-mmodel-only/at_logic-variables.c:30: Warning:
[eva:alarm] tests/gmp/at_on-purely-logic-variables.c:37: Warning:
out of bounds write. assert \valid(__gen_e_acsl_at_4 + 0);
[eva:alarm] tests/full-mmodel-only/at_logic-variables.c:22: Warning:
[eva:alarm] tests/gmp/at_on-purely-logic-variables.c:29: Warning:
out of bounds write.
assert \valid(__gen_e_acsl_at_2 + (int)(__gen_e_acsl_j_2 - 2));
[eva] tests/full-mmodel-only/at_logic-variables.c:22:
[eva] tests/gmp/at_on-purely-logic-variables.c:29:
starting to merge loop iterations
[eva:alarm] tests/full-mmodel-only/at_logic-variables.c:21: Warning:
[eva:alarm] tests/gmp/at_on-purely-logic-variables.c:28: Warning:
out of bounds write. assert \valid(__gen_e_acsl_at + 0);
[eva:alarm] tests/full-mmodel-only/at_logic-variables.c:38: Warning:
[eva:alarm] tests/gmp/at_on-purely-logic-variables.c:45: Warning:
out of bounds write.
assert
\valid(__gen_e_acsl_at_6 +
(int)((int)((int)(__gen_e_acsl_v_4 - -4) * 12) +
(int)(__gen_e_acsl_u_4 - 9)));
[eva] tests/full-mmodel-only/at_logic-variables.c:38:
(int)((int)((int)(__gen_e_acsl_u_4 - 9) * 32) +
(int)(__gen_e_acsl_v_4 - -4)));
[eva] tests/gmp/at_on-purely-logic-variables.c:45:
starting to merge loop iterations
[eva:alarm] tests/full-mmodel-only/at_logic-variables.c:38: Warning:
[eva:alarm] tests/gmp/at_on-purely-logic-variables.c:45: Warning:
signed overflow. assert __gen_e_acsl_v_4 - -4 ≤ 2147483647;
[eva:alarm] tests/full-mmodel-only/at_logic-variables.c:38: Warning:
signed overflow. assert (int)(__gen_e_acsl_v_4 - -4) * 12 ≤ 2147483647;
[eva:alarm] tests/full-mmodel-only/at_logic-variables.c:38: Warning:
[eva:alarm] tests/gmp/at_on-purely-logic-variables.c:45: Warning:
signed overflow.
assert
(int)((int)(__gen_e_acsl_v_4 - -4) * 12) + (int)(__gen_e_acsl_u_4 - 9) ≤
(int)((int)(__gen_e_acsl_u_4 - 9) * 32) + (int)(__gen_e_acsl_v_4 - -4) ≤
2147483647;
[eva:alarm] tests/full-mmodel-only/at_logic-variables.c:27: Warning:
[eva:alarm] tests/gmp/at_on-purely-logic-variables.c:34: Warning:
out of bounds write.
assert
\valid(__gen_e_acsl_at_3 +
(int)((int)((int)(__gen_e_acsl_v_2 - -4) * 12) +
(int)(__gen_e_acsl_u_2 - 9)));
[eva] tests/full-mmodel-only/at_logic-variables.c:27:
(int)((int)((int)(__gen_e_acsl_u_2 - 9) * 11) +
(int)(__gen_e_acsl_v_2 - -4)));
[eva] tests/gmp/at_on-purely-logic-variables.c:34:
starting to merge loop iterations
[eva:alarm] tests/full-mmodel-only/at_logic-variables.c:21: Warning:
[eva:alarm] tests/gmp/at_on-purely-logic-variables.c:28: Warning:
assertion got status unknown.
[eva] using specification for function __e_acsl_valid_read
[eva] using specification for function __e_acsl_assert
[eva:alarm] tests/full-mmodel-only/at_logic-variables.c:22: Warning:
[eva:alarm] tests/gmp/at_on-purely-logic-variables.c:29: Warning: