Commit 78f9aaab authored by Fonenantsoa Maurica 's avatar Fonenantsoa Maurica
Browse files

Addresses Julien's review no.2:

MAJOR:
- malloc and free
  - Distinct tables for malloc and free
  - Efficient insertion of free and malloc
  - Remove entries for malloc and free when they are not needed anymore
- Using kf instead of fundec
- Using closure of vi_at: not (straightforwardly) possible
- Logic scope:
  - No Lscope.top
  - Proper reseting of the lscope
  - Proper binding of logic variables
  - Module Env.Logic_scope
- Comment for the over-approximation of t_size

STYLE:
- No useless new lines
- Spaces
- Parentheses
- Latex style for formula in comment of index_from_sizes_and_shifts
- match -> function
- Logical variable -> logic variable
- Renaming:
  - add_to_lscope ->  extend_lscope
  - memory_infos_from_quantifs -> sizes_and_shifts_from_quantifs
  - res -> sizes_and_shifts, memory_infos -> sizes_and_shifts
- Typos
- Forward references at the end of the mli
- Consistent ordering of arguments inside Lscope API

OTHERS:
- Auxiliary function append_block_of_env_to_block
- Squash pattern matching of mk_storing_loops
- No Interval.infer in to_exp
- Refactoring of pre_from_label
- pi_beta_j with fold_left
- No superfluous env for sizes_and_shifts_from_quantifs
- More efficient accumulator for computing size
- Squash pattern matching of sizes_and_shifts_from_quantifs
- No superfluous option for get_lscope_var
- Better definition of effective_lscope_from_pred_or_term
- Using List.find for defining get_lscope_var
- Do not export get_lscope_var
- Lscope.empty () -> Lscope.empty
parent c9f1976f
This diff is collapsed.
......@@ -24,17 +24,7 @@ open Cil_types
open Cil_datatype
(* Convert \at on terms or predicates in which we can find purely
logical variable. *)
(**************************************************************************)
(********************** Forward references ********************************)
(**************************************************************************)
val predicate_to_exp_ref:
(kernel_function -> Env.t -> predicate -> exp * Env.t) ref
val term_to_exp_ref:
(kernel_function -> Env.t -> term -> exp * Env.t) ref
logic variable. *)
(**************************************************************************)
(*************************** Translation **********************************)
......@@ -49,19 +39,24 @@ val to_exp:
(*****************************************************************************)
(* The different possible evaluations of the [\at] under study are
stored on a memory location that needs to be alloted then freed.
stored in a memory location that needs to be alloted then freed.
This part is designed for that purpose. *)
type malloc_and_free_stmts = {
mf_malloc : stmt;
mf_free : stmt
}
(* A malloc stmt and its associated free stmt. *)
val get_mallocs: kernel_function -> stmt list
(* Get the list of [malloc] stmts that need to be inserted into [kf]. *)
val add_malloc_and_free_stmts:
kernel_function -> malloc_and_free_stmts -> unit
(* Add a [malloc] and [free] stmts that need to be added to [kf] *)
val get_frees: kernel_function -> stmt list
(* Get the list of [malloc] stmts that need to be inserted into [kf]. *)
val get_malloc_and_free_stmts: fundec -> stmt list * stmt list
(* Get the list of [malloc] and [free] stmts that need to be added
to [fundec] *)
\ No newline at end of file
val remove_mallocs_and_frees: kernel_function -> unit
(* Remove all [malloc] and [free] stmts for [kf] from the internal table. *)
(**************************************************************************)
(********************** Forward references ********************************)
(**************************************************************************)
val predicate_to_exp_ref:
(kernel_function -> Env.t -> predicate -> exp * Env.t) ref
val term_to_exp_ref:
(kernel_function -> Env.t -> term -> exp * Env.t) ref
\ No newline at end of file
......@@ -53,6 +53,7 @@ type local_env =
type t =
{ visitor: Visitor.frama_c_visitor;
lscope: Lscope.t;
lscope_reset: bool;
annotation_kind: Misc.annotation_kind;
new_global_vars: (varinfo * scope) list;
(* generated variables. The scope indicates the level where the variable
......@@ -110,7 +111,8 @@ let empty_local_env =
let dummy =
{ visitor = new Visitor.generic_frama_c_visitor (Cil.inplace_visit ());
lscope = Lscope.empty ();
lscope = Lscope.empty;
lscope_reset = true;
annotation_kind = Misc.Assertion;
new_global_vars = [];
global_mpz_tbl = empty_mpz_tbl;
......@@ -122,7 +124,8 @@ let dummy =
let empty v =
{ visitor = v;
lscope = Lscope.empty ();
lscope = Lscope.empty;
lscope_reset = true;
annotation_kind = Misc.Assertion;
new_global_vars = [];
global_mpz_tbl = empty_mpz_tbl;
......@@ -302,6 +305,9 @@ module Logic_binding = struct
try Logic_var.Map.find logic_v env.var_mapping
with Not_found -> assert false
let set env lv vi =
{ env with var_mapping = Logic_var.Map.add lv vi env.var_mapping }
let remove env v =
let map = env.var_mapping in
assert (Logic_var.Map.mem v map);
......@@ -318,9 +324,15 @@ let current_kf env =
let get_visitor env = env.visitor
let get_behavior env = env.visitor#behavior
let get_lscope env = env.lscope
let add_to_lscope env lvs = { env with lscope = Lscope.add env.lscope lvs }
let reset_lscope env = { env with lscope = Lscope.empty () }
module Logic_scope = struct
let get env = env.lscope
let extend env lvs = { env with lscope = Lscope.add lvs env.lscope }
let set_reset env bool = { env with lscope_reset = bool }
let get_reset env = env.lscope_reset
let reset env =
if env.lscope_reset then { env with lscope = Lscope.empty }
else env
end
let emitter =
Emitter.create
......@@ -365,6 +377,11 @@ 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 }
......
......@@ -67,6 +67,7 @@ val new_var_and_mpz_init:
module Logic_binding: sig
val add: ?ty:typ -> t -> logic_var -> varinfo * exp * t
val get: t -> logic_var -> varinfo
val set: t -> logic_var -> varinfo -> t
val remove: t -> logic_var -> t
end
......@@ -86,6 +87,10 @@ val extend_stmt_in_place: t -> stmt -> pre:bool -> block -> t
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 push: t -> t
(** Push a new local context in the environment *)
......@@ -116,15 +121,26 @@ val get_behavior: t -> Cil.visitor_behavior
val current_kf: t -> kernel_function option
(** Kernel function currently visited in the new project. *)
val get_lscope: t -> Lscope.t
(* Return the logical scope associated to the environment. *)
module Logic_scope: sig
val get: t -> Lscope.t
(** Return the logic scope associated to the environment. *)
val extend: t -> Lscope.lscope_var -> t
(** Add a new logic variable with its associated information in the
logic scope of the environment. *)
val add_to_lscope: t -> Lscope.lscope_var -> t
(* Add a new logical variable with its associated information in the
logical scope of the environment. *)
val reset: t -> t
(** Return a new environment in which the logic scope is reset
iff [set_reset _ true] has been called beforehand. Do nothing otherwise. *)
val reset_lscope: t -> t
(* Return a new environment in which the logical scope has been reset. *)
val set_reset: t -> bool -> t
(** Setter of the information indicating whether the logic scope should be
reset at next call to [reset]. *)
val get_reset: t -> bool
(** Getter of the information indicating whether the logic scope should be
reset at next call to [reset]. *)
end
(* ************************************************************************** *)
(** {2 Current annotation kind} *)
......
......@@ -31,38 +31,34 @@ type lscope_var =
type t = lscope_var list
(* The logic scope is usually small, so a list is fine instead of a Map *)
let empty () = []
let empty = []
let is_empty = function [] -> true | _ :: _ -> false
let add t lvs = t @ [lvs]
(* We need to append [lvs], and not prepend it.
This is so that the first element of the list is
the first that should be translated,
the 2nd element the 2nd to be translated and so on. *)
let add lscope_var t = lscope_var :: t
let top = function
| [] -> None
| lvs :: lscope -> Some(lvs, lscope)
let get_all t = List.rev t
let rec get_lscope_var lv t =
match t with
| [] ->
None
| lvs :: t' ->
match lvs with
| Lvs_let(lv', _) | Lvs_quantif(_, lv', _)
| Lvs_formal(lv', _) | Lvs_global(lv', _) ->
if Cil_datatype.Logic_var.equal lv lv' then Some lvs
else get_lscope_var lv t'
let get_lscope_var 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
let effective_lscope_from_pred_or_term pot potential_lscope =
let effective_lscope = ref (empty ()) in
let effective_lscope = ref empty in
let o = object inherit Visitor.frama_c_inplace
method !vlogic_var_use lv =
begin match get_lscope_var lv potential_lscope with
| None -> ()
| Some lvs -> effective_lscope := add !effective_lscope lvs
begin match lv.lv_origin with
| Some _ ->
(* [lv] is not purely logic. Thus it is not to be put inside
[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
end;
Cil.DoChildren
end
......
......@@ -23,7 +23,7 @@
open Cil_types
(* Handle the logic scope of a term.
We define the logic scope of a term [t] to be the set of PURELY logical
We define the logic scope of a term [t] to be the set of PURELY logic
variables that are visible by [t]. *)
type lscope_var =
......@@ -34,23 +34,22 @@ type lscope_var =
type t
val empty: unit -> t
val empty: t
(* Create an empty logic scope. *)
val is_empty: t -> bool
(* Check whether the given logic scope is empty. *)
val add: t -> lscope_var -> t
val add: lscope_var -> t -> t
(* Return a new logic scope in which the given [lscope_var] has been added. *)
val get_lscope_var: logic_var -> t -> lscope_var option
(* Return the [lscope_var] associated to the given logic var, if it exists. *)
val top: t -> (lscope_var * t) option
(* Return the outermost [lscope_var]. *)
val get_all: t -> lscope_var list
(* Return the list of [lscope_var] of the given logic scope.
The first element is the first [lscope_var] that was added to [t], the
second element is the second [lscope_var] that was added to [t], an so on. *)
val effective_lscope_from_pred_or_term: Misc.pred_or_term -> t -> t
(* We define the EFFECTIVE logical scope of a predicate or term [pot],
(* We define the EFFECTIVE logic scope of a predicate or term [pot],
for a given POTENTIAL logical [potential_lscope] scope, to be the set [S] of
logical variables from [potential_lscope] that appear in [pot].
logic variables from [potential_lscope] that appear in [pot].
[effective_lscope_from_pred_or_term pot potential_lscope] computes [S]. *)
\ No newline at end of file
......@@ -307,6 +307,22 @@ let term_has_lv_from_vi t =
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"
......
......@@ -116,10 +116,20 @@ val is_bitfield_pointers: logic_type -> bool
val term_has_lv_from_vi: term -> bool
(* Return [true] iff the given term contains a variables that originated from
a C varinfo, that is a non-purely logical variable. *)
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"
......
......@@ -146,7 +146,7 @@ let convert kf env loc is_forall p bounded_vars hyps goal =
| Rgt | Rge | Req | Rneq -> assert false
in
let lvs = Lscope.Lvs_quantif(t1, lv, t2) in
Env.add_to_lscope env lvs)
Env.Logic_scope.extend env lvs)
env
guards
in
......
......@@ -4,7 +4,9 @@
and without --gmp-only
*/
/*@ ensures \forall integer n; 1 < n <= 3 ==> \old(t[n] == 12); */
/*@ ensures \forall integer n; 1 < n <= 3 ==>
\old(t[n] == 12) && \old(t[n - 1] > 5);
ensures \let m = 4; \old(t[m] == -4) && \old(t[m - 4]) == 9; */
void f(int *t) {}
int main(void) {
......
[e-acsl] beginning translation.
[e-acsl] tests/full-mmodel-only/at_logic-variables.c:45: Warning:
[e-acsl] tests/full-mmodel-only/at_logic-variables.c:47: Warning:
E-ACSL construct
`\at on purely logical variables that needs to allocate too much memory (bigger than int_max bytes)'
`\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:47: Warning:
[e-acsl] tests/full-mmodel-only/at_logic-variables.c:49: Warning:
E-ACSL construct `\at with logic variable linked to C variable'
is not yet supported.
Ignoring annotation.
......@@ -21,22 +21,173 @@
[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_full_init
[eva] tests/full-mmodel-only/at_logic-variables.c:36:
allocating variable __malloc_main_l36
[eva] tests/full-mmodel-only/at_logic-variables.c:32:
allocating variable __malloc_main_l32
[eva] tests/full-mmodel-only/at_logic-variables.c:28:
allocating variable __malloc_main_l28
[eva] tests/full-mmodel-only/at_logic-variables.c:25:
allocating variable __malloc_main_l25
[eva] tests/full-mmodel-only/at_logic-variables.c:20:
allocating variable __malloc_main_l20
[eva] tests/full-mmodel-only/at_logic-variables.c:19:
allocating variable __malloc_main_l19
[eva:alarm] tests/full-mmodel-only/at_logic-variables.c:28: Warning:
[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:
out of bounds write. assert \valid(__gen_e_acsl_at_4 + 0);
[eva:alarm] tests/full-mmodel-only/at_logic-variables.c:22: 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:
starting to merge loop iterations
[eva:alarm] tests/full-mmodel-only/at_logic-variables.c:21: Warning:
out of bounds write. assert \valid(__gen_e_acsl_at + 0);
[eva:alarm] tests/full-mmodel-only/at_logic-variables.c:38: 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:
starting to merge loop iterations
[eva:alarm] tests/full-mmodel-only/at_logic-variables.c:38: 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:
signed overflow.
assert
(int)((int)(__gen_e_acsl_v_4 - -4) * 12) + (int)(__gen_e_acsl_u_4 - 9) ≤
2147483647;
[eva:alarm] tests/full-mmodel-only/at_logic-variables.c:27: 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:
starting to merge loop iterations
[eva:alarm] tests/full-mmodel-only/at_logic-variables.c:21: 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:
assertion got status unknown.
[eva:alarm] tests/full-mmodel-only/at_logic-variables.c:22: Warning:
function __e_acsl_assert: precondition got status unknown.
[eva:alarm] tests/full-mmodel-only/at_logic-variables.c:22: Warning:
accessing uninitialized left-value.
assert \initialized(__gen_e_acsl_at_2 + (__gen_e_acsl_j - 2));
[eva:alarm] tests/full-mmodel-only/at_logic-variables.c:22: Warning:
out of bounds read.
assert \valid_read(__gen_e_acsl_at_2 + (int)(__gen_e_acsl_j - 2));
[eva] tests/full-mmodel-only/at_logic-variables.c:22:
starting to merge loop iterations
[eva:alarm] tests/full-mmodel-only/at_logic-variables.c:22: Warning:
function __e_acsl_assert: precondition got status unknown.
[eva:alarm] tests/full-mmodel-only/at_logic-variables.c:24: Warning:
assertion got status unknown.
[eva:alarm] tests/full-mmodel-only/at_logic-variables.c:27: Warning:
function __e_acsl_assert: precondition got status unknown.
[eva:alarm] tests/full-mmodel-only/at_logic-variables.c:26: Warning:
accessing uninitialized left-value.
assert
\initialized(__gen_e_acsl_at_3 +
((__gen_e_acsl_v - -4) * 12 + (__gen_e_acsl_u - 9)));
[eva:alarm] tests/full-mmodel-only/at_logic-variables.c:26: Warning:
out of bounds read.
assert
\valid_read(__gen_e_acsl_at_3 +
(int)((int)((int)(__gen_e_acsl_v - -4) * 12) +
(int)(__gen_e_acsl_u - 9)));
[eva] tests/full-mmodel-only/at_logic-variables.c:26:
starting to merge loop iterations
[eva:alarm] tests/full-mmodel-only/at_logic-variables.c:30: Warning:
assertion got status unknown.
[eva:alarm] tests/full-mmodel-only/at_logic-variables.c:34: Warning:
out of bounds write.
assert \valid(__gen_e_acsl_at_5 + (int)(__gen_e_acsl_k_4 - -8));
[eva] tests/full-mmodel-only/at_logic-variables.c:34:
starting to merge loop iterations
[eva:alarm] tests/full-mmodel-only/at_logic-variables.c:34: Warning:
assertion got status unknown.
[eva:alarm] tests/full-mmodel-only/at_logic-variables.c:34: Warning:
function __e_acsl_assert: precondition got status unknown.
[eva:alarm] tests/full-mmodel-only/at_logic-variables.c:34: Warning:
accessing uninitialized left-value.
assert \initialized(__gen_e_acsl_at_5 + (__gen_e_acsl_k_3 - -8));
[eva:alarm] tests/full-mmodel-only/at_logic-variables.c:34: Warning:
out of bounds read.
assert \valid_read(__gen_e_acsl_at_5 + (int)(__gen_e_acsl_k_3 - -8));
[eva] tests/full-mmodel-only/at_logic-variables.c:34:
starting to merge loop iterations
[eva:alarm] tests/full-mmodel-only/at_logic-variables.c:34: Warning:
function __e_acsl_assert: precondition got status unknown.
[eva:alarm] tests/full-mmodel-only/at_logic-variables.c:36: Warning:
assertion got status unknown.
[eva:alarm] tests/full-mmodel-only/at_logic-variables.c:38: Warning:
function __e_acsl_assert: precondition got status unknown.
[eva:alarm] tests/full-mmodel-only/at_logic-variables.c:37: Warning:
accessing uninitialized left-value.
assert
\initialized(__gen_e_acsl_at_6 +
((__gen_e_acsl_v_3 - -4) * 12 + (__gen_e_acsl_u_3 - 9)));
[eva:alarm] tests/full-mmodel-only/at_logic-variables.c:37: Warning:
out of bounds read.
assert
\valid_read(__gen_e_acsl_at_6 +
(int)((int)((int)(__gen_e_acsl_v_3 - -4) * 12) +
(int)(__gen_e_acsl_u_3 - 9)));
[eva] tests/full-mmodel-only/at_logic-variables.c:37:
starting to merge loop iterations
[eva] tests/full-mmodel-only/at_logic-variables.c:9:
allocating variable __malloc___gen_e_acsl_f_l9
[eva] tests/full-mmodel-only/at_logic-variables.c:9:
allocating variable __malloc___gen_e_acsl_f_l9_0
[eva] tests/full-mmodel-only/at_logic-variables.c:8:
allocating variable __malloc___gen_e_acsl_f_l8
[eva] tests/full-mmodel-only/at_logic-variables.c:8:
allocating variable __malloc___gen_e_acsl_f_l8_0
[eva:alarm] tests/full-mmodel-only/at_logic-variables.c:9: Warning:
out of bounds write. assert \valid(__gen_e_acsl_at_4 + 0);
[eva:alarm] tests/full-mmodel-only/at_logic-variables.c:20: Warning:
accessing uninitialized left-value. assert \initialized(&__gen_e_acsl_j);
[kernel] tests/full-mmodel-only/at_logic-variables.c:20: Warning:
all target addresses were invalid. This path is assumed to be dead.
[eva:alarm] tests/full-mmodel-only/at_logic-variables.c:9: Warning:
out of bounds write. assert \valid(__gen_e_acsl_at_3 + 0);
[eva:alarm] tests/full-mmodel-only/at_logic-variables.c:8: Warning:
out of bounds write.
assert \valid(__gen_e_acsl_at_2 + (int)(__gen_e_acsl_n_3 - 2));
[eva] tests/full-mmodel-only/at_logic-variables.c:8:
starting to merge loop iterations
[eva:alarm] tests/full-mmodel-only/at_logic-variables.c:8: Warning:
out of bounds write.
assert \valid(__gen_e_acsl_at + (int)(__gen_e_acsl_n_2 - 2));
[eva] tests/full-mmodel-only/at_logic-variables.c:8:
starting to merge loop iterations
[eva] using specification for function __e_acsl_delete_block
[eva:alarm] tests/full-mmodel-only/at_logic-variables.c:8: Warning:
function __e_acsl_assert: precondition got status unknown.
[eva:alarm] tests/full-mmodel-only/at_logic-variables.c:8: Warning:
accessing uninitialized left-value.
assert \initialized(__gen_e_acsl_at + (__gen_e_acsl_n - 2));
[eva:alarm] tests/full-mmodel-only/at_logic-variables.c:8: Warning:
out of bounds read.
assert \valid_read(__gen_e_acsl_at + (int)(__gen_e_acsl_n - 2));
[eva:alarm] tests/full-mmodel-only/at_logic-variables.c:8: Warning:
function __e_acsl_assert: precondition got status unknown.
[eva:alarm] tests/full-mmodel-only/at_logic-variables.c:8: Warning:
accessing uninitialized left-value.
assert \initialized(__gen_e_acsl_at_2 + (__gen_e_acsl_n - 2));
[eva:alarm] tests/full-mmodel-only/at_logic-variables.c:8: Warning:
out of bounds read.
assert \valid_read(__gen_e_acsl_at_2 + (int)(__gen_e_acsl_n - 2));
[eva] tests/full-mmodel-only/at_logic-variables.c:7:
starting to merge loop iterations
[eva:alarm] tests/full-mmodel-only/at_logic-variables.c:7: Warning:
function __gen_e_acsl_f: postcondition got status unknown.
[eva:alarm] tests/full-mmodel-only/at_logic-variables.c:9: Warning:
function __gen_e_acsl_f: postcondition got status unknown.
[eva:alarm] tests/full-mmodel-only/at_logic-variables.c:46: Warning:
assertion got status unknown.
[eva:alarm] tests/full-mmodel-only/at_logic-variables.c:48: Warning:
assertion got status unknown.
[eva] using specification for function __e_acsl_memory_clean
[eva] done for function main
......@@ -312,7 +312,7 @@ let rec thost_to_host kf env th = match th with
let e, env = term_to_exp kf env t in
Mem e, env, ""
and toffset_to_offset ?loc kf env toff = match toff with
and toffset_to_offset ?loc kf env = function
| TNoOffset -> NoOffset, env
| TField(f, offset) ->
let offset, env = toffset_to_offset ?loc kf env offset in
......@@ -378,8 +378,7 @@ and context_insensitive_term_to_exp kf env t =
let ctx = Typing.get_integer_ty t in
Typing.type_term ~use_gmp_opt:true ~ctx zero;
let e, env =
comparison_to_exp
kf ~loc ~name:"not" env Typing.gmp Eq t zero (Some t)
comparison_to_exp kf ~loc ~name:"not" env Typing.gmp Eq t zero (Some t)
in
e, env, false, ""
else begin
......@@ -469,8 +468,7 @@ and context_insensitive_term_to_exp kf env t =
let env' = Env.push env1 in
let res2 = term_to_exp kf (Env.push env') t2 in
let e, env =
conditional_to_exp
~name:"or" loc (Some t) e1 (Cil.one loc, env') res2
conditional_to_exp ~name:"or" loc (Some t) e1 (Cil.one loc, env') res2
in
e, env, false, ""
| TBinOp(LAnd, t1, t2) ->
......@@ -552,7 +550,7 @@ and context_insensitive_term_to_exp kf env t =
let e, env = term_to_exp kf env t in
e, env, false, ""
| Tat(t', label) ->
let potential_lscope = Env.get_lscope env in
let potential_lscope = Env.Logic_scope.get env in
let effective_lscope = Lscope.effective_lscope_from_pred_or_term
(Misc.PoT_term t') potential_lscope
in
......@@ -589,7 +587,7 @@ and context_insensitive_term_to_exp kf env t =
| Trange _ -> not_yet env "range"
| Tlet(li, t) ->
let lvs = Lscope.Lvs_let(li.l_var_info, Misc.term_of_li li) in
let env = Env.add_to_lscope env lvs in
let env = Env.Logic_scope.extend env lvs in
let env = env_of_li li kf env loc in
let e, env = term_to_exp kf env t in
Interval.Env.remove li.l_var_info;
......@@ -920,11 +918,7 @@ and at_to_exp_no_lscope env t_opt label e =
let block, new_env =
Env.pop_and_get new_env new_stmt ~global_clear:false Env.Middle
in
let pre = match label with
| BuiltinLabel(Here | Post) -> true
| BuiltinLabel(Old | Pre | LoopEntry | LoopCurrent | Init)
| FormalLabel _ | StmtLabel _ -> false
in
let pre = Env.pre_from_label label in
env_ref := Env.extend_stmt_in_place new_env stmt ~pre block;
Cil.ChangeTo stmt