diff --git a/src/plugins/e-acsl/Makefile.in b/src/plugins/e-acsl/Makefile.in
index e12228f3c5541e1458ef4f9d0861b658d36101d8..13768e6bfbc325d7a77691443608f60bb05c4c78 100644
--- a/src/plugins/e-acsl/Makefile.in
+++ b/src/plugins/e-acsl/Makefile.in
@@ -69,16 +69,18 @@ PLUGIN_CMO:= local_config \
mmodel_analysis \
exit_points \
label \
+ lscope \
env \
keep_status \
dup_functions \
interval \
typing \
+ loops \
quantif \
+ at_with_lscope \
translate \
temporal \
prepare_ast \
- loops \
visit \
main
diff --git a/src/plugins/e-acsl/at_with_lscope.ml b/src/plugins/e-acsl/at_with_lscope.ml
new file mode 100644
index 0000000000000000000000000000000000000000..b266dff47c569425190f3ba6912993c39d50e996
--- /dev/null
+++ b/src/plugins/e-acsl/at_with_lscope.ml
@@ -0,0 +1,340 @@
+(**************************************************************************)
+(* *)
+(* This file is part of Frama-C. *)
+(* *)
+(* Copyright (C) 2007-2018 *)
+(* CEA (Commissariat à l'énergie atomique et aux énergies *)
+(* alternatives) *)
+(* *)
+(* you can redistribute it and/or modify it under the terms of the GNU *)
+(* Lesser General Public License as published by the Free Software *)
+(* Foundation, version 2.1. *)
+(* *)
+(* It is distributed in the hope that it will be useful, *)
+(* but WITHOUT ANY WARRANTY; without even the implied warranty of *)
+(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the *)
+(* GNU Lesser General Public License for more details. *)
+(* *)
+(* See the GNU Lesser General Public License version 2.1 *)
+(* for more details (enclosed in the file licenses/LGPLv2.1). *)
+(* *)
+(**************************************************************************)
+
+open Cil_types
+
+(**************************************************************************)
+(********************** Forward references ********************************)
+(**************************************************************************)
+
+let predicate_to_exp_ref
+ : (kernel_function -> Env.t -> predicate -> exp * Env.t) ref
+ = Extlib.mk_fun "named_predicate_to_exp_ref"
+
+let term_to_exp_ref
+ : (kernel_function -> Env.t -> term -> exp * Env.t) ref
+ = Extlib.mk_fun "term_to_exp_ref"
+
+(*****************************************************************************)
+(**************************** Handling memory ********************************)
+(*****************************************************************************)
+
+(* 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_all tbl kf =
+ if Cil_datatype.Kf.Hashtbl.mem tbl kf then begin
+ Cil_datatype.Kf.Hashtbl.remove tbl kf;
+ remove_all tbl kf
+ end
+
+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 **********************************)
+(**************************************************************************)
+
+(* Builds the terms [t_size] and [t_shifted] from each
+ [Lvs_quantif(tmin, lv, tmax)] from [lscope]
+ where [t_size = tmax - tmin + (-1|0|1)] depending on whether the
+ inequalities are strict or large
+ and [t_shifted = lv - tmin + (-1|0)] (so that we start indexing at 0) *)
+let rec sizes_and_shifts_from_quantifs ~loc kf lscope sizes_and_shifts =
+ match lscope with
+ | [] ->
+ sizes_and_shifts
+ | Lscope.Lvs_quantif(tmin, _, _, _, tmax) ::_
+ when Misc.term_has_lv_from_vi tmin || Misc.term_has_lv_from_vi tmax ->
+ Error.not_yet "\\at with logic variable linked to C variable"
+ | Lscope.Lvs_quantif(tmin, rel1, lv, rel2, tmax) :: lscope' ->
+ let t_size = Logic_const.term ~loc (TBinOp(MinusA, tmax, tmin)) Linteger in
+ let t_size = match rel1, rel2 with
+ | Rle, Rle ->
+ Logic_const.term
+ ~loc
+ (TBinOp(PlusA, t_size, Cil.lone ~loc ()))
+ Linteger
+ | Rlt, Rle | Rle, Rlt ->
+ t_size
+ | Rlt, Rlt ->
+ Logic_const.term
+ ~loc
+ (TBinOp(MinusA, t_size, Cil.lone ~loc ()))
+ Linteger
+ | _ ->
+ Options.fatal "Unexpected comparison operator"
+ in
+ let i = Interval.infer t_size in
+ (* The EXACT amount of memory that is needed can be known at runtime. This
+ is because the tightest bounds for the variables can be known at runtime.
+ Example: In the following predicate
+ [\exists integer u; 9 <= u <= 13 &&
+ \forall integer v; -5 < v <= (u <= 11 ? u + 6 : u - 9) ==>
+ \at(u + v > 0, K)]
+ the upper bound [M] for [v] depends on [u].
+ In chronological order, [M] equals to 15, 16, 17, 3 and 4.
+ Thus the tightest upper bound for [v] is [max(M)=17].
+ HOWEVER, computing that exact information requires extra nested loops,
+ prior to the [malloc] stmts, that will try all the possible values of the
+ variables involved in the bounds.
+ Instead of sacrificing time over memory (by performing these extra
+ computations), we consider that sacrificing memory over time is more
+ beneficial. In particular, though we may allocate more memory than
+ needed, the number of reads/writes into it is the same in both cases.
+ Conclusion: over-approximate [t_size] *)
+ let t_size = match Ival.min_and_max i with
+ | _, Some max ->
+ Logic_const.tint ~loc max
+ | _, None ->
+ Error.not_yet
+ "\\at on purely logic variables and with quantifier that uses \
+ too complex bound (E-ACSL cannot infer a finite upper bound to it)"
+ in
+ (* Index *)
+ let t_lv = Logic_const.tvar ~loc lv in
+ let t_shifted = match rel1 with
+ | Rle ->
+ Logic_const.term ~loc (TBinOp(MinusA, t_lv, tmin)) Linteger
+ | Rlt ->
+ let t = Logic_const.term ~loc (TBinOp(MinusA, t_lv, tmin)) Linteger in
+ Logic_const.term ~loc (TBinOp(MinusA, t, Cil.lone ~loc())) Linteger
+ | _ ->
+ Options.fatal "Unexpected comparison operator"
+ in
+ (* Returning *)
+ let sizes_and_shifts = (t_size, t_shifted) :: sizes_and_shifts in
+ sizes_and_shifts_from_quantifs ~loc kf lscope' sizes_and_shifts
+ | (Lscope.Lvs_let(_, t) | Lscope.Lvs_global(_, t)) :: _
+ when Misc.term_has_lv_from_vi t ->
+ Error.not_yet "\\at with logic variable linked to C variable"
+ | Lscope.Lvs_let _ :: lscope' ->
+ sizes_and_shifts_from_quantifs ~loc kf lscope' sizes_and_shifts
+ | Lscope.Lvs_formal _ :: _ ->
+ Error.not_yet "\\at using formal variable of a logic function"
+ | Lscope.Lvs_global _ :: _ ->
+ Error.not_yet "\\at using global logic variable"
+
+let size_from_sizes_and_shifts ~loc = function
+ | [] ->
+ (* No quantified variable. But still need to allocate [1*sizeof(_)] amount
+ of memory to store purely logic variables that are NOT quantified
+ (example: from \let). *)
+ Cil.lone ~loc ()
+ | (size, _) :: sizes_and_shifts ->
+ List.fold_left
+ (fun t_size (t_s, _) ->
+ Logic_const.term ~loc (TBinOp(Mult, t_size, t_s)) Linteger)
+ size
+ sizes_and_shifts
+
+(* Build the left-value corresponding to [*(at + index)]. *)
+let lval_at_index ~loc kf env (e_at, vi_at, t_index) =
+ Typing.type_term ~use_gmp_opt:false ~ctx:Typing.c_int t_index;
+ let term_to_exp = !term_to_exp_ref in
+ let e_index, env = term_to_exp kf env t_index in
+ let e_index = Cil.constFold false e_index in
+ let e_addr =
+ Cil.new_exp ~loc (BinOp(PlusPI, e_at, e_index, vi_at.vtype))
+ in
+ let lval_at_index = Mem e_addr, NoOffset in
+ lval_at_index, env
+
+(* Associate to each possible tuple of quantifiers
+ a unique index from the set {n | 0 <= n < n_max}.
+ That index will serve to identify the memory location where the evaluation
+ of the term/predicate is stored for the given tuple of quantifier.
+ The following gives the smallest set of such indexes (hence we use the
+ smallest amount of memory in some respect):
+ 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 index_from_sizes_and_shifts ~loc sizes_and_shifts =
+ let product terms = List.fold_left
+ (fun product t ->
+ Logic_const.term ~loc (TBinOp(Mult, product, t)) Linteger)
+ (Cil.lone ~loc ())
+ terms
+ in
+ let sum, _ = List.fold_left
+ (fun (index, sizes) (t_size, t_shifted) ->
+ let pi_beta_j = product 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
+ let env_ref = ref env in
+ let o = object
+ inherit Visitor.frama_c_inplace
+ method !vstmt_aux stmt =
+ assert (!env_ref == env);
+ 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));
+ !env_ref
+
+let to_exp ~loc kf env pot label =
+ 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 =
+ sizes_and_shifts_from_quantifs ~loc kf lscope_vars []
+ in
+ (* Creating the pointer *)
+ let ty = match pot with
+ | Misc.PoT_pred _ ->
+ Cil.intType
+ | Misc.PoT_term t ->
+ begin match Typing.get_integer_ty t with
+ | Typing.C_type _ | Typing.Other ->
+ Typing.get_typ t
+ | Typing.Gmp ->
+ Error.not_yet "\\at on purely logic variables and over gmp type"
+ 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;
+ [])
+ in
+ (* Index *)
+ let t_index = index_from_sizes_and_shifts ~loc sizes_and_shifts in
+ (* Innermost block *)
+ let mk_innermost_block env =
+ let term_to_exp = !term_to_exp_ref in
+ let named_predicate_to_exp = !predicate_to_exp_ref in
+ match pot with
+ | Misc.PoT_pred p ->
+ let env = Env.push env in
+ let lval, env = lval_at_index ~loc kf env (e_at, vi_at, t_index) in
+ let e, env = named_predicate_to_exp kf env p in
+ let e = Cil.constFold false e in
+ 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
+ in
+ (* We CANNOT return [block.bstmts] because it does NOT contain
+ variable declarations. *)
+ [ Cil.mkStmt ~valid_sid:true (Block block) ], env
+ | Misc.PoT_term t ->
+ begin match Typing.get_integer_ty t with
+ | Typing.C_type _ | Typing.Other ->
+ let env = Env.push env in
+ let lval, env = lval_at_index ~loc kf env (e_at, vi_at, t_index) in
+ let e, env = term_to_exp kf env t in
+ let e = Cil.constFold false e in
+ 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
+ in
+ (* We CANNOT return [block.bstmts] because it does NOT contain
+ variable declarations. *)
+ [ Cil.mkStmt ~valid_sid:true (Block block) ], env
+ | Typing.Gmp ->
+ Error.not_yet "\\at on purely logic variables and over gmp type"
+ end
+ in
+ (* Storing loops *)
+ let lscope_vars = Lscope.get_all (Env.Logic_scope.get env) in
+ let env = Env.push env in
+ let storing_loops_stmts, env =
+ Loops.mk_nested_loops ~loc mk_innermost_block kf env lscope_vars
+ in
+ let storing_loops_block = Cil.mkBlock storing_loops_stmts in
+ let storing_loops_block, env = Env.pop_and_get
+ env
+ (Cil.mkStmt ~valid_sid:true (Block storing_loops_block))
+ ~global_clear:false
+ Env.After
+ in
+ (* Put at label *)
+ let env = put_block_at_label env storing_loops_block label in
+ (* 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
diff --git a/src/plugins/e-acsl/at_with_lscope.mli b/src/plugins/e-acsl/at_with_lscope.mli
new file mode 100644
index 0000000000000000000000000000000000000000..40eeb55fd3c1c9b3625c16eb9ddcea102495b06f
--- /dev/null
+++ b/src/plugins/e-acsl/at_with_lscope.mli
@@ -0,0 +1,69 @@
+(**************************************************************************)
+(* *)
+(* This file is part of Frama-C. *)
+(* *)
+(* Copyright (C) 2007-2018 *)
+(* CEA (Commissariat à l'énergie atomique et aux énergies *)
+(* alternatives) *)
+(* *)
+(* you can redistribute it and/or modify it under the terms of the GNU *)
+(* Lesser General Public License as published by the Free Software *)
+(* Foundation, version 2.1. *)
+(* *)
+(* It is distributed in the hope that it will be useful, *)
+(* but WITHOUT ANY WARRANTY; without even the implied warranty of *)
+(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the *)
+(* GNU Lesser General Public License for more details. *)
+(* *)
+(* See the GNU Lesser General Public License version 2.1 *)
+(* for more details (enclosed in the file licenses/LGPLv2.1). *)
+(* *)
+(**************************************************************************)
+
+open Cil_types
+open Cil_datatype
+
+(* Convert \at on terms or predicates in which we can find purely
+ logic variable. *)
+
+(**************************************************************************)
+(*************************** Translation **********************************)
+(**************************************************************************)
+
+val to_exp:
+ loc:Location.t -> kernel_function -> Env.t ->
+ Misc.pred_or_term -> logic_label -> exp * Env.t
+
+(*****************************************************************************)
+(**************************** Handling memory ********************************)
+(*****************************************************************************)
+
+(* The different possible evaluations of the [\at] under study are
+ stored in a memory location that needs to be alloted then freed.
+ This part is designed for that purpose. *)
+
+module Malloc: sig
+ val find_all: kernel_function -> stmt list
+ (* Return 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
+
+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 ********************************)
+(**************************************************************************)
+
+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
diff --git a/src/plugins/e-acsl/doc/Changelog b/src/plugins/e-acsl/doc/Changelog
index 21e6f60037087fe70025dc22e78128b9040885f2..4adf3772d04bbd70aff6198441d842f4e4728849 100644
--- a/src/plugins/e-acsl/doc/Changelog
+++ b/src/plugins/e-acsl/doc/Changelog
@@ -19,6 +19,8 @@
# configure configure
###############################################################################
+-* E-ACSL [2018/10/04] Support for \at on purely logic variables.
+ Fix bug #1762 about out-of-scope variables when using \old.
* E-ACSL [2018/10/02] Fix bug #2305 about taking the address of a
bitfield.
- E-ACSL [2018/09/18] Support for ranges in memory builtins
diff --git a/src/plugins/e-acsl/doc/refman/at_on-purely-logic-variables.c b/src/plugins/e-acsl/doc/refman/at_on-purely-logic-variables.c
new file mode 100644
index 0000000000000000000000000000000000000000..88bbc974a191e189a3fdaa7e88047b65abf6387f
--- /dev/null
+++ b/src/plugins/e-acsl/doc/refman/at_on-purely-logic-variables.c
@@ -0,0 +1,12 @@
+main(void) {
+ int m = 2;
+ int n = 7;;
+ K: ;
+ n = 875;
+ /*@ assert
+ \let k = 3;
+ \exists integer u; 9 <= u < 21 &&
+ \forall integer v; -5 < v <= (u < 15 ? u + 6 : k) ==>
+ \at(n + u + v > 0, K); */ ;
+ return 0;
+}
diff --git a/src/plugins/e-acsl/doc/refman/at_on-purely-logic-variables_not-yet.c b/src/plugins/e-acsl/doc/refman/at_on-purely-logic-variables_not-yet.c
new file mode 100644
index 0000000000000000000000000000000000000000..dff4da97bd3e5b3fa986023c89a94a7307563cd5
--- /dev/null
+++ b/src/plugins/e-acsl/doc/refman/at_on-purely-logic-variables_not-yet.c
@@ -0,0 +1,2 @@
+/*@ ensures \forall int i; 0 <= i < n-1 ==> \old(t[i]) == t[i+1]; */
+void reverse(int *t, int n) { }
diff --git a/src/plugins/e-acsl/doc/refman/changes_modern.tex b/src/plugins/e-acsl/doc/refman/changes_modern.tex
index 99a5c9360d647dc13f05eebf515b6ff6fa296016..bbcf78dedebb7f60052f788e1606d485795cd53e 100644
--- a/src/plugins/e-acsl/doc/refman/changes_modern.tex
+++ b/src/plugins/e-acsl/doc/refman/changes_modern.tex
@@ -119,6 +119,8 @@ in \lstinline|\\at|}
\subsection*{Version \eacslversion}
\begin{itemize}
+\item \changeinsection{at}{support of \lstinline|\\at| on purely
+logic variables}
\item \changeinsection{locations}{support of ranges in memory built-ins
(e.g. \lstinline|\\valid| or \lstinline|\\initialized|)}
\end{itemize}
diff --git a/src/plugins/e-acsl/doc/refman/speclang_modern.tex b/src/plugins/e-acsl/doc/refman/speclang_modern.tex
index 2b4fa7dec498ee36d6c79fa6a84e1a43bfe71fd0..3adb89eb13dd0ba7731bb2be8fd24caf64fc863e 100644
--- a/src/plugins/e-acsl/doc/refman/speclang_modern.tex
+++ b/src/plugins/e-acsl/doc/refman/speclang_modern.tex
@@ -512,6 +512,30 @@ only the first one is accepted and valid in \eacsl since evaluating the term
\end{example}
+For the time being, \verb|\at| can be applied to any term or predicate that uses
+quantified variables, let-binded variables and C variables.
+
+\begin{example}
+The \verb|\at| construct of the following example is supported.
+\cinput{at_on-purely-logic-variables.c}
+
+\end{example}
+
+
+\begin{notimplementedenv}
+However, quantified variables that use C variables in their bounds and
+let-binded variables that use C variables in their definition
+are not yet supported.
+
+\begin{example}
+The \verb|\at| construct of the following example is \emph{not yet} supported
+since the quantified variable \verb|i| uses the C variable \verb|n| in the
+definition of its upper bound.
+\cinput{at_on-purely-logic-variables_not-yet.c}
+
+\end{example}
+\end{notimplementedenv}
+
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\subsection{Statement contracts}
diff --git a/src/plugins/e-acsl/env.ml b/src/plugins/e-acsl/env.ml
index 6cbc310cb12e66d4da8067836bca1bb4733c2bee..aeb9cc143e247a31d4abaf5747dd76a4e2ce4708 100644
--- a/src/plugins/e-acsl/env.ml
+++ b/src/plugins/e-acsl/env.ml
@@ -51,7 +51,9 @@ type local_env =
rte: bool }
type t =
- { visitor: Visitor.frama_c_visitor;
+ { 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
@@ -59,7 +61,8 @@ type t =
global_mpz_tbl: mpz_tbl;
env_stack: local_env list;
init_env: local_env;
- var_mapping: Varinfo.t Logic_var.Map.t; (* bind logic var to C var *)
+ var_mapping: Varinfo.t Stack.t Logic_var.Map.t;
+ (* records of C bindings for logic vars *)
loop_invariants: predicate list list;
(* list of loop invariants for each currently visited loops *)
cpt: int; (* counter used when generating variables *) }
@@ -108,7 +111,9 @@ let empty_local_env =
rte = true }
let dummy =
- { visitor = new Visitor.generic_frama_c_visitor (Cil.inplace_visit ());
+ { visitor = new Visitor.generic_frama_c_visitor (Cil.inplace_visit ());
+ lscope = Lscope.empty;
+ lscope_reset = true;
annotation_kind = Misc.Assertion;
new_global_vars = [];
global_mpz_tbl = empty_mpz_tbl;
@@ -119,7 +124,9 @@ let dummy =
cpt = 0; }
let empty v =
- { visitor = v;
+ { visitor = v;
+ lscope = Lscope.empty;
+ lscope_reset = true;
annotation_kind = Misc.Assertion;
new_global_vars = [];
global_mpz_tbl = empty_mpz_tbl;
@@ -280,29 +287,48 @@ module Logic_binding = struct
| 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 =
+ | 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 env ~name:logic_v.lv_name None ty (fun _ _ -> [])
+ let v, e, env = new_var
+ ~loc:Location.unknown
+ env
+ ~name:logic_v.lv_name
+ None
+ 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 with var_mapping = Logic_var.Map.add logic_v v env.var_mapping }
+ v, e, env
- let get env logic_v =
- try Logic_var.Map.find logic_v env.var_mapping
- with Not_found -> assert false
+ let get env logic_v =
+ try
+ let varinfos = Logic_var.Map.find logic_v env.var_mapping in
+ Stack.top varinfos
+ with Not_found | Stack.Empty ->
+ assert false
- let remove env v =
- let map = env.var_mapping in
- assert (Logic_var.Map.mem v map);
- { env with var_mapping = Logic_var.Map.remove v map }
+ let remove env logic_v =
+ try
+ let varinfos = Logic_var.Map.find logic_v env.var_mapping in
+ ignore (Stack.pop varinfos);
+ env
+ with Not_found | Stack.Empty ->
+ assert false
end
@@ -315,6 +341,16 @@ let current_kf env =
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 }
+ 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
"E_ACSL"
@@ -345,12 +381,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
diff --git a/src/plugins/e-acsl/env.mli b/src/plugins/e-acsl/env.mli
index bb32297e32dd877b7127bb645f1f44047b191224..b56fe807cd817458a57e3b58a3004f0d89bb42dc 100644
--- a/src/plugins/e-acsl/env.mli
+++ b/src/plugins/e-acsl/env.mli
@@ -66,8 +66,13 @@ val new_var_and_mpz_init:
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 get: t -> logic_var -> varinfo
+ (* Return the latest C binding. *)
+
val remove: t -> logic_var -> t
+ (* Remove the latest C binding. *)
end
val add_assert: t -> stmt -> predicate -> unit
@@ -80,11 +85,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 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 [label] 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 *)
@@ -116,6 +121,27 @@ val get_behavior: t -> Cil.visitor_behavior
val current_kf: t -> kernel_function option
(** Kernel function currently visited in the new project. *)
+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 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 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} *)
(* ************************************************************************** *)
diff --git a/src/plugins/e-acsl/loops.ml b/src/plugins/e-acsl/loops.ml
index 3997c2c9ef324672d9aea532bfc8b0380a7e0a7b..b359b7beb1d82d9b23977ef0977a608a08ab8379 100644
--- a/src/plugins/e-acsl/loops.ml
+++ b/src/plugins/e-acsl/loops.ml
@@ -20,27 +20,44 @@
(* *)
(**************************************************************************)
+open Cil
open Cil_types
+(**************************************************************************)
+(********************** Forward references ********************************)
+(**************************************************************************)
+
+let translate_named_predicate_ref
+ : (kernel_function -> Env.t -> predicate -> Env.t) ref
+ = Extlib.mk_fun "translate_named_predicate_ref"
+
+let term_to_exp_ref
+ : (kernel_function -> Env.t -> term -> exp * Env.t) ref
+ = Extlib.mk_fun "term_to_exp_ref"
+
+(**************************************************************************)
+(************************* Loop invariants ********************************)
+(**************************************************************************)
+
module Loop_invariants_actions = Hook.Make(struct end)
let apply_after_transformation prj =
Project.on prj Loop_invariants_actions.apply ()
-let mv_invariants env ~old stmt =
+let mv_invariants env ~old stmt =
Options.feedback ~current:true ~level:3
"keep loop invariants attached to its loop";
match Env.current_kf env with
| None -> assert false
| Some kf ->
- let filter _ ca = match ca.annot_content with
+ let filter _ ca = match ca.annot_content with
| AInvariant(_, b, _) -> b
| _ -> false
in
let l = Annotations.code_annot_emitter ~filter stmt in
if l != [] then
Loop_invariants_actions.extend
- (fun () ->
+ (fun () ->
List.iter
(fun (ca, e) ->
Annotations.remove_code_annot e ~kf old ca;
@@ -48,21 +65,22 @@ let mv_invariants env ~old stmt =
l)
let preserve_invariant prj env kf stmt = match stmt.skind with
- | Loop(_, ({ bstmts = stmts } as blk), loc, cont, break) ->
+ | Loop(_, ({ bstmts = stmts } as blk), loc, cont, break) ->
let rec handle_invariants (stmts, env, _ as acc) = function
- | [] ->
+ | [] ->
(* empty loop body: no need to verify the invariant twice *)
acc
- | [ last ] ->
+ | [ last ] ->
let invariants, env = Env.pop_loop env in
let env = Env.push env in
- let env =
+ let env =
+ let translate_named_predicate = !translate_named_predicate_ref in
Project.on
prj
- (List.fold_left (Translate.translate_named_predicate kf) env)
- invariants
+ (List.fold_left (translate_named_predicate kf) env)
+ invariants
in
- let blk, env =
+ let blk, env =
Env.pop_and_get env last ~global_clear:false Env.Before
in
Misc.mk_block prj last blk :: stmts, env, invariants != []
@@ -71,11 +89,160 @@ let preserve_invariant prj env kf stmt = match stmt.skind with
let env = Env.set_annotation_kind env Misc.Invariant in
let stmts, env, has_loop = handle_invariants ([], env, false) stmts in
let new_blk = { blk with bstmts = List.rev stmts } in
- { stmt with skind = Loop([], new_blk, loc, cont, break) },
- env,
+ { stmt with skind = Loop([], new_blk, loc, cont, break) },
+ env,
has_loop
| _ -> stmt, env, false
+(**************************************************************************)
+(**************************** Nested loops ********************************)
+(**************************************************************************)
+
+let rec mk_nested_loops ~loc mk_innermost_block kf env lscope_vars =
+ let term_to_exp = !term_to_exp_ref in
+ match lscope_vars with
+ | [] ->
+ mk_innermost_block env
+ | Lscope.Lvs_quantif(t1, rel1, logic_x, rel2, t2) :: lscope_vars' ->
+ let ctx =
+ let ty1 = Typing.get_integer_ty t1 in
+ let ty2 = Typing.get_integer_ty t2 in
+ Typing.join ty1 ty2
+ in
+ let t_plus_one ?ty t =
+ (* whenever provided, [ty] is known to be the type of the result *)
+ let tone = Cil.lone ~loc () in
+ let res = Logic_const.term ~loc (TBinOp(PlusA, t, tone)) Linteger in
+ Extlib.may
+ (fun ty ->
+ Typing.unsafe_set tone ~ctx:ty ctx;
+ Typing.unsafe_set t ~ctx:ty ctx;
+ Typing.unsafe_set res ty)
+ ty;
+ res
+ in
+ let t1 = match rel1 with
+ | Rlt ->
+ let t = t_plus_one t1 in
+ Typing.type_term ~use_gmp_opt:false ~ctx t;
+ t
+ | Rle ->
+ t1
+ | Rgt | Rge | Req | Rneq ->
+ assert false
+ in
+ let t2_one, bop2 = match rel2 with
+ | Rlt ->
+ t2, Lt
+ | Rle ->
+ (* we increment the loop counter one more time (at the end of the
+ loop). Thus to prevent overflow, check the type of [t2+1]
+ instead of [t2]. *)
+ t_plus_one t2, Le
+ | Rgt | Rge | Req | Rneq ->
+ assert false
+ in
+ Typing.type_term ~use_gmp_opt:false ~ctx t2_one;
+ let ctx_one =
+ let ty1 = Typing.get_integer_ty t1 in
+ let ty2 = Typing.get_integer_ty t2_one in
+ Typing.join ty1 ty2
+ in
+ let ty =
+ try Typing.typ_of_integer_ty ctx_one
+ with Typing.Not_an_integer -> assert false
+ in
+ (* loop counter corresponding to the quantified variable *)
+ let var_x, x, env = Env.Logic_binding.add ~ty env logic_x in
+ let lv_x = var var_x in
+ let env = match ctx_one with
+ | Typing.C_type _ -> env
+ | Typing.Gmp -> Env.add_stmt env (Gmpz.init ~loc x)
+ | Typing.Other -> assert false
+ in
+ (* build the inner loops and loop body *)
+ let body, env =
+ mk_nested_loops ~loc mk_innermost_block kf env lscope_vars'
+ in
+ (* initialize the loop counter to [t1] *)
+ let e1, env = term_to_exp kf (Env.push env) t1 in
+ let init_blk, env = Env.pop_and_get
+ env
+ (Gmpz.affect ~loc:e1.eloc lv_x x e1)
+ ~global_clear:false
+ Env.Middle
+ in
+ (* generate the guard [x bop t2] *)
+ let block_to_stmt b = mkStmt ~valid_sid:true (Block b) in
+ let tlv = Logic_const.tvar ~loc logic_x in
+ let guard =
+ (* must copy [t2] to force being typed again *)
+ Logic_const.term ~loc
+ (TBinOp(bop2, tlv, { t2 with term_node = t2.term_node } )) Linteger
+ in
+ Typing.type_term ~use_gmp_opt:false ~ctx:Typing.c_int guard;
+ let guard_exp, env = term_to_exp kf (Env.push env) guard in
+ let break_stmt = mkStmt ~valid_sid:true (Break guard_exp.eloc) in
+ let guard_blk, env = Env.pop_and_get
+ env
+ (mkStmt
+ ~valid_sid:true
+ (If(
+ guard_exp,
+ mkBlock [ mkEmptyStmt ~loc () ],
+ mkBlock [ break_stmt ],
+ guard_exp.eloc)))
+ ~global_clear:false
+ Env.Middle
+ in
+ let guard = block_to_stmt guard_blk in
+ (* increment the loop counter [x++];
+ previous typing ensures that [x++] fits type [ty] *)
+ (* TODO: should check that it does not overflow in the case of the type
+ of the loop variable is __declared__ too small. *)
+ let tlv_one = t_plus_one ~ty:ctx_one tlv in
+ let incr, env = term_to_exp kf (Env.push env) tlv_one in
+ let next_blk, env = Env.pop_and_get
+ env
+ (Gmpz.affect ~loc:incr.eloc lv_x x incr)
+ ~global_clear:false
+ Env.Middle
+ in
+ (* remove logic binding now that the block is constructed *)
+ let env = Env.Logic_binding.remove env logic_x in
+ (* generate the whole loop *)
+ let start = block_to_stmt init_blk in
+ let next = block_to_stmt next_blk in
+ let stmt = mkStmt
+ ~valid_sid:true
+ (Loop(
+ [],
+ mkBlock (guard :: body @ [ next ]),
+ loc,
+ None,
+ Some break_stmt))
+ in
+ [ start ; stmt ], env
+ | Lscope.Lvs_let(lv, t) :: lscope_vars' ->
+ let ty = Typing.get_typ t in
+ let vi_of_lv, exp_of_lv, env = Env.Logic_binding.add ~ty 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 stmts, env =
+ 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
+ (* return *)
+ let_stmt :: stmts, env
+ | Lscope.Lvs_formal _ :: _ ->
+ Error.not_yet
+ "creating nested loops from formal variable of a logic function"
+ | Lscope.Lvs_global _ :: _ ->
+ Error.not_yet
+ "creating nested loops from global logic variable"
+
+
(*
Local Variables:
compile-command: "make"
diff --git a/src/plugins/e-acsl/loops.mli b/src/plugins/e-acsl/loops.mli
index ba56d942004fc4383a949448eba3bf5883f25562..1f2d658a8e25528cc3367cbb4906ba003e331271 100644
--- a/src/plugins/e-acsl/loops.mli
+++ b/src/plugins/e-acsl/loops.mli
@@ -24,19 +24,47 @@
open Cil_types
+(**************************************************************************)
+(************************* Loop invariants ********************************)
+(**************************************************************************)
+
val apply_after_transformation: Project.t -> unit
val mv_invariants: Env.t -> old:stmt -> stmt -> unit
(** Transfer the loop invariants from the [old] loop to the new one.
Both statements must be loops. *)
-val preserve_invariant:
+val preserve_invariant:
Project.t -> Env.t -> Kernel_function.t -> stmt -> stmt * Env.t * bool
(** modify the given stmt loop to insert the code which preserves its loop
invarariants. Also return the modify environment and a boolean which
indicates whether the annotations corresponding to the loop invariant must
be moved from the new statement to the old one. *)
+(**************************************************************************)
+(**************************** Nested loops ********************************)
+(**************************************************************************)
+
+val mk_nested_loops:
+ loc:location -> (Env.t -> stmt list * Env.t) -> kernel_function -> Env.t ->
+ Lscope.lscope_var list -> stmt list * Env.t
+(** [mk_nested_loops ~loc mk_innermost_block kf env lvars] creates nested
+ loops (with the proper statements for initializing the loop counters)
+ from the list of logic variables [lvars]. Quantified variables create
+ loops while let-bindings simply create new variables.
+ The [mk_innermost_block] closure creates the statements of the innermost
+ block. *)
+
+(**************************************************************************)
+(********************** Forward references ********************************)
+(**************************************************************************)
+
+val translate_named_predicate_ref:
+ (kernel_function -> Env.t -> predicate -> Env.t) ref
+
+val term_to_exp_ref:
+ (kernel_function -> Env.t -> term -> exp * Env.t) ref
+
(*
Local Variables:
compile-command: "make"
diff --git a/src/plugins/e-acsl/lscope.ml b/src/plugins/e-acsl/lscope.ml
new file mode 100644
index 0000000000000000000000000000000000000000..e3c50676d35aa7e0f3c9aea1ecbc1ccd8aac5e50
--- /dev/null
+++ b/src/plugins/e-acsl/lscope.ml
@@ -0,0 +1,64 @@
+(**************************************************************************)
+(* *)
+(* This file is part of Frama-C. *)
+(* *)
+(* Copyright (C) 2007-2018 *)
+(* CEA (Commissariat à l'énergie atomique et aux énergies *)
+(* alternatives) *)
+(* *)
+(* you can redistribute it and/or modify it under the terms of the GNU *)
+(* Lesser General Public License as published by the Free Software *)
+(* Foundation, version 2.1. *)
+(* *)
+(* It is distributed in the hope that it will be useful, *)
+(* but WITHOUT ANY WARRANTY; without even the implied warranty of *)
+(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the *)
+(* GNU Lesser General Public License for more details. *)
+(* *)
+(* See the GNU Lesser General Public License version 2.1 *)
+(* for more details (enclosed in the file licenses/LGPLv2.1). *)
+(* *)
+(**************************************************************************)
+
+open Cil_types
+
+type lscope_var =
+ | Lvs_let of logic_var * term
+ | Lvs_quantif of term * relation * logic_var * relation * term
+ | Lvs_formal of logic_var * logic_info
+ | Lvs_global of logic_var * term
+
+type t = lscope_var list
+(* The logic scope is usually small, so a list is fine instead of a Map *)
+
+let empty = []
+
+let is_empty = function [] -> true | _ :: _ -> false
+
+let add lscope_var t = lscope_var :: t
+
+let get_all t = List.rev t
+
+let exists 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
+ List.exists is_lv t
+
+exception Lscope_used
+let is_used lscope pot =
+ let o = object inherit Visitor.frama_c_inplace
+ method !vlogic_var_use lv = match lv.lv_origin with
+ | Some _ -> Cil.SkipChildren
+ | None -> if exists lv lscope then raise Lscope_used else Cil.SkipChildren
+ end
+ in
+ try
+ (match pot with
+ | Misc.PoT_pred p -> ignore (Visitor.visitFramacPredicate o p)
+ | Misc.PoT_term t -> ignore (Visitor.visitFramacTerm o t));
+ false
+ with Lscope_used ->
+ true
\ No newline at end of file
diff --git a/src/plugins/e-acsl/lscope.mli b/src/plugins/e-acsl/lscope.mli
new file mode 100644
index 0000000000000000000000000000000000000000..d3c80d15fe87391bc9ec129f10fad2c0201bd5a6
--- /dev/null
+++ b/src/plugins/e-acsl/lscope.mli
@@ -0,0 +1,53 @@
+(**************************************************************************)
+(* *)
+(* This file is part of Frama-C. *)
+(* *)
+(* Copyright (C) 2007-2018 *)
+(* CEA (Commissariat à l'énergie atomique et aux énergies *)
+(* alternatives) *)
+(* *)
+(* you can redistribute it and/or modify it under the terms of the GNU *)
+(* Lesser General Public License as published by the Free Software *)
+(* Foundation, version 2.1. *)
+(* *)
+(* It is distributed in the hope that it will be useful, *)
+(* but WITHOUT ANY WARRANTY; without even the implied warranty of *)
+(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the *)
+(* GNU Lesser General Public License for more details. *)
+(* *)
+(* See the GNU Lesser General Public License version 2.1 *)
+(* for more details (enclosed in the file licenses/LGPLv2.1). *)
+(* *)
+(**************************************************************************)
+
+open Cil_types
+
+(* Handle the logic scope of a term.
+ 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 =
+ | Lvs_let of logic_var * term (* the expression to which the lv is binded *)
+ | Lvs_quantif of term * relation * logic_var * relation * term
+ | Lvs_formal of logic_var * logic_info (* the logic definition *)
+ | Lvs_global of logic_var * term (* same as Lvs_let *)
+
+type t
+
+val empty: t
+(* Create an empty logic scope. *)
+
+val is_empty: t -> bool
+(* Check whether the given logic scope is empty. *)
+
+val add: lscope_var -> t -> t
+(* Return a new logic scope in which the given [lscope_var] has been added. *)
+
+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 is_used: t -> Misc.pred_or_term -> bool
+(* [is_used lscope pot] returns [true] iff [pot] uses a variable from
+ [lscope]. *)
\ No newline at end of file
diff --git a/src/plugins/e-acsl/misc.ml b/src/plugins/e-acsl/misc.ml
index 1b48696679d33a0787c9f6c037b71bfe04f58fc2..89ff5794ca4f86d4f852934c90980b13b402ce82 100644
--- a/src/plugins/e-acsl/misc.ml
+++ b/src/plugins/e-acsl/misc.ml
@@ -290,6 +290,22 @@ let is_bitfield_pointers lty =
else
is_bitfield_pointer lty
+exception Lv_from_vi_found
+let term_has_lv_from_vi t =
+ 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
+
(*
Local Variables:
compile-command: "make"
diff --git a/src/plugins/e-acsl/misc.mli b/src/plugins/e-acsl/misc.mli
index 9dbd86e33fb00aada379667e35a442dbe818dc59..006fa6d4383a0f783d87aa82d747c40d63861d08 100644
--- a/src/plugins/e-acsl/misc.mli
+++ b/src/plugins/e-acsl/misc.mli
@@ -114,6 +114,12 @@ val is_bitfield_pointers: logic_type -> bool
(* 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
+ a C varinfo, that is a non-purely logic variable. *)
+
+type pred_or_term = PoT_pred of predicate | PoT_term of term
+
(*
Local Variables:
compile-command: "make"
diff --git a/src/plugins/e-acsl/quantif.ml b/src/plugins/e-acsl/quantif.ml
index 1af799e81cb0016bd6acfbb8e252ab538c51aa2b..fa8fc69a5ef68fe8f93d9ae7f14cafd5a645804f 100644
--- a/src/plugins/e-acsl/quantif.ml
+++ b/src/plugins/e-acsl/quantif.ml
@@ -25,12 +25,8 @@ open Cil
open Cil_datatype
let predicate_to_exp_ref
- : (kernel_function -> Env.t -> predicate -> exp * Env.t) ref
- = Extlib.mk_fun "named_predicate_to_exp_ref"
-
-let term_to_exp_ref
- : (kernel_function -> Env.t -> term -> exp * Env.t) ref
- = Extlib.mk_fun "term_to_exp_ref"
+ : (kernel_function -> Env.t -> predicate -> exp * Env.t) ref
+ = Extlib.mk_fun "named_predicate_to_exp_ref"
let compute_quantif_guards quantif bounded_vars hyps =
let error msg pp x =
@@ -92,13 +88,13 @@ let compute_quantif_guards quantif bounded_vars hyps =
(match vars with
| [] -> ()
| _ :: _ ->
- let msg =
+ let msg =
Format.asprintf
- "@[unguarded variable%s %tin quantification@ %a@]"
- (if List.length vars = 1 then "" else "s")
- (fun fmt ->
+ "@[unguarded variable%s %tin quantification@ %a@]"
+ (if List.length vars = 1 then "" else "s")
+ (fun fmt ->
List.iter
- (fun v -> Format.fprintf fmt "@[%a @]" Printer.pp_logic_var v)
+ (fun v -> Format.fprintf fmt "@[%a @]" Printer.pp_logic_var v)
vars)
Printer.pp_predicate quantif
in
@@ -107,22 +103,30 @@ let compute_quantif_guards quantif bounded_vars hyps =
let () = Typing.compute_quantif_guards_ref := compute_quantif_guards
-module Label_ids =
+module Label_ids =
State_builder.Counter(struct let name = "E_ACSL.Label_ids" end)
let convert kf env loc is_forall p bounded_vars hyps goal =
- (* part depending on the kind of quantifications
+ (* part depending on the kind of quantifications
(either universal or existential) *)
- let init_val, found_val, mk_guard =
+ let init_val, found_val, mk_guard =
let z = zero ~loc in
let o = one ~loc in
- if is_forall then o, z, (fun x -> x)
+ if is_forall then o, z, (fun x -> x)
else z, o, (fun e -> new_exp ~loc:e.eloc (UnOp(LNot, e, intType)))
in
- let named_predicate_to_exp = !predicate_to_exp_ref in
- let term_to_exp = !term_to_exp_ref in
(* universal quantification over integers (or a subtype of integer) *)
let guards = compute_quantif_guards p bounded_vars hyps in
+ (* transform [guards] into [lscope_var list],
+ and update logic scope in the process *)
+ let lvs_guards, env = List.fold_right
+ (fun (t1, rel1, lv, rel2, t2) (lvs_guards, env) ->
+ let lvs = Lscope.Lvs_quantif(t1, rel1, lv, rel2, t2) in
+ let env = Env.Logic_scope.extend env lvs in
+ lvs :: lvs_guards, env)
+ guards
+ ([], env)
+ in
let var_res, res, env =
(* variable storing the result of the quantifier *)
let name = if is_forall then "forall" else "exists" in
@@ -133,149 +137,39 @@ let convert kf env loc is_forall p bounded_vars hyps goal =
None
intType
(fun v _ ->
- let lv = var v in
- [ mkStmtOneInstr ~valid_sid:true (Set(lv, init_val, loc)) ])
+ let lv = var v in
+ [ mkStmtOneInstr ~valid_sid:true (Set(lv, init_val, loc)) ])
in
let end_loop_ref = ref dummyStmt in
- let rec mk_for_loop env = function
- | [] ->
- (* innermost loop body: store the result in [res] and go out according
- to evaluation of the goal *)
- let test, env = named_predicate_to_exp kf (Env.push env) goal in
- let then_block = mkBlock [ mkEmptyStmt ~loc () ] in
- let else_block =
- (* use a 'goto', not a simple 'break' in order to handle 'forall' with
- multiple binders (leading to imbricated loops) *)
- mkBlock
- [ mkStmtOneInstr
- ~valid_sid:true (Set(var var_res, found_val, loc));
- mkStmt ~valid_sid:true (Goto(end_loop_ref, loc)) ]
- in
- let blk, env =
- Env.pop_and_get
- env
- (mkStmt ~valid_sid:true
- (If(mk_guard test, then_block, else_block, loc)))
- ~global_clear:false
- Env.After
- in
- let blk = Cil.flatten_transient_sub_blocks blk in
- [ mkStmt ~valid_sid:true (Block blk) ], env
- | (t1, rel1, logic_x, rel2, t2) :: tl ->
- let ctx =
- let ty1 = Typing.get_integer_ty t1 in
- let ty2 = Typing.get_integer_ty t2 in
- Typing.join ty1 ty2
- in
- let t_plus_one ?ty t =
- (* whenever provided, [ty] is known to be the type of the result *)
- let tone = Logic_const.tinteger ~loc 1 in
- let res = Logic_const.term ~loc (TBinOp(PlusA, t, tone)) Linteger in
- Extlib.may
- (fun ty ->
- Typing.unsafe_set tone ~ctx:ty ctx;
- Typing.unsafe_set t ~ctx:ty ctx;
- Typing.unsafe_set res ty)
- ty;
- res
- in
- let t1 = match rel1 with
- | Rlt ->
- let t = t_plus_one t1 in
- Typing.type_term ~use_gmp_opt:false ~ctx t;
- t
- | Rle -> t1
- | Rgt | Rge | Req | Rneq -> assert false
- in
- let t2_one, bop2 = match rel2 with
- | Rlt -> t2, Lt
- | Rle ->
- (* we increment the loop counter one more time (at the end of the
- loop). Thus to prevent overflow, check the type of [t2+1]
- instead of [t2]. *)
- t_plus_one t2, Le
- | Rgt | Rge | Req | Rneq -> assert false
- in
- Typing.type_term ~use_gmp_opt:false ~ctx t2_one;
- let ctx_one =
- let ty1 = Typing.get_integer_ty t1 in
- let ty2 = Typing.get_integer_ty t2_one in
- Typing.join ty1 ty2
- in
- let ty =
- try Typing.typ_of_integer_ty ctx_one
- with Typing.Not_an_integer -> assert false
- in
- (* loop counter corresponding to the quantified variable *)
- let var_x, x, env = Env.Logic_binding.add ~ty env logic_x in
- let lv_x = var var_x in
- let env = match ctx_one with
- | Typing.C_type _ -> env
- | Typing.Gmp -> Env.add_stmt env (Gmpz.init ~loc x)
- | Typing.Other -> assert false
- in
- (* build the inner loops and loop body *)
- let body, env = mk_for_loop env tl in
- (* initialize the loop counter to [t1] *)
- let e1, env = term_to_exp kf (Env.push env) t1 in
- let init_blk, env =
- Env.pop_and_get
- env
- (Gmpz.affect ~loc:e1.eloc lv_x x e1)
- ~global_clear:false
- Env.Middle
- in
- (* generate the guard [x bop t2] *)
- let stmts_block b = [ mkStmt ~valid_sid:true (Block b) ] in
- let tlv = Logic_const.tvar ~loc logic_x in
- let guard =
- (* must copy [t2] to force being typed again *)
- Logic_const.term ~loc
- (TBinOp(bop2, tlv, { t2 with term_node = t2.term_node } )) Linteger
- in
- Typing.type_term ~use_gmp_opt:false ~ctx:Typing.c_int guard;
- let guard_exp, env = term_to_exp kf (Env.push env) guard in
- let break_stmt = mkStmt ~valid_sid:true (Break guard_exp.eloc) in
- let guard_blk, env =
- Env.pop_and_get
- env
- (mkStmt ~valid_sid:true
- (If(guard_exp,
- mkBlock [ mkEmptyStmt ~loc () ],
- mkBlock [ break_stmt ],
- guard_exp.eloc)))
- ~global_clear:false
- Env.Middle
- in
- let guard = stmts_block guard_blk in
- (* increment the loop counter [x++];
- previous typing ensures that [x++] fits type [ty] *)
- (* TODO: should check that it does not overflow in the case of the type
- of the loop variable is __declared__ too small. *)
- let tlv_one = t_plus_one ~ty:ctx_one tlv in
- let incr, env = term_to_exp kf (Env.push env) tlv_one in
- let next_blk, env =
- Env.pop_and_get
- env
- (Gmpz.affect ~loc:incr.eloc lv_x x incr)
- ~global_clear:false
- Env.Middle
- in
- (* generate the whole loop *)
- let start = stmts_block init_blk in
- let next = stmts_block next_blk in
- start @
- [ mkStmt ~valid_sid:true
- (Loop ([],
- mkBlock (guard @ body @ next),
- loc,
- None,
- Some break_stmt)) ],
+ (* innermost block *)
+ let mk_innermost_block env =
+ (* innermost loop body: store the result in [res] and go out according
+ to evaluation of the goal *)
+ let named_predicate_to_exp = !predicate_to_exp_ref in
+ let test, env = named_predicate_to_exp kf (Env.push env) goal in
+ let then_block = mkBlock [ mkEmptyStmt ~loc () ] in
+ let else_block =
+ (* use a 'goto', not a simple 'break' in order to handle 'forall' with
+ multiple binders (leading to imbricated loops) *)
+ mkBlock
+ [ mkStmtOneInstr ~valid_sid:true (Set(var var_res, found_val, loc));
+ mkStmt ~valid_sid:true (Goto(end_loop_ref, loc)) ]
+ in
+ let blk, env = Env.pop_and_get
env
+ (mkStmt ~valid_sid:true
+ (If(mk_guard test, then_block, else_block, loc)))
+ ~global_clear:false
+ Env.After
+ in
+ let blk = Cil.flatten_transient_sub_blocks blk in
+ [ mkStmt ~valid_sid:true (Block blk) ], env
+ in
+ let stmts, env =
+ Loops.mk_nested_loops ~loc mk_innermost_block kf env lvs_guards
in
- let stmts, env = mk_for_loop env guards in
- let env =
- Env.add_stmt env (mkStmt ~valid_sid:true (Block (mkBlock stmts)))
+ let env =
+ Env.add_stmt env (mkStmt ~valid_sid:true (Block (mkBlock stmts)))
in
(* where to jump to go out of the loop *)
let end_loop = mkEmptyStmt ~loc () in
@@ -284,16 +178,15 @@ let convert kf env loc is_forall p bounded_vars hyps goal =
end_loop.labels <- label :: end_loop.labels;
end_loop_ref := end_loop;
let env = Env.add_stmt env end_loop in
- let env = List.fold_left Env.Logic_binding.remove env bounded_vars in
res, env
-let quantif_to_exp kf env p =
+let quantif_to_exp kf env p =
let loc = p.pred_loc in
match p.pred_content with
- | Pforall(bounded_vars, { pred_content = Pimplies(hyps, goal) }) ->
+ | Pforall(bounded_vars, { pred_content = Pimplies(hyps, goal) }) ->
convert kf env loc true p bounded_vars hyps goal
| Pforall _ -> Error.not_yet "unguarded \\forall quantification"
- | Pexists(bounded_vars, { pred_content = Pand(hyps, goal) }) ->
+ | Pexists(bounded_vars, { pred_content = Pand(hyps, goal) }) ->
convert kf env loc false p bounded_vars hyps goal
| Pexists _ -> Error.not_yet "unguarded \\exists quantification"
| _ -> assert false
diff --git a/src/plugins/e-acsl/quantif.mli b/src/plugins/e-acsl/quantif.mli
index 5e67e747265d04f8e59d363a103d6bab672d3a26..d8e8b9819c91d418be5d6f9b207e7f7dd8f2f58e 100644
--- a/src/plugins/e-acsl/quantif.mli
+++ b/src/plugins/e-acsl/quantif.mli
@@ -24,19 +24,17 @@
open Cil_types
-val quantif_to_exp: kernel_function -> Env.t -> predicate -> exp * Env.t
+val quantif_to_exp:
+ kernel_function -> Env.t -> predicate -> exp * Env.t
(** The given predicate must be a quantification. *)
(* ***********************************************************************)
(** {2 Forward references} *)
(* ***********************************************************************)
-val predicate_to_exp_ref:
+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
-
(*
Local Variables:
compile-command: "make"
diff --git a/src/plugins/e-acsl/tests/gmp/at_on-purely-logic-variables.c b/src/plugins/e-acsl/tests/gmp/at_on-purely-logic-variables.c
new file mode 100644
index 0000000000000000000000000000000000000000..a289de1d5a1c02e97bd12f1f5205a24c93639039
--- /dev/null
+++ b/src/plugins/e-acsl/tests/gmp/at_on-purely-logic-variables.c
@@ -0,0 +1,69 @@
+/* run.config
+ COMMENT: \at on purely logic variables
+ COMMENT:
+*/
+
+/*@ 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) {}
+
+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;
+ L: ;
+ n = 9;
+ K: ;
+ n = 666;
+
+ // Predicates:
+ /*@ assert \let i = 3; \at(n + i == 10, L); */ ;
+ /*@ assert \exists integer j; 2 <= j < 5 && \at(n + j == 11, L); */ ;
+ /*@ assert
+ \let k = -7;
+ \exists integer u; 9 <= u < 21 &&
+ \forall integer v; -5 < v <= 6 ==>
+ \at((u > 0 ? n + k : u + v) > 0, K); */ ;
+
+ // Terms:
+ /*@ assert \let i = 3; \at(n + i, L) == 10; */ ;
+ unsigned int m = 3;
+ G: ;
+ m = -3;
+ /*@ assert \exists integer k; -9 < k < 0 && \at(m + k, G) == 0; */ ;
+ /*@ assert
+ \exists integer u; 9 <= u < 21 &&
+ \forall integer v; -5 < v <= (u < 15 ? u + 6 : 3) ==>
+ \at(n + u + v > 0, K); */ ;
+
+ // Function calls:
+ int t[5] = {9, 12, 12, 12, -4};
+ f(t);
+ g();
+
+ // Name capturing
+ /*@ assert
+ \exists integer u; 10 <= u < 20
+ && \exists integer v; -10 < v <= -5 + (\let u = -2; u) // another u
+ && \exists integer w; 100 < w <= 200
+ && \at(n - u +
+ (\let u = 42; u) // yet another u
+ + v + w > 0, K); */ ;
+
+ // Not yet:
+ /*@ assert
+ \exists integer j; 2 <= j < 10000000000000000 // too big => not_yet
+ && \at(n + j == 11, L); */ ;
+ /*@ assert \let i = n; // lv defined with C var => not_yet
+ \at(n + i == 10, L); */ ;
+
+ return 0;
+}
\ No newline at end of file
diff --git a/src/plugins/e-acsl/tests/gmp/oracle/at_on-purely-logic-variables.0.res.oracle b/src/plugins/e-acsl/tests/gmp/oracle/at_on-purely-logic-variables.0.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..5170b1fe4ba40ee38526fcf4da7a7232988f4b14
--- /dev/null
+++ b/src/plugins/e-acsl/tests/gmp/oracle/at_on-purely-logic-variables.0.res.oracle
@@ -0,0 +1,163 @@
+[e-acsl] beginning translation.
+[e-acsl] tests/gmp/at_on-purely-logic-variables.c:64: 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/gmp/at_on-purely-logic-variables.c:65: Warning:
+ E-ACSL construct `\at with logic variable linked to C variable'
+ 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] tests/gmp/at_on-purely-logic-variables.c:57:
+ allocating variable __malloc_main_l57
+[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/gmp/at_on-purely-logic-variables.c:29:
+ starting to merge loop iterations
+[eva] tests/gmp/at_on-purely-logic-variables.c:57:
+ starting to merge loop iterations
+[eva:alarm] tests/gmp/at_on-purely-logic-variables.c:57: Warning:
+ out of bounds write.
+ assert
+ \valid(__gen_e_acsl_at_7 +
+ (int)((int)((int)(__gen_e_acsl_u_6 - 10) * 300) +
+ (int)((int)((int)((int)(__gen_e_acsl_v_6 - -10) - 1) * 100) +
+ (int)((int)(__gen_e_acsl_w_2 - 100) - 1))));
+[eva] tests/gmp/at_on-purely-logic-variables.c:45:
+ starting to merge loop iterations
+[eva] tests/gmp/at_on-purely-logic-variables.c:34:
+ starting to merge loop iterations
+[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/gmp/at_on-purely-logic-variables.c:29: Warning:
+ assertion got status unknown.
+[eva:alarm] tests/gmp/at_on-purely-logic-variables.c:29: Warning:
+ accessing uninitialized left-value.
+ assert \initialized(__gen_e_acsl_at_2 + (__gen_e_acsl_j - 2));
+[eva] tests/gmp/at_on-purely-logic-variables.c:29:
+ starting to merge loop iterations
+[eva:alarm] tests/gmp/at_on-purely-logic-variables.c:29: Warning:
+ function __e_acsl_assert: precondition got status unknown.
+[eva:alarm] tests/gmp/at_on-purely-logic-variables.c:29: Warning:
+ function __e_acsl_assert: precondition got status unknown.
+[eva:alarm] tests/gmp/at_on-purely-logic-variables.c:31: Warning:
+ assertion got status unknown.
+[eva:alarm] tests/gmp/at_on-purely-logic-variables.c:33: Warning:
+ accessing uninitialized left-value.
+ assert
+ \initialized(__gen_e_acsl_at_3 +
+ ((__gen_e_acsl_u - 9) * 11 + ((__gen_e_acsl_v - -5) - 1)));
+[eva] tests/gmp/at_on-purely-logic-variables.c:33:
+ starting to merge loop iterations
+[eva:alarm] tests/gmp/at_on-purely-logic-variables.c:34: Warning:
+ function __e_acsl_assert: precondition got status unknown.
+[eva:alarm] tests/gmp/at_on-purely-logic-variables.c:37: Warning:
+ assertion got status unknown.
+[eva] tests/gmp/at_on-purely-logic-variables.c:41:
+ starting to merge loop iterations
+[eva:alarm] tests/gmp/at_on-purely-logic-variables.c:41: Warning:
+ assertion got status unknown.
+[eva:alarm] tests/gmp/at_on-purely-logic-variables.c:41: Warning:
+ accessing uninitialized left-value.
+ assert \initialized(__gen_e_acsl_at_5 + ((__gen_e_acsl_k_3 - -9) - 1));
+[eva] tests/gmp/at_on-purely-logic-variables.c:41:
+ starting to merge loop iterations
+[eva:alarm] tests/gmp/at_on-purely-logic-variables.c:41: Warning:
+ function __e_acsl_assert: precondition got status unknown.
+[eva:alarm] tests/gmp/at_on-purely-logic-variables.c:41: Warning:
+ function __e_acsl_assert: precondition got status unknown.
+[eva:alarm] tests/gmp/at_on-purely-logic-variables.c:43: Warning:
+ assertion got status unknown.
+[eva:alarm] tests/gmp/at_on-purely-logic-variables.c:44: Warning:
+ accessing uninitialized left-value.
+ assert
+ \initialized(__gen_e_acsl_at_6 +
+ ((__gen_e_acsl_u_3 - 9) * 32 + ((__gen_e_acsl_v_3 - -5) - 1)));
+[eva] tests/gmp/at_on-purely-logic-variables.c:44:
+ starting to merge loop iterations
+[eva:alarm] tests/gmp/at_on-purely-logic-variables.c:45: Warning:
+ function __e_acsl_assert: precondition got status unknown.
+[eva] tests/gmp/at_on-purely-logic-variables.c:8:
+ allocating variable __malloc___gen_e_acsl_f_l8
+[eva] tests/gmp/at_on-purely-logic-variables.c:8:
+ allocating variable __malloc___gen_e_acsl_f_l8_0
+[eva] tests/gmp/at_on-purely-logic-variables.c:7:
+ allocating variable __malloc___gen_e_acsl_f_l7
+[eva] tests/gmp/at_on-purely-logic-variables.c:7:
+ allocating variable __malloc___gen_e_acsl_f_l7_0
+[eva] tests/gmp/at_on-purely-logic-variables.c:7:
+ starting to merge loop iterations
+[eva] tests/gmp/at_on-purely-logic-variables.c:7:
+ starting to merge loop iterations
+[eva] using specification for function __e_acsl_delete_block
+[eva:alarm] tests/gmp/at_on-purely-logic-variables.c:7: Warning:
+ accessing uninitialized left-value.
+ assert \initialized(__gen_e_acsl_at + ((__gen_e_acsl_n - 1) - 1));
+[eva:alarm] tests/gmp/at_on-purely-logic-variables.c:7: Warning:
+ accessing uninitialized left-value.
+ assert \initialized(__gen_e_acsl_at_2 + ((__gen_e_acsl_n - 1) - 1));
+[eva] tests/gmp/at_on-purely-logic-variables.c:6:
+ starting to merge loop iterations
+[eva:alarm] tests/gmp/at_on-purely-logic-variables.c:7: Warning:
+ function __e_acsl_assert: precondition got status unknown.
+[eva:alarm] tests/gmp/at_on-purely-logic-variables.c:7: Warning:
+ function __e_acsl_assert: precondition got status unknown.
+[eva:alarm] tests/gmp/at_on-purely-logic-variables.c:6: Warning:
+ function __gen_e_acsl_f: postcondition got status unknown.
+[eva:alarm] tests/gmp/at_on-purely-logic-variables.c:8: Warning:
+ function __gen_e_acsl_f: postcondition got status unknown.
+[eva] tests/gmp/at_on-purely-logic-variables.c:16:
+ allocating variable __malloc_g_l16
+[eva] tests/gmp/at_on-purely-logic-variables.c:16:
+ starting to merge loop iterations
+[eva:alarm] tests/gmp/at_on-purely-logic-variables.c:16: Warning:
+ assertion got status unknown.
+[eva:alarm] tests/gmp/at_on-purely-logic-variables.c:16: Warning:
+ accessing uninitialized left-value.
+ assert \initialized(__gen_e_acsl_at + (__gen_e_acsl_w - 3));
+[eva] tests/gmp/at_on-purely-logic-variables.c:16:
+ starting to merge loop iterations
+[eva:alarm] tests/gmp/at_on-purely-logic-variables.c:16: Warning:
+ function __e_acsl_assert: precondition got status unknown.
+[eva:alarm] tests/gmp/at_on-purely-logic-variables.c:16: Warning:
+ function __e_acsl_assert: precondition got status unknown.
+[eva:alarm] tests/gmp/at_on-purely-logic-variables.c:54: Warning:
+ assertion got status unknown.
+[eva:alarm] tests/gmp/at_on-purely-logic-variables.c:56: Warning:
+ accessing uninitialized left-value.
+ assert
+ \initialized(__gen_e_acsl_at_7 +
+ ((__gen_e_acsl_u_5 - 10) * 300 +
+ (((__gen_e_acsl_v_5 - -10) - 1) * 100 +
+ ((__gen_e_acsl_w - 100) - 1))));
+[eva:alarm] tests/gmp/at_on-purely-logic-variables.c:63: Warning:
+ assertion got status unknown.
+[eva:alarm] tests/gmp/at_on-purely-logic-variables.c:65: Warning:
+ assertion got status unknown.
+[eva] using specification for function __e_acsl_memory_clean
+[eva] done for function main
diff --git a/src/plugins/e-acsl/tests/gmp/oracle/at_on-purely-logic-variables.1.res.oracle b/src/plugins/e-acsl/tests/gmp/oracle/at_on-purely-logic-variables.1.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..1e6a8533f45e6676b9d6c5b3062032e0c04185bd
--- /dev/null
+++ b/src/plugins/e-acsl/tests/gmp/oracle/at_on-purely-logic-variables.1.res.oracle
@@ -0,0 +1,98 @@
+[e-acsl] beginning translation.
+[e-acsl] tests/gmp/at_on-purely-logic-variables.c:16: 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/gmp/at_on-purely-logic-variables.c:28: 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/gmp/at_on-purely-logic-variables.c:29: 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/gmp/at_on-purely-logic-variables.c:34: 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/gmp/at_on-purely-logic-variables.c:37: Warning:
+ E-ACSL construct `\at on purely logic variables and over gmp type'
+ is not yet supported.
+ Ignoring annotation.
+[e-acsl] tests/gmp/at_on-purely-logic-variables.c:41: Warning:
+ E-ACSL construct `\at on purely logic variables and over gmp type'
+ is not yet supported.
+ Ignoring annotation.
+[e-acsl] tests/gmp/at_on-purely-logic-variables.c:45: Warning:
+ E-ACSL construct
+ `\at on purely logic variables and with quantifier that uses too complex bound (E-ACSL cannot infer a finite upper bound to it)'
+ is not yet supported.
+ Ignoring annotation.
+[e-acsl] tests/gmp/at_on-purely-logic-variables.c:57: 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/gmp/at_on-purely-logic-variables.c:64: 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/gmp/at_on-purely-logic-variables.c:65: Warning:
+ E-ACSL construct `\at with logic variable linked to C variable'
+ is not yet supported.
+ Ignoring annotation.
+[e-acsl] tests/gmp/at_on-purely-logic-variables.c:7: 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/gmp/at_on-purely-logic-variables.c:8: 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] 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_full_init
+[eva:alarm] tests/gmp/at_on-purely-logic-variables.c:28: Warning:
+ assertion got status unknown.
+[eva:alarm] tests/gmp/at_on-purely-logic-variables.c:29: Warning:
+ assertion got status unknown.
+[eva:alarm] tests/gmp/at_on-purely-logic-variables.c:31: Warning:
+ assertion got status unknown.
+[eva:alarm] tests/gmp/at_on-purely-logic-variables.c:37: Warning:
+ assertion got status unknown.
+[eva:alarm] tests/gmp/at_on-purely-logic-variables.c:41: Warning:
+ assertion got status unknown.
+[eva:alarm] tests/gmp/at_on-purely-logic-variables.c:43: Warning:
+ assertion got status unknown.
+[eva] using specification for function __e_acsl_delete_block
+[eva:alarm] tests/gmp/at_on-purely-logic-variables.c:6: Warning:
+ function __gen_e_acsl_f: postcondition got status unknown.
+[eva:alarm] tests/gmp/at_on-purely-logic-variables.c:8: Warning:
+ function __gen_e_acsl_f: postcondition got status unknown.
+[eva:alarm] tests/gmp/at_on-purely-logic-variables.c:16: Warning:
+ assertion got status unknown.
+[eva:alarm] tests/gmp/at_on-purely-logic-variables.c:54: Warning:
+ assertion got status unknown.
+[eva:alarm] tests/gmp/at_on-purely-logic-variables.c:63: Warning:
+ assertion got status unknown.
+[eva:alarm] tests/gmp/at_on-purely-logic-variables.c:65: Warning:
+ assertion got status unknown.
+[eva] using specification for function __e_acsl_memory_clean
+[eva] done for function main
diff --git a/src/plugins/e-acsl/tests/gmp/oracle/gen_at_on-purely-logic-variables.c b/src/plugins/e-acsl/tests/gmp/oracle/gen_at_on-purely-logic-variables.c
new file mode 100644
index 0000000000000000000000000000000000000000..c6f65b06f7c80ea452bdd467b56a65ec502f71f2
--- /dev/null
+++ b/src/plugins/e-acsl/tests/gmp/oracle/gen_at_on-purely-logic-variables.c
@@ -0,0 +1,726 @@
+/* Generated by Frama-C */
+#include "stdio.h"
+#include "stdlib.h"
+/*@ ensures
+ ∀ ℤ 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 __gen_e_acsl_f(int *t);
+
+void f(int *t)
+{
+ __e_acsl_store_block((void *)(& t),(size_t)8);
+ __e_acsl_delete_block((void *)(& t));
+ return;
+}
+
+void g(void)
+{
+ int *__gen_e_acsl_at;
+ int m;
+ __gen_e_acsl_at = (int *)malloc((size_t)12);
+ m = 8;
+ Q:
+ {
+ {
+ int __gen_e_acsl_w_2;
+ __gen_e_acsl_w_2 = 3;
+ while (1) {
+ if (__gen_e_acsl_w_2 < 6) ; else break;
+ *(__gen_e_acsl_at + (__gen_e_acsl_w_2 - 3)) = m + (long)__gen_e_acsl_w_2 == 12L;
+ __gen_e_acsl_w_2 ++;
+ }
+ }
+ ;
+ }
+ m = 10;
+ /*@ assert ∃ ℤ w; 3 ≤ w < 6 ∧ \at(m + w ≡ 12,Q); */
+ {
+ int __gen_e_acsl_exists;
+ int __gen_e_acsl_w;
+ __gen_e_acsl_exists = 0;
+ __gen_e_acsl_w = 3;
+ while (1) {
+ if (__gen_e_acsl_w < 6) ; else break;
+ {
+ int __gen_e_acsl_valid_read;
+ __gen_e_acsl_valid_read = __e_acsl_valid_read((void *)(__gen_e_acsl_at + (int)(
+ __gen_e_acsl_w - 3L)),
+ sizeof(int),
+ (void *)__gen_e_acsl_at,
+ (void *)(& __gen_e_acsl_at));
+ __e_acsl_assert(__gen_e_acsl_valid_read,(char *)"RTE",(char *)"g",
+ (char *)"mem_access: \\valid_read(__gen_e_acsl_at + (int)(__gen_e_acsl_w - 3))",
+ 16);
+ /*@ assert
+ Value: initialization:
+ \initialized(__gen_e_acsl_at + (__gen_e_acsl_w - 3));
+ */
+ if (! *(__gen_e_acsl_at + (__gen_e_acsl_w - 3))) ;
+ else {
+ __gen_e_acsl_exists = 1;
+ goto e_acsl_end_loop1;
+ }
+ }
+ __gen_e_acsl_w ++;
+ }
+ e_acsl_end_loop1: ;
+ __e_acsl_assert(__gen_e_acsl_exists,(char *)"Assertion",(char *)"g",
+ (char *)"\\exists integer w; 3 <= w < 6 && \\at(m + w == 12,Q)",
+ 16);
+ }
+ free((void *)__gen_e_acsl_at);
+ return;
+}
+
+int main(void)
+{
+ int *__gen_e_acsl_at_7;
+ int *__gen_e_acsl_at_6;
+ long *__gen_e_acsl_at_5;
+ long *__gen_e_acsl_at_4;
+ int *__gen_e_acsl_at_3;
+ int *__gen_e_acsl_at_2;
+ int *__gen_e_acsl_at;
+ int __retres;
+ int n;
+ __e_acsl_memory_init((int *)0,(char ***)0,(size_t)8);
+ __gen_e_acsl_at_7 = (int *)malloc((size_t)12000);
+ __gen_e_acsl_at_6 = (int *)malloc((size_t)1536);
+ __gen_e_acsl_at_5 = (long *)malloc((size_t)64);
+ __gen_e_acsl_at_4 = (long *)malloc((size_t)8);
+ __gen_e_acsl_at_3 = (int *)malloc((size_t)528);
+ __gen_e_acsl_at_2 = (int *)malloc((size_t)12);
+ __gen_e_acsl_at = (int *)malloc((size_t)4);
+ __e_acsl_store_block((void *)(& n),(size_t)4);
+ __e_acsl_full_init((void *)(& n));
+ n = 7;
+ L:
+ {
+ {
+ int __gen_e_acsl_i_4;
+ __gen_e_acsl_i_4 = 3;
+ *(__gen_e_acsl_at_4 + 0) = n + (long)__gen_e_acsl_i_4;
+ }
+ {
+ int __gen_e_acsl_j_2;
+ __gen_e_acsl_j_2 = 2;
+ while (1) {
+ if (__gen_e_acsl_j_2 < 5) ; else break;
+ *(__gen_e_acsl_at_2 + (__gen_e_acsl_j_2 - 2)) = n + (long)__gen_e_acsl_j_2 == 11L;
+ __gen_e_acsl_j_2 ++;
+ }
+ }
+ {
+ int __gen_e_acsl_i_2;
+ __gen_e_acsl_i_2 = 3;
+ *(__gen_e_acsl_at + 0) = n + (long)__gen_e_acsl_i_2 == 10L;
+ }
+ ;
+ }
+ __e_acsl_full_init((void *)(& n));
+ n = 9;
+ K:
+ {
+ {
+ int __gen_e_acsl_u_6;
+ int __gen_e_acsl_v_6;
+ int __gen_e_acsl_w_2;
+ __gen_e_acsl_u_6 = 10;
+ while (1) {
+ if (__gen_e_acsl_u_6 < 20) ; else break;
+ __gen_e_acsl_v_6 = -10 + 1;
+ while (1) {
+ {
+ int __gen_e_acsl_u_8;
+ __gen_e_acsl_u_8 = -2;
+ if (__gen_e_acsl_v_6 <= -5 + __gen_e_acsl_u_8) ; else break;
+ }
+ __gen_e_acsl_w_2 = 100 + 1;
+ while (1) {
+ if (__gen_e_acsl_w_2 <= 200) ; else break;
+ {
+ int __gen_e_acsl_u_7;
+ __gen_e_acsl_u_7 = 42;
+ /*@ assert
+ Value: mem_access:
+ \valid(__gen_e_acsl_at_7 +
+ (int)((int)((int)(__gen_e_acsl_u_6 - 10) * 300) +
+ (int)((int)((int)((int)(__gen_e_acsl_v_6 -
+ -10)
+ - 1)
+ * 100)
+ +
+ (int)((int)(__gen_e_acsl_w_2 - 100) -
+ 1))));
+ */
+ *(__gen_e_acsl_at_7 + ((__gen_e_acsl_u_6 - 10) * 300 + (
+ ((__gen_e_acsl_v_6 - -10) - 1) * 100 + (
+ (__gen_e_acsl_w_2 - 100) - 1)))) =
+ (((n - (long)__gen_e_acsl_u_6) + __gen_e_acsl_u_7) + __gen_e_acsl_v_6) + __gen_e_acsl_w_2 > 0L;
+ }
+ __gen_e_acsl_w_2 ++;
+ }
+ __gen_e_acsl_v_6 ++;
+ }
+ __gen_e_acsl_u_6 ++;
+ }
+ }
+ {
+ int __gen_e_acsl_u_4;
+ int __gen_e_acsl_v_4;
+ __gen_e_acsl_u_4 = 9;
+ while (1) {
+ if (__gen_e_acsl_u_4 < 21) ; else break;
+ __gen_e_acsl_v_4 = -5 + 1;
+ while (1) {
+ {
+ int __gen_e_acsl_if_2;
+ if (__gen_e_acsl_u_4 < 15) __gen_e_acsl_if_2 = __gen_e_acsl_u_4 + 6;
+ else __gen_e_acsl_if_2 = 3;
+ if (__gen_e_acsl_v_4 <= __gen_e_acsl_if_2) ; else break;
+ }
+ *(__gen_e_acsl_at_6 + ((__gen_e_acsl_u_4 - 9) * 32 + ((__gen_e_acsl_v_4 - -5) - 1))) =
+ (n + (long)__gen_e_acsl_u_4) + __gen_e_acsl_v_4 > 0L;
+ __gen_e_acsl_v_4 ++;
+ }
+ __gen_e_acsl_u_4 ++;
+ }
+ }
+ {
+ int __gen_e_acsl_k_2;
+ int __gen_e_acsl_u_2;
+ int __gen_e_acsl_v_2;
+ __gen_e_acsl_k_2 = -7;
+ __gen_e_acsl_u_2 = 9;
+ while (1) {
+ if (__gen_e_acsl_u_2 < 21) ; else break;
+ __gen_e_acsl_v_2 = -5 + 1;
+ while (1) {
+ if (__gen_e_acsl_v_2 <= 6) ; else break;
+ {
+ long __gen_e_acsl_if;
+ if (__gen_e_acsl_u_2 > 0) __gen_e_acsl_if = n + (long)__gen_e_acsl_k_2;
+ else __gen_e_acsl_if = __gen_e_acsl_u_2 + __gen_e_acsl_v_2;
+ *(__gen_e_acsl_at_3 + ((__gen_e_acsl_u_2 - 9) * 11 + ((__gen_e_acsl_v_2 - -5) - 1))) =
+ __gen_e_acsl_if > 0L;
+ }
+ __gen_e_acsl_v_2 ++;
+ }
+ __gen_e_acsl_u_2 ++;
+ }
+ }
+ ;
+ }
+ __e_acsl_full_init((void *)(& n));
+ n = 666;
+ /*@ assert \let i = 3; \at(n + i ≡ 10,L); */
+ {
+ int __gen_e_acsl_i;
+ int __gen_e_acsl_valid_read;
+ __gen_e_acsl_i = 3;
+ __gen_e_acsl_valid_read = __e_acsl_valid_read((void *)(__gen_e_acsl_at + 0),
+ sizeof(int),
+ (void *)__gen_e_acsl_at,
+ (void *)(& __gen_e_acsl_at));
+ __e_acsl_assert(__gen_e_acsl_valid_read,(char *)"RTE",(char *)"main",
+ (char *)"mem_access: \\valid_read(__gen_e_acsl_at + 0)",
+ 28);
+ __e_acsl_assert(*(__gen_e_acsl_at + 0),(char *)"Assertion",
+ (char *)"main",
+ (char *)"\\let i = 3; \\at(n + i == 10,L)",28);
+ }
+ /*@ assert ∃ ℤ j; 2 ≤ j < 5 ∧ \at(n + j ≡ 11,L); */
+ {
+ int __gen_e_acsl_exists;
+ int __gen_e_acsl_j;
+ __gen_e_acsl_exists = 0;
+ __gen_e_acsl_j = 2;
+ while (1) {
+ if (__gen_e_acsl_j < 5) ; else break;
+ {
+ int __gen_e_acsl_valid_read_2;
+ __gen_e_acsl_valid_read_2 = __e_acsl_valid_read((void *)(__gen_e_acsl_at_2 + (int)(
+ __gen_e_acsl_j - 2L)),
+ sizeof(int),
+ (void *)__gen_e_acsl_at_2,
+ (void *)(& __gen_e_acsl_at_2));
+ __e_acsl_assert(__gen_e_acsl_valid_read_2,(char *)"RTE",
+ (char *)"main",
+ (char *)"mem_access: \\valid_read(__gen_e_acsl_at_2 + (int)(__gen_e_acsl_j - 2))",
+ 29);
+ /*@ assert
+ Value: initialization:
+ \initialized(__gen_e_acsl_at_2 + (__gen_e_acsl_j - 2));
+ */
+ if (! *(__gen_e_acsl_at_2 + (__gen_e_acsl_j - 2))) ;
+ else {
+ __gen_e_acsl_exists = 1;
+ goto e_acsl_end_loop2;
+ }
+ }
+ __gen_e_acsl_j ++;
+ }
+ e_acsl_end_loop2: ;
+ __e_acsl_assert(__gen_e_acsl_exists,(char *)"Assertion",(char *)"main",
+ (char *)"\\exists integer j; 2 <= j < 5 && \\at(n + j == 11,L)",
+ 29);
+ }
+ /*@ assert \let k = -7;
+ ∃ ℤ u;
+ 9 ≤ u < 21 ∧
+ (∀ ℤ v; -5 < v ≤ 6 ⇒ \at((u > 0? n + k: u + v) > 0,K));
+ */
+ {
+ int __gen_e_acsl_k;
+ int __gen_e_acsl_exists_2;
+ int __gen_e_acsl_u;
+ __gen_e_acsl_k = -7;
+ __gen_e_acsl_exists_2 = 0;
+ __gen_e_acsl_u = 9;
+ while (1) {
+ if (__gen_e_acsl_u < 21) ; else break;
+ {
+ int __gen_e_acsl_forall;
+ int __gen_e_acsl_v;
+ __gen_e_acsl_forall = 1;
+ __gen_e_acsl_v = -5 + 1;
+ while (1) {
+ if (__gen_e_acsl_v <= 6) ; else break;
+ {
+ int __gen_e_acsl_valid_read_3;
+ __gen_e_acsl_valid_read_3 = __e_acsl_valid_read((void *)(
+ __gen_e_acsl_at_3 + (int)(
+ (long)((int)(
+ (long)((int)(
+ __gen_e_acsl_u - 9L)) * 11L)) + (int)(
+ (int)(__gen_e_acsl_v - -5L) - 1))),
+ sizeof(int),
+ (void *)__gen_e_acsl_at_3,
+ (void *)(& __gen_e_acsl_at_3));
+ __e_acsl_assert(__gen_e_acsl_valid_read_3,(char *)"RTE",
+ (char *)"main",
+ (char *)"mem_access:\n \\valid_read(__gen_e_acsl_at_3 +\n (int)((int)((int)(__gen_e_acsl_u - 9) * 11) +\n (int)((int)(__gen_e_acsl_v - -5) - 1)))",
+ 34);
+ /*@ assert
+ Value: initialization:
+ \initialized(__gen_e_acsl_at_3 +
+ ((__gen_e_acsl_u - 9) * 11 +
+ ((__gen_e_acsl_v - -5) - 1)));
+ */
+ if (*(__gen_e_acsl_at_3 + ((__gen_e_acsl_u - 9) * 11 + ((
+ __gen_e_acsl_v - -5) - 1))))
+ ;
+ else {
+ __gen_e_acsl_forall = 0;
+ goto e_acsl_end_loop3;
+ }
+ }
+ __gen_e_acsl_v ++;
+ }
+ e_acsl_end_loop3: ;
+ if (! __gen_e_acsl_forall) ;
+ else {
+ __gen_e_acsl_exists_2 = 1;
+ goto e_acsl_end_loop4;
+ }
+ }
+ __gen_e_acsl_u ++;
+ }
+ e_acsl_end_loop4: ;
+ __e_acsl_assert(__gen_e_acsl_exists_2,(char *)"Assertion",(char *)"main",
+ (char *)"\\let k = -7;\n\\exists integer u;\n 9 <= u < 21 &&\n (\\forall integer v; -5 < v <= 6 ==> \\at((u > 0? n + k: u + v) > 0,K))",
+ 31);
+ }
+ /*@ assert \let i = 3; \at(n + i,L) ≡ 10; */
+ {
+ int __gen_e_acsl_i_3;
+ int __gen_e_acsl_valid_read_4;
+ __gen_e_acsl_i_3 = 3;
+ __gen_e_acsl_valid_read_4 = __e_acsl_valid_read((void *)(__gen_e_acsl_at_4 + 0),
+ sizeof(long),
+ (void *)__gen_e_acsl_at_4,
+ (void *)(& __gen_e_acsl_at_4));
+ __e_acsl_assert(__gen_e_acsl_valid_read_4,(char *)"RTE",(char *)"main",
+ (char *)"mem_access: \\valid_read(__gen_e_acsl_at_4 + 0)",
+ 37);
+ __e_acsl_assert(*(__gen_e_acsl_at_4 + 0) == 10L,(char *)"Assertion",
+ (char *)"main",
+ (char *)"\\let i = 3; \\at(n + i,L) == 10",37);
+ }
+ unsigned int m = (unsigned int)3;
+ G:
+ {
+ {
+ int __gen_e_acsl_k_4;
+ __gen_e_acsl_k_4 = -9 + 1;
+ while (1) {
+ if (__gen_e_acsl_k_4 < 0) ; else break;
+ *(__gen_e_acsl_at_5 + ((__gen_e_acsl_k_4 - -9) - 1)) = m + (long)__gen_e_acsl_k_4;
+ __gen_e_acsl_k_4 ++;
+ }
+ }
+ ;
+ }
+ m = (unsigned int)(-3);
+ /*@ assert ∃ ℤ k; -9 < k < 0 ∧ \at(m + k,G) ≡ 0; */
+ {
+ int __gen_e_acsl_exists_3;
+ int __gen_e_acsl_k_3;
+ __gen_e_acsl_exists_3 = 0;
+ __gen_e_acsl_k_3 = -9 + 1;
+ while (1) {
+ if (__gen_e_acsl_k_3 < 0) ; else break;
+ {
+ int __gen_e_acsl_valid_read_5;
+ __gen_e_acsl_valid_read_5 = __e_acsl_valid_read((void *)(__gen_e_acsl_at_5 + (
+ (int)(
+ __gen_e_acsl_k_3 - -9L) - 1)),
+ sizeof(long),
+ (void *)__gen_e_acsl_at_5,
+ (void *)(& __gen_e_acsl_at_5));
+ __e_acsl_assert(__gen_e_acsl_valid_read_5,(char *)"RTE",
+ (char *)"main",
+ (char *)"mem_access:\n \\valid_read(__gen_e_acsl_at_5 + (int)((int)(__gen_e_acsl_k_3 - -9) - 1))",
+ 41);
+ /*@ assert
+ Value: initialization:
+ \initialized(__gen_e_acsl_at_5 + ((__gen_e_acsl_k_3 - -9) - 1));
+ */
+ if (! (*(__gen_e_acsl_at_5 + ((__gen_e_acsl_k_3 - -9) - 1)) == 0L))
+ ;
+ else {
+ __gen_e_acsl_exists_3 = 1;
+ goto e_acsl_end_loop5;
+ }
+ }
+ __gen_e_acsl_k_3 ++;
+ }
+ e_acsl_end_loop5: ;
+ __e_acsl_assert(__gen_e_acsl_exists_3,(char *)"Assertion",(char *)"main",
+ (char *)"\\exists integer k; -9 < k < 0 && \\at(m + k,G) == 0",
+ 41);
+ }
+ /*@ assert
+ ∃ ℤ u;
+ 9 ≤ u < 21 ∧
+ (∀ ℤ v; -5 < v ≤ (u < 15? u + 6: 3) ⇒ \at((n + u) + v > 0,K));
+ */
+ {
+ int __gen_e_acsl_exists_4;
+ int __gen_e_acsl_u_3;
+ __gen_e_acsl_exists_4 = 0;
+ __gen_e_acsl_u_3 = 9;
+ while (1) {
+ if (__gen_e_acsl_u_3 < 21) ; else break;
+ {
+ int __gen_e_acsl_forall_2;
+ int __gen_e_acsl_v_3;
+ __gen_e_acsl_forall_2 = 1;
+ __gen_e_acsl_v_3 = -5 + 1;
+ while (1) {
+ {
+ int __gen_e_acsl_if_3;
+ if (__gen_e_acsl_u_3 < 15) __gen_e_acsl_if_3 = __gen_e_acsl_u_3 + 6;
+ else __gen_e_acsl_if_3 = 3;
+ if (__gen_e_acsl_v_3 <= __gen_e_acsl_if_3) ; else break;
+ }
+ {
+ int __gen_e_acsl_valid_read_6;
+ __gen_e_acsl_valid_read_6 = __e_acsl_valid_read((void *)(
+ __gen_e_acsl_at_6 + (int)(
+ (long)((int)(
+ (long)((int)(
+ __gen_e_acsl_u_3 - 9L)) * 32L)) + (int)(
+ (int)(__gen_e_acsl_v_3 - -5L) - 1))),
+ sizeof(int),
+ (void *)__gen_e_acsl_at_6,
+ (void *)(& __gen_e_acsl_at_6));
+ __e_acsl_assert(__gen_e_acsl_valid_read_6,(char *)"RTE",
+ (char *)"main",
+ (char *)"mem_access:\n \\valid_read(__gen_e_acsl_at_6 +\n (int)((int)((int)(__gen_e_acsl_u_3 - 9) * 32) +\n (int)((int)(__gen_e_acsl_v_3 - -5) - 1)))",
+ 45);
+ /*@ assert
+ Value: initialization:
+ \initialized(__gen_e_acsl_at_6 +
+ ((__gen_e_acsl_u_3 - 9) * 32 +
+ ((__gen_e_acsl_v_3 - -5) - 1)));
+ */
+ if (*(__gen_e_acsl_at_6 + ((__gen_e_acsl_u_3 - 9) * 32 + (
+ (__gen_e_acsl_v_3 - -5) - 1))))
+ ;
+ else {
+ __gen_e_acsl_forall_2 = 0;
+ goto e_acsl_end_loop6;
+ }
+ }
+ __gen_e_acsl_v_3 ++;
+ }
+ e_acsl_end_loop6: ;
+ if (! __gen_e_acsl_forall_2) ;
+ else {
+ __gen_e_acsl_exists_4 = 1;
+ goto e_acsl_end_loop7;
+ }
+ }
+ __gen_e_acsl_u_3 ++;
+ }
+ e_acsl_end_loop7: ;
+ __e_acsl_assert(__gen_e_acsl_exists_4,(char *)"Assertion",(char *)"main",
+ (char *)"\\exists integer u;\n 9 <= u < 21 &&\n (\\forall integer v; -5 < v <= (u < 15? u + 6: 3) ==> \\at((n + u) + v > 0,K))",
+ 43);
+ }
+ int t[5] = {9, 12, 12, 12, -4};
+ __e_acsl_store_block((void *)(t),(size_t)20);
+ __e_acsl_full_init((void *)(& t));
+ __gen_e_acsl_f(t);
+ g();
+ /*@ assert
+ ∃ ℤ u;
+ 10 ≤ u < 20 ∧
+ (∃ ℤ v;
+ -10 < v ≤ -5 + (\let u = -2; u) ∧
+ (∃ ℤ w;
+ 100 < w ≤ 200 ∧
+ \at((((n - u) + (\let u = 42; u)) + v) + w > 0,K)));
+ */
+ {
+ int __gen_e_acsl_exists_5;
+ int __gen_e_acsl_u_5;
+ __gen_e_acsl_exists_5 = 0;
+ __gen_e_acsl_u_5 = 10;
+ while (1) {
+ if (__gen_e_acsl_u_5 < 20) ; else break;
+ {
+ int __gen_e_acsl_exists_6;
+ int __gen_e_acsl_v_5;
+ __gen_e_acsl_exists_6 = 0;
+ __gen_e_acsl_v_5 = -10 + 1;
+ while (1) {
+ {
+ int __gen_e_acsl_u_9;
+ __gen_e_acsl_u_9 = -2;
+ if (__gen_e_acsl_v_5 <= -5 + __gen_e_acsl_u_9) ; else break;
+ }
+ {
+ int __gen_e_acsl_exists_7;
+ int __gen_e_acsl_w;
+ __gen_e_acsl_exists_7 = 0;
+ __gen_e_acsl_w = 100 + 1;
+ while (1) {
+ if (__gen_e_acsl_w <= 200) ; else break;
+ {
+ int __gen_e_acsl_valid_read_7;
+ __gen_e_acsl_valid_read_7 = __e_acsl_valid_read((void *)(
+ __gen_e_acsl_at_7 + (int)(
+ (long)((int)(
+ (long)((int)(
+ __gen_e_acsl_u_5 - 10L)) * 300L)) + (int)(
+ (long)((int)(
+ (long)((int)(
+ (int)(
+ __gen_e_acsl_v_5 - -10L) - 1)) * 100L)) + (int)(
+ (long)((int)(
+ __gen_e_acsl_w - 100L)) - 1L)))),
+ sizeof(int),
+ (void *)__gen_e_acsl_at_7,
+ (void *)(& __gen_e_acsl_at_7));
+ __e_acsl_assert(__gen_e_acsl_valid_read_7,(char *)"RTE",
+ (char *)"main",
+ (char *)"mem_access:\n \\valid_read(__gen_e_acsl_at_7 +\n (int)((int)((int)(__gen_e_acsl_u_5 - 10) * 300) +\n (int)((int)((int)((int)(__gen_e_acsl_v_5 - -10) - 1) *\n 100)\n + (int)((int)(__gen_e_acsl_w - 100) - 1))))",
+ 57);
+ /*@ assert
+ Value: initialization:
+ \initialized(__gen_e_acsl_at_7 +
+ ((__gen_e_acsl_u_5 - 10) * 300 +
+ (((__gen_e_acsl_v_5 - -10) - 1) * 100 +
+ ((__gen_e_acsl_w - 100) - 1))));
+ */
+ if (! *(__gen_e_acsl_at_7 + ((__gen_e_acsl_u_5 - 10) * 300 + (
+ ((__gen_e_acsl_v_5 - -10) - 1) * 100 + (
+ (__gen_e_acsl_w - 100) - 1)))))
+ ;
+ else {
+ __gen_e_acsl_exists_7 = 1;
+ goto e_acsl_end_loop8;
+ }
+ }
+ __gen_e_acsl_w ++;
+ }
+ e_acsl_end_loop8: ;
+ if (! __gen_e_acsl_exists_7) ;
+ else {
+ __gen_e_acsl_exists_6 = 1;
+ goto e_acsl_end_loop9;
+ }
+ }
+ __gen_e_acsl_v_5 ++;
+ }
+ e_acsl_end_loop9: ;
+ if (! __gen_e_acsl_exists_6) ;
+ else {
+ __gen_e_acsl_exists_5 = 1;
+ goto e_acsl_end_loop10;
+ }
+ }
+ __gen_e_acsl_u_5 ++;
+ }
+ e_acsl_end_loop10: ;
+ __e_acsl_assert(__gen_e_acsl_exists_5,(char *)"Assertion",(char *)"main",
+ (char *)"\\exists integer u;\n 10 <= u < 20 &&\n (\\exists integer v;\n -10 < v <= -5 + (\\let u = -2; u) &&\n (\\exists integer w;\n 100 < w <= 200 && \\at((((n - u) + (\\let u = 42; u)) + v) + w > 0,K)))",
+ 54);
+ }
+ /*@ assert ∃ ℤ j; 2 ≤ j < 10000000000000000 ∧ \at(n + j ≡ 11,L);
+ */
+ ;
+ /*@ assert \let i = n; \at(n + i ≡ 10,L); */ ;
+ __retres = 0;
+ __e_acsl_delete_block((void *)(t));
+ __e_acsl_delete_block((void *)(& n));
+ free((void *)__gen_e_acsl_at_7);
+ free((void *)__gen_e_acsl_at_6);
+ free((void *)__gen_e_acsl_at_5);
+ free((void *)__gen_e_acsl_at_4);
+ free((void *)__gen_e_acsl_at_3);
+ free((void *)__gen_e_acsl_at_2);
+ free((void *)__gen_e_acsl_at);
+ __e_acsl_memory_clean();
+ return __retres;
+}
+
+/*@ ensures
+ ∀ ℤ 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 __gen_e_acsl_f(int *t)
+{
+ int *__gen_e_acsl_at_4;
+ int *__gen_e_acsl_at_3;
+ int *__gen_e_acsl_at_2;
+ int *__gen_e_acsl_at;
+ __gen_e_acsl_at_4 = (int *)malloc((size_t)4);
+ __gen_e_acsl_at_3 = (int *)malloc((size_t)4);
+ __gen_e_acsl_at_2 = (int *)malloc((size_t)8);
+ __gen_e_acsl_at = (int *)malloc((size_t)8);
+ {
+ int __gen_e_acsl_m_3;
+ __gen_e_acsl_m_3 = 4;
+ *(__gen_e_acsl_at_4 + 0) = *(t + (__gen_e_acsl_m_3 - 4));
+ }
+ {
+ int __gen_e_acsl_m_2;
+ __gen_e_acsl_m_2 = 4;
+ *(__gen_e_acsl_at_3 + 0) = *(t + __gen_e_acsl_m_2) == -4;
+ }
+ {
+ int __gen_e_acsl_n_3;
+ __gen_e_acsl_n_3 = 1 + 1;
+ while (1) {
+ if (__gen_e_acsl_n_3 <= 3) ; else break;
+ *(__gen_e_acsl_at_2 + ((__gen_e_acsl_n_3 - 1) - 1)) = *(t + (__gen_e_acsl_n_3 - 1)) > 5;
+ __gen_e_acsl_n_3 ++;
+ }
+ }
+ {
+ int __gen_e_acsl_n_2;
+ __gen_e_acsl_n_2 = 1 + 1;
+ while (1) {
+ if (__gen_e_acsl_n_2 <= 3) ; else break;
+ *(__gen_e_acsl_at + ((__gen_e_acsl_n_2 - 1) - 1)) = *(t + __gen_e_acsl_n_2) == 12;
+ __gen_e_acsl_n_2 ++;
+ }
+ }
+ __e_acsl_store_block((void *)(& t),(size_t)8);
+ f(t);
+ {
+ int __gen_e_acsl_forall;
+ int __gen_e_acsl_n;
+ int __gen_e_acsl_m;
+ int __gen_e_acsl_valid_read_3;
+ int __gen_e_acsl_and_2;
+ __gen_e_acsl_forall = 1;
+ __gen_e_acsl_n = 1 + 1;
+ while (1) {
+ if (__gen_e_acsl_n <= 3) ; else break;
+ {
+ int __gen_e_acsl_valid_read;
+ int __gen_e_acsl_and;
+ __gen_e_acsl_valid_read = __e_acsl_valid_read((void *)(__gen_e_acsl_at + (int)(
+ (long)((int)(
+ __gen_e_acsl_n - 1L)) - 1L)),
+ sizeof(int),
+ (void *)__gen_e_acsl_at,
+ (void *)(& __gen_e_acsl_at));
+ __e_acsl_assert(__gen_e_acsl_valid_read,(char *)"RTE",(char *)"f",
+ (char *)"mem_access:\n \\valid_read(__gen_e_acsl_at + (int)((int)(__gen_e_acsl_n - 1) - 1))",
+ 7);
+ /*@ assert
+ Value: initialization:
+ \initialized(__gen_e_acsl_at + ((__gen_e_acsl_n - 1) - 1));
+ */
+ if (*(__gen_e_acsl_at + ((__gen_e_acsl_n - 1) - 1))) {
+ int __gen_e_acsl_valid_read_2;
+ __gen_e_acsl_valid_read_2 = __e_acsl_valid_read((void *)(__gen_e_acsl_at_2 + (int)(
+ (long)((int)(
+ __gen_e_acsl_n - 1L)) - 1L)),
+ sizeof(int),
+ (void *)__gen_e_acsl_at_2,
+ (void *)(& __gen_e_acsl_at_2));
+ __e_acsl_assert(__gen_e_acsl_valid_read_2,(char *)"RTE",
+ (char *)"f",
+ (char *)"mem_access:\n \\valid_read(__gen_e_acsl_at_2 + (int)((int)(__gen_e_acsl_n - 1) - 1))",
+ 7);
+ /*@ assert
+ Value: initialization:
+ \initialized(__gen_e_acsl_at_2 + ((__gen_e_acsl_n - 1) - 1));
+ */
+ __gen_e_acsl_and = *(__gen_e_acsl_at_2 + ((__gen_e_acsl_n - 1) - 1));
+ }
+ else __gen_e_acsl_and = 0;
+ if (__gen_e_acsl_and) ;
+ else {
+ __gen_e_acsl_forall = 0;
+ goto e_acsl_end_loop11;
+ }
+ }
+ __gen_e_acsl_n ++;
+ }
+ e_acsl_end_loop11: ;
+ __e_acsl_assert(__gen_e_acsl_forall,(char *)"Postcondition",(char *)"f",
+ (char *)"\\forall integer n;\n 1 < n <= 3 ==> \\old(*(t + n) == 12) && \\old(*(t + (n - 1)) > 5)",
+ 6);
+ __gen_e_acsl_m = 4;
+ __gen_e_acsl_valid_read_3 = __e_acsl_valid_read((void *)(__gen_e_acsl_at_3 + 0),
+ sizeof(int),
+ (void *)__gen_e_acsl_at_3,
+ (void *)(& __gen_e_acsl_at_3));
+ __e_acsl_assert(__gen_e_acsl_valid_read_3,(char *)"RTE",(char *)"f",
+ (char *)"mem_access: \\valid_read(__gen_e_acsl_at_3 + 0)",
+ 8);
+ if (*(__gen_e_acsl_at_3 + 0)) {
+ int __gen_e_acsl_valid_read_4;
+ __gen_e_acsl_valid_read_4 = __e_acsl_valid_read((void *)(__gen_e_acsl_at_4 + 0),
+ sizeof(int),
+ (void *)__gen_e_acsl_at_4,
+ (void *)(& __gen_e_acsl_at_4));
+ __e_acsl_assert(__gen_e_acsl_valid_read_4,(char *)"RTE",(char *)"f",
+ (char *)"mem_access: \\valid_read(__gen_e_acsl_at_4 + 0)",
+ 8);
+ __gen_e_acsl_and_2 = *(__gen_e_acsl_at_4 + 0) == 9;
+ }
+ else __gen_e_acsl_and_2 = 0;
+ __e_acsl_assert(__gen_e_acsl_and_2,(char *)"Postcondition",(char *)"f",
+ (char *)"\\let m = 4; \\old(*(t + m) == -4) && \\old(*(t + (m - 4))) == 9",
+ 8);
+ __e_acsl_delete_block((void *)(& t));
+ free((void *)__gen_e_acsl_at_4);
+ free((void *)__gen_e_acsl_at_3);
+ free((void *)__gen_e_acsl_at_2);
+ free((void *)__gen_e_acsl_at);
+ return;
+ }
+}
+
+
diff --git a/src/plugins/e-acsl/tests/gmp/oracle/gen_at_on-purely-logic-variables2.c b/src/plugins/e-acsl/tests/gmp/oracle/gen_at_on-purely-logic-variables2.c
new file mode 100644
index 0000000000000000000000000000000000000000..2c6d212d7a8b887c51dd0afd90d6b03a8fe215c7
--- /dev/null
+++ b/src/plugins/e-acsl/tests/gmp/oracle/gen_at_on-purely-logic-variables2.c
@@ -0,0 +1,103 @@
+/* Generated by Frama-C */
+#include "stdio.h"
+#include "stdlib.h"
+/*@ ensures
+ ∀ ℤ 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 __gen_e_acsl_f(int *t);
+
+void f(int *t)
+{
+ __e_acsl_store_block((void *)(& t),(size_t)8);
+ __e_acsl_delete_block((void *)(& t));
+ return;
+}
+
+void g(void)
+{
+ int m;
+ m = 8;
+ Q: ;
+ m = 10;
+ /*@ assert ∃ ℤ w; 3 ≤ w < 6 ∧ \at(m + w ≡ 12,Q); */ ;
+ return;
+}
+
+int main(void)
+{
+ int __retres;
+ int n;
+ __e_acsl_memory_init((int *)0,(char ***)0,(size_t)8);
+ __e_acsl_store_block((void *)(& n),(size_t)4);
+ __e_acsl_full_init((void *)(& n));
+ n = 7;
+ L: ;
+ __e_acsl_full_init((void *)(& n));
+ n = 9;
+ K: ;
+ __e_acsl_full_init((void *)(& n));
+ n = 666;
+ /*@ assert \let i = 3; \at(n + i ≡ 10,L); */ ;
+ /*@ assert ∃ ℤ j; 2 ≤ j < 5 ∧ \at(n + j ≡ 11,L); */ ;
+ /*@
+ assert \let k = -7;
+ ∃ ℤ u;
+ 9 ≤ u < 21 ∧
+ (∀ ℤ v; -5 < v ≤ 6 ⇒ \at((u > 0? n + k: u + v) > 0,K));
+ */
+ ;
+ /*@ assert \let i = 3; \at(n + i,L) ≡ 10; */ ;
+ unsigned int m = (unsigned int)3;
+ G: ;
+ m = (unsigned int)(-3);
+ /*@ assert ∃ ℤ k; -9 < k < 0 ∧ \at(m + k,G) ≡ 0; */ ;
+ /*@
+ assert
+ ∃ ℤ u;
+ 9 ≤ u < 21 ∧
+ (∀ ℤ v; -5 < v ≤ (u < 15? u + 6: 3) ⇒ \at((n + u) + v > 0,K));
+ */
+ ;
+ int t[5] = {9, 12, 12, 12, -4};
+ __e_acsl_store_block((void *)(t),(size_t)20);
+ __e_acsl_full_init((void *)(& t));
+ __gen_e_acsl_f(t);
+ g();
+ /*@
+ assert
+ ∃ ℤ u;
+ 10 ≤ u < 20 ∧
+ (∃ ℤ v;
+ -10 < v ≤ -5 + (\let u = -2; u) ∧
+ (∃ ℤ w;
+ 100 < w ≤ 200 ∧
+ \at((((n - u) + (\let u = 42; u)) + v) + w > 0,K)));
+ */
+ ;
+ /*@ assert ∃ ℤ j; 2 ≤ j < 10000000000000000 ∧ \at(n + j ≡ 11,L);
+ */
+ ;
+ /*@ assert \let i = n; \at(n + i ≡ 10,L); */ ;
+ __retres = 0;
+ __e_acsl_delete_block((void *)(t));
+ __e_acsl_delete_block((void *)(& n));
+ __e_acsl_memory_clean();
+ return __retres;
+}
+
+/*@ ensures
+ ∀ ℤ 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 __gen_e_acsl_f(int *t)
+{
+ __e_acsl_store_block((void *)(& t),(size_t)8);
+ f(t);
+ __e_acsl_delete_block((void *)(& t));
+ return;
+}
+
+
diff --git a/src/plugins/e-acsl/tests/gmp/test_config b/src/plugins/e-acsl/tests/gmp/test_config
index b51a18dcf2f95a90239b1a25a517a65a5e866834..645d2c1fa60b62e4c9c9223a7c2f6adf06608878 100644
--- a/src/plugins/e-acsl/tests/gmp/test_config
+++ b/src/plugins/e-acsl/tests/gmp/test_config
@@ -1,5 +1,5 @@
LOG: gen_@PTEST_NAME@.c
-OPT: -machdep gcc_x86_64 -check -e-acsl -then-last -load-script tests/print.cmxs -print -ocode tests/gmp/result/gen_@PTEST_NAME@.c -kernel-verbose 0 -val -no-val-print -no-val-show-progress -no-results
+OPT: -machdep gcc_x86_64 -check -e-acsl -then-last -load-script tests/print.cmxs -print -ocode tests/gmp/result/gen_@PTEST_NAME@.c -kernel-verbose 0 -val -no-val-print -no-val-show-progress -no-results -eva-no-alloc-returns-null
EXEC: ./scripts/testrun.sh @PTEST_NAME@ gmp "1" "--frama-c=@frama-c@"
LOG: gen_@PTEST_NAME@2.c
-OPT: -machdep gcc_x86_64 -check -e-acsl -e-acsl-gmp-only -then-last -load-script tests/print.cmxs -print -ocode tests/gmp/result/gen_@PTEST_NAME@2.c -kernel-verbose 0 -val -no-val-print -no-val-show-progress -no-results
+OPT: -machdep gcc_x86_64 -check -e-acsl -e-acsl-gmp-only -then-last -load-script tests/print.cmxs -print -ocode tests/gmp/result/gen_@PTEST_NAME@2.c -kernel-verbose 0 -val -no-val-print -no-val-show-progress -no-results -eva-no-alloc-returns-null
diff --git a/src/plugins/e-acsl/translate.ml b/src/plugins/e-acsl/translate.ml
index 4510c8f3fdf32192a964c9ac49eec82aaf5b5c95..8afed8ab60fd26c4412c5a6d3b2fa3d27ac2deee 100644
--- a/src/plugins/e-acsl/translate.ml
+++ b/src/plugins/e-acsl/translate.ml
@@ -296,7 +296,7 @@ let cast_integer_to_float lty lty_t e =
else
e
-let rec thost_to_host kf env = function
+let rec thost_to_host kf env th = match th with
| TVar { lv_origin = Some v } ->
Var (Cil.get_varinfo (Env.get_behavior env) v), env, v.vname
| TVar ({ lv_origin = None } as logic_v) ->
@@ -424,7 +424,8 @@ and context_insensitive_term_to_exp kf env t =
(* do not generate [e2] from [t2] twice *)
let guard, env =
let name = name_of_binop bop ^ "_guard" in
- comparison_to_exp ~loc kf env Typing.gmp ~e1:e2 ~name Eq t2 zero t
+ comparison_to_exp
+ ~loc kf env Typing.gmp ~e1:e2 ~name Eq t2 zero t
in
let mk_stmts _v e =
assert (Gmpz.is_t ty);
@@ -549,10 +550,15 @@ 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) ->
- (* convert [t'] to [e] in a separated local env *)
- let e, env = term_to_exp kf (Env.push env) t' in
- let e, env, is_mpz_string = at_to_exp env (Some t) label e in
- e, env, is_mpz_string, ""
+ let lscope = Env.Logic_scope.get env in
+ let pot = Misc.PoT_term t' in
+ if Lscope.is_used lscope pot then
+ let e, env = At_with_lscope.to_exp ~loc kf env pot label in
+ e, env, false, ""
+ else
+ let e, env = term_to_exp kf (Env.push env) t' in
+ let e, env, is_mpz_string = at_to_exp_no_lscope env (Some t) label e in
+ e, env, is_mpz_string, ""
| Tbase_addr(BuiltinLabel Here, t) ->
mmodel_call ~loc kf "base_addr" Cil.voidPtrType env t
| Tbase_addr _ -> not_yet env "labeled \\base_addr"
@@ -576,6 +582,8 @@ and context_insensitive_term_to_exp kf env t =
| Tcomprehension _ -> not_yet env "tset comprehension"
| 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.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;
@@ -590,7 +598,9 @@ and term_to_exp kf env t =
Printer.pp_term t generate_rte;
let env = Env.rte env false in
let t = match t.term_node with TLogic_coerce(_, t) -> t | _ -> t in
- let e, env, is_mpz_string, name = context_insensitive_term_to_exp kf env t in
+ let e, env, is_mpz_string, name =
+ context_insensitive_term_to_exp kf env t
+ in
let env = if generate_rte then translate_rte kf env e else env in
let cast = Typing.get_cast t in
let name = if name = "" then None else Some name in
@@ -675,7 +685,13 @@ and mmodel_call_with_size ~loc kf name ctx env t =
res, env
in
mmodel_call_with_ranges
- ~loc kf name ctx env t call_for_unsupported_constructs
+ ~loc
+ kf
+ name
+ ctx
+ env
+ t
+ call_for_unsupported_constructs
and mmodel_call_valid ~loc kf name ctx env t =
let call_for_unsupported_constructs ~loc kf name ctx env t =
@@ -703,7 +719,13 @@ and mmodel_call_valid ~loc kf name ctx env t =
res, env
in
mmodel_call_with_ranges
- ~loc kf name ctx env t call_for_unsupported_constructs
+ ~loc
+ kf
+ name
+ ctx
+ env
+ t
+ call_for_unsupported_constructs
(* [mmodel_call_with_ranges] handles ranges in [t] when calling builtin [name].
It only supports the following cases for the time being:
@@ -859,7 +881,7 @@ and mmodel_call_memory_block ~loc kf name ctx env p r =
in
e, env
-and at_to_exp env t_opt label e =
+and at_to_exp_no_lscope env t_opt label e =
let stmt = E_acsl_label.get_stmt (Env.get_visitor env) label in
(* generate a new variable denoting [\at(t',label)].
That is this variable which is the resulting expression.
@@ -884,20 +906,15 @@ and at_to_exp env t_opt label e =
inherit Visitor.frama_c_inplace
method !vstmt_aux stmt =
(* either a standard C affectation or an mpz one according to type of
- [e] *)
+ [e] *)
let new_stmt = Gmpz.init_set ~loc (Cil.var res_v) res e in
assert (!env_ref == new_env);
(* generate the new block of code for the labeled statement and the
- corresponding environment *)
+ corresponding environment *)
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
+ Env.pop_and_get new_env new_stmt ~global_clear:false Env.Middle
in
- env_ref := Env.extend_stmt_in_place new_env stmt ~pre block;
+ env_ref := Env.extend_stmt_in_place new_env stmt ~label block;
Cil.ChangeTo stmt
end
in
@@ -936,7 +953,8 @@ and named_predicate_content_to_exp ?name kf env p =
| Pand(p1, p2) ->
(* p1 && p2 <==> if p1 then p2 else false *)
let e1, env1 = named_predicate_to_exp kf (Env.rte env true) p1 in
- let _, env2 as res2 = named_predicate_to_exp kf (Env.push env1) p2 in
+ let _, env2 as res2 =
+ named_predicate_to_exp kf (Env.push env1) p2 in
let env3 = Env.push env2 in
let name = match name with None -> "and" | Some n -> n in
conditional_to_exp ~name loc None e1 res2 (Cil.zero loc, env3)
@@ -969,10 +987,13 @@ and named_predicate_content_to_exp ?name kf env p =
Cil.new_exp ~loc (UnOp(LNot, e, Cil.intType)), env
| Pif(t, p2, p3) ->
let e1, env1 = term_to_exp kf (Env.rte env true) t in
- let (_, env2 as res2) = named_predicate_to_exp kf (Env.push env1) p2 in
+ let (_, env2 as res2) =
+ named_predicate_to_exp kf (Env.push env1) p2 in
let res3 = named_predicate_to_exp kf (Env.push env2) p3 in
conditional_to_exp loc None e1 res2 res3
| Plet(li, p) ->
+ let lvs = Lscope.Lvs_let(li.l_var_info, Misc.term_of_li li) in
+ let env = Env.Logic_scope.extend env lvs in
let env = env_of_li li kf env loc in
let e, env = named_predicate_to_exp kf env p in
Interval.Env.remove li.l_var_info;
@@ -981,11 +1002,17 @@ and named_predicate_content_to_exp ?name kf env p =
| Pat(p, BuiltinLabel Here) ->
named_predicate_to_exp kf env p
| Pat(p', label) ->
- (* convert [t'] to [e] in a separated local env *)
- let e, env = named_predicate_to_exp kf (Env.push env) p' in
- let e, env, is_string = at_to_exp env None label e in
- assert (not is_string);
- e, env
+ let lscope = Env.Logic_scope.get env in
+ let pot = Misc.PoT_pred p' in
+ if Lscope.is_used lscope pot then
+ At_with_lscope.to_exp ~loc kf env pot label
+ else begin
+ (* convert [t'] to [e] in a separated local env *)
+ let e, env = named_predicate_to_exp kf (Env.push env) p' in
+ let e, env, is_string = at_to_exp_no_lscope env None label e in
+ assert (not is_string);
+ e, env
+ end
| Pvalid_read(BuiltinLabel Here as llabel, t) as pc
| (Pvalid(BuiltinLabel Here as llabel, t) as pc) ->
let call_valid t =
@@ -1022,7 +1049,8 @@ and named_predicate_content_to_exp ?name kf env p =
| TAddrOf (TVar { lv_origin = Some vi }, TNoOffset)
when vi.vformal || vi.vglob || Functions.RTL.is_generated_name vi.vname ->
Cil.one ~loc, env
- | _ -> mmodel_call_with_size ~loc kf "initialized" Cil.intType env t)
+ | _ ->
+ mmodel_call_with_size ~loc kf "initialized" Cil.intType env t)
| Pinitialized _ -> not_yet env "labeled \\initialized"
| Pallocable _ -> not_yet env "\\allocate"
| Pfreeable(BuiltinLabel Here, t) ->
@@ -1061,7 +1089,13 @@ and translate_rte_annots:
handle_error
(fun env ->
Options.feedback ~dkey ~level:4 "prevent RTE from %a" pp elt;
- translate_named_predicate kf (Env.rte env false) p)
+ (* The logic scope MUST NOT be reset here since we still might be
+ in the middle of the translation of the original predicate. *)
+ let lscope_reset_old = Env.Logic_scope.get_reset env in
+ let env = Env.Logic_scope.set_reset env false in
+ let env = translate_named_predicate kf (Env.rte env false) p in
+ let env = Env.Logic_scope.set_reset env lscope_reset_old in
+ env)
env
| _ -> assert false)
env
@@ -1082,6 +1116,7 @@ and translate_named_predicate kf env p =
Typing.type_named_predicate ~must_clear:rte p;
let e, env = named_predicate_to_exp kf ~rte env p in
assert (Typ.equal (Cil.typeOf e) Cil.intType);
+ let env = Env.Logic_scope.reset env in
Env.add_stmt
env
(Misc.mk_e_acsl_guard ~reverse:true (Env.annotation_kind env) kf e p)
@@ -1090,8 +1125,11 @@ let named_predicate_to_exp ?name kf env p =
named_predicate_to_exp ?name kf env p (* forget optional argument ?rte *)
let () =
- Quantif.term_to_exp_ref := term_to_exp;
- Quantif.predicate_to_exp_ref := named_predicate_to_exp
+ Loops.term_to_exp_ref := term_to_exp;
+ Loops.translate_named_predicate_ref := translate_named_predicate;
+ Quantif.predicate_to_exp_ref := named_predicate_to_exp;
+ At_with_lscope.term_to_exp_ref := term_to_exp;
+ At_with_lscope.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/translate.mli b/src/plugins/e-acsl/translate.mli
index 77207f008721471b78209def6378a9df79deb60e..4f8540341fa2d6340d09325272825dbe46866080 100644
--- a/src/plugins/e-acsl/translate.mli
+++ b/src/plugins/e-acsl/translate.mli
@@ -32,14 +32,14 @@ val translate_pre_code_annotation:
kernel_function -> Env.t -> code_annotation -> Env.t
val translate_post_code_annotation:
kernel_function -> Env.t -> code_annotation -> Env.t
-val translate_named_predicate:
+val translate_named_predicate:
kernel_function -> Env.t -> predicate -> Env.t
val translate_rte_annots:
- (Format.formatter -> 'a -> unit) ->
+ (Format.formatter -> 'a -> unit) ->
'a ->
- kernel_function ->
- Env.t ->
+ kernel_function ->
+ Env.t ->
code_annotation list ->
Env.t
diff --git a/src/plugins/e-acsl/typing.mli b/src/plugins/e-acsl/typing.mli
index 2319e9c37671cae5d175c52d98a31045472de96a..e8a74d55ae836bdb349a116b739b0607c80e43b2 100644
--- a/src/plugins/e-acsl/typing.mli
+++ b/src/plugins/e-acsl/typing.mli
@@ -132,6 +132,15 @@ 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 *)
+(*****************************************************************************)
+
+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. *)
+
(******************************************************************************)
(** {2 Internal stuff} *)
(******************************************************************************)
diff --git a/src/plugins/e-acsl/visit.ml b/src/plugins/e-acsl/visit.ml
index 68fed7786520b3528633e2e3122779d6316e5e93..91933f67a107917c3db8381f5b77ad4c65eedad2 100644
--- a/src/plugins/e-acsl/visit.ml
+++ b/src/plugins/e-acsl/visit.ml
@@ -456,6 +456,17 @@ you must call function `%s' and `__e_acsl_memory_clean by yourself.@]"
f.slocals <- locals;
f.sbody.blocals <- blocks
+ (* Memory management for \at on purely logic variables:
+ Put [malloc] stmts at proper locations *)
+ method private insert_malloc_and_free_stmts kf f =
+ let malloc_stmts = At_with_lscope.Malloc.find_all kf in
+ let fstmts = malloc_stmts @ f.sbody.bstmts in
+ f.sbody.bstmts <- fstmts;
+ (* Now that [malloc] stmts for [kf] have been inserted,
+ there is no more need to keep the corresponding entries in the
+ table managing them. *)
+ At_with_lscope.Malloc.remove_all kf
+
method !vfunc f =
if generate then begin
Exit_points.generate f;
@@ -467,6 +478,7 @@ you must call function `%s' and `__e_acsl_memory_clean by yourself.@]"
(fun f ->
Exit_points.clear ();
self#add_generated_variables_in_function f;
+ self#insert_malloc_and_free_stmts kf f;
Options.feedback ~dkey ~level:2 "function %a done."
Kernel_function.pretty kf;
f)
@@ -834,10 +846,12 @@ you must call function `%s' and `__e_acsl_memory_clean by yourself.@]"
method !vblock blk =
let handle_memory new_blk =
- match new_blk.blocals with
- | [] -> new_blk
- | _ :: _ ->
- let kf = Extlib.the self#current_kf in
+ let kf = Extlib.the self#current_kf in
+ let free_stmts = At_with_lscope.Free.find_all kf in
+ match new_blk.blocals, free_stmts with
+ | [], [] ->
+ new_blk
+ | [], _ :: _ | _ :: _, [] | _ :: _, _ :: _ ->
let add_locals stmts =
List.fold_left
(fun acc vi ->
@@ -854,10 +868,14 @@ you must call function `%s' and `__e_acsl_memory_clean by yourself.@]"
preceded by clean if any *)
let init, tl =
if self#is_main kf && Mmodel_analysis.use_model () then
- [ potential_clean; ret ], tl
+ free_stmts @ [ potential_clean; ret ], tl
else
- [ ret ], l
+ free_stmts @ [ ret ], l
in
+ (* Now that [free] stmts for [kf] have been inserted,
+ there is no more need to keep the corresponding entries in the
+ table managing them. *)
+ At_with_lscope.Free.remove_all kf;
blk.bstmts <-
List.fold_left (fun acc v -> v :: acc) (add_locals init) tl
| { skind = Block b } :: _ ->