From a8665b8a6958af290160d2140665484f3ce197d0 Mon Sep 17 00:00:00 2001
From: Fonenantsoa Maurica <maurica.fonenantsoa@gmail.com>
Date: Mon, 1 Oct 2018 13:52:36 +0200
Subject: [PATCH] Refactor At.mk_storing_loops with Quantif.mk_for_loops.
---
src/plugins/e-acsl/Makefile.in | 2 +-
src/plugins/e-acsl/at_with_lscope.ml | 234 ++++------
src/plugins/e-acsl/env.ml | 51 ++-
src/plugins/e-acsl/env.mli | 6 +-
src/plugins/e-acsl/loops.ml | 191 +++++++-
src/plugins/e-acsl/loops.mli | 30 +-
src/plugins/e-acsl/lscope.ml | 4 +-
src/plugins/e-acsl/lscope.mli | 3 +-
src/plugins/e-acsl/quantif.ml | 235 +++-------
src/plugins/e-acsl/quantif.mli | 5 +-
.../tests/gmp/at_on-purely-logic-variables.c | 9 +
.../at_on-purely-logic-variables.0.res.oracle | 71 ++-
.../at_on-purely-logic-variables.1.res.oracle | 13 +-
.../oracle/gen_at_on-purely-logic-variables.c | 417 ++++++++++++------
.../gen_at_on-purely-logic-variables2.c | 11 +
src/plugins/e-acsl/translate.ml | 3 +-
src/plugins/e-acsl/translate.mli | 8 +-
17 files changed, 752 insertions(+), 541 deletions(-)
diff --git a/src/plugins/e-acsl/Makefile.in b/src/plugins/e-acsl/Makefile.in
index adfb3eccf89..13768e6bfbc 100644
--- a/src/plugins/e-acsl/Makefile.in
+++ b/src/plugins/e-acsl/Makefile.in
@@ -75,12 +75,12 @@ PLUGIN_CMO:= local_config \
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
index 7611d53eb17..6f01e99b709 100644
--- a/src/plugins/e-acsl/at_with_lscope.ml
+++ b/src/plugins/e-acsl/at_with_lscope.ml
@@ -66,20 +66,33 @@ end
(* Builds the terms [t_size] and [t_shifted] from each
[Lvs_quantif(tmin, lv, tmax)] from [lscope]
- where [t_size = tmax - tmin + 1] (+1 because the inequalities are large
- due to previous normalization)
- and [t_shifted = lv - tmin] (so that we start indexing at 0) *)
+ 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) ::_
+ | 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, lv, tmax) :: lscope' ->
+ | 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 =
- Logic_const.term ~loc (TBinOp(PlusA, t_size, Cil.lone ~loc ())) Linteger
+ 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
@@ -100,17 +113,23 @@ let rec sizes_and_shifts_from_quantifs ~loc kf lscope sizes_and_shifts =
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)"
+ | _, 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 =
- Logic_const.term ~loc (TBinOp(MinusA, t_lv, tmin)) Linteger
+ 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
@@ -138,13 +157,6 @@ let size_from_sizes_and_shifts ~loc = function
size
sizes_and_shifts
-let append_block_of_env_to_block env block =
- let block_stmt = Cil.mkStmt ~valid_sid:true (Block block) in
- let block, env =
- Env.pop_and_get env block_stmt ~global_clear:false Env.After
- in
- block, env
-
(* 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;
@@ -157,129 +169,6 @@ let lval_at_index ~loc kf env (e_at, vi_at, t_index) =
let lval_at_index = Mem e_addr, NoOffset in
lval_at_index, env
-(* [mk_storing_loops] creates the nested loops that are used to store the
- different possible values of [pot].
- These loops are similar to those generated by [Quantif], with the difference
- that the aim of the innermost block is to store values,
- not to check the validity of some (quantified) predicate. *)
-let rec mk_storing_loops ~loc kf env lscope (e_at, vi_at, t_index) pot =
- let term_to_exp = !term_to_exp_ref in
- let named_predicate_to_exp = !predicate_to_exp_ref in
- match lscope, 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 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
- 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 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
- block, env
- | Typing.Gmp ->
- Error.not_yet "\\at on purely logic variables and over gmp type"
- end
- | Lscope.Lvs_quantif(tmin, lv, tmax) :: lscope', pot ->
- (* TODO: a refactor with [Quantif] may be possible for this case *)
- let vi_of_lv_old = Env.Logic_binding.get env lv in
- let env = Env.push env in
- let vi_of_lv, _, env =
- (* We need to redeclare the lv thus new varinfo needed *)
- Env.Logic_binding.add ~ty:vi_of_lv_old.vtype env lv
- in
- let t_lv = Logic_const.tvar ~loc lv in
- (* Guard *)
- let guard =
- Logic_const.term ~loc (TBinOp(Le, t_lv, tmax)) (Ctype Cil.intType)
- in
- Typing.type_term ~use_gmp_opt:false ~ctx:Typing.c_int guard;
- let guard_exp, env = term_to_exp kf env guard in
- (* Break *)
- let break_stmt = Cil.mkStmt ~valid_sid:true (Break guard_exp.eloc) in
- (* Inner loop *)
- let loop', env =
- mk_storing_loops ~loc kf env lscope' (e_at, vi_at, t_index) pot
- in
- let loop' = Cil.mkStmt ~valid_sid:true (Block loop') in
- (* Loop counter *)
- let plus_one_term = Logic_const.term
- ~loc
- (TBinOp(PlusA, t_lv, Cil.lone ~loc ()))
- Linteger
- in
- Typing.type_term ~use_gmp_opt:true plus_one_term;
- let plus_one_exp, env = term_to_exp kf env plus_one_term in
- let plus_one_stmt = match Typing.get_integer_ty plus_one_term with
- | Typing.C_type _ | Typing.Gmp ->
- Gmpz.init_set ~loc (Cil.var vi_of_lv) (Cil.evar vi_of_lv) plus_one_exp
- | Typing.Other ->
- assert false
- in
- (* If guard is satisfiable then inner loop, else break *)
- let if_stmt = Cil.mkStmt
- ~valid_sid:true
- (If(guard_exp,
- Cil.mkBlock [ loop'; plus_one_stmt ],
- Cil.mkBlock [ break_stmt ],
- guard_exp.eloc))
- in
- let loop = Cil.mkStmt
- ~valid_sid:true
- (Loop ([],
- Cil.mkBlock [ if_stmt ],
- loc,
- None,
- Some break_stmt))
- in
- (* Init lv *)
- let tmin_exp, env = term_to_exp kf env tmin in
- let set_tmin = match Typing.get_integer_ty plus_one_term with
- | Typing.C_type _ | Typing.Gmp ->
- Gmpz.init_set ~loc (Cil.var vi_of_lv) (Cil.evar vi_of_lv) tmin_exp
- | Typing.Other ->
- assert false
- in
- (* The whole block *)
- let block = Cil.mkBlock [set_tmin; loop] in
- let b, env = append_block_of_env_to_block env block in
- let env = Env.Logic_binding.set env lv vi_of_lv_old in
- b, env
- | Lscope.Lvs_let(lv, t) :: lscope', pot ->
- let vi_of_lv_old = Env.Logic_binding.get env lv in
- let env = Env.push env in
- let vi_of_lv, exp_of_lv, env =
- (* We need to redeclare the lv thus new varinfo needed *)
- Env.Logic_binding.add ~ty:vi_of_lv_old.vtype env lv
- in
- let e, env = term_to_exp kf env t in
- let let_stmt = Gmpz.init_set ~loc (Cil.var vi_of_lv) exp_of_lv e in
- let block, env =
- mk_storing_loops ~loc kf env lscope' (e_at, vi_at, t_index) pot
- in
- (* The whole block *)
- block.bstmts <- let_stmt :: block.bstmts;
- let b, env = append_block_of_env_to_block env block in
- let env = Env.Logic_binding.set env lv vi_of_lv_old in
- b, env
- | 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"
-
(* 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
@@ -390,15 +279,60 @@ let to_exp ~loc kf env pot label =
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 storing_loops, env =
- mk_storing_loops ~loc kf env lscope_vars (e_at, vi_at, t_index) pot
- (* [t_index] MUST NOT be translated here because the logic bindings
- will differ once inside [mk_storing_loops] *)
+ 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 label in
+ 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
diff --git a/src/plugins/e-acsl/env.ml b/src/plugins/e-acsl/env.ml
index 4c1114d2261..af52b7caf17 100644
--- a/src/plugins/e-acsl/env.ml
+++ b/src/plugins/e-acsl/env.ml
@@ -61,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 list) 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 *) }
@@ -286,32 +287,50 @@ 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 bindings =
+ try v :: (Logic_var.Map.find logic_v env.var_mapping)
+ with Not_found -> [ v ]
in
v,
- e,
- { env with var_mapping = Logic_var.Map.add logic_v v env.var_mapping }
+ e,
+ { env with var_mapping =
+ Logic_var.Map.add logic_v bindings env.var_mapping }
- let get env logic_v =
- try Logic_var.Map.find logic_v env.var_mapping
+ let get env logic_v =
+ try
+ match Logic_var.Map.find logic_v env.var_mapping with
+ | [] -> assert false
+ | vi :: _ -> vi
with Not_found -> assert false
- let set env lv vi =
- { env with var_mapping = Logic_var.Map.add lv vi env.var_mapping }
-
- let remove env v =
+ let 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 bindings =
+ try Logic_var.Map.find v env.var_mapping
+ with Not_found -> assert false
+ in
+ match bindings with
+ | [] ->
+ assert false
+ | [ _ ] ->
+ { env with var_mapping = Logic_var.Map.remove v map }
+ | _ :: bindings ->
+ { env with var_mapping = Logic_var.Map.add v bindings env.var_mapping }
end
diff --git a/src/plugins/e-acsl/env.mli b/src/plugins/e-acsl/env.mli
index aa9aeda495a..b56fe807cd8 100644
--- a/src/plugins/e-acsl/env.mli
+++ b/src/plugins/e-acsl/env.mli
@@ -66,9 +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
- val set: t -> logic_var -> varinfo -> t
+ (* Return the latest C binding. *)
+
val remove: t -> logic_var -> t
+ (* Remove the latest C binding. *)
end
val add_assert: t -> stmt -> predicate -> unit
diff --git a/src/plugins/e-acsl/loops.ml b/src/plugins/e-acsl/loops.ml
index 3997c2c9ef3..9f982de071a 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 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
+ (* 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 = stmts_block init_blk in
+ let next = stmts_block 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 ba56d942004..ba113cea4db 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 the 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
index 805032015e9..a14a42fa1c9 100644
--- a/src/plugins/e-acsl/lscope.ml
+++ b/src/plugins/e-acsl/lscope.ml
@@ -24,7 +24,7 @@ open Cil_types
type lscope_var =
| Lvs_let of logic_var * term
- | Lvs_quantif of term * 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
@@ -41,7 +41,7 @@ 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_let(lv', _) | Lvs_quantif(_, _, lv', _, _) | Lvs_formal(lv', _)
| Lvs_global(lv', _) ->
Cil_datatype.Logic_var.equal lv lv'
in
diff --git a/src/plugins/e-acsl/lscope.mli b/src/plugins/e-acsl/lscope.mli
index 90f84997432..dbc8a2560f3 100644
--- a/src/plugins/e-acsl/lscope.mli
+++ b/src/plugins/e-acsl/lscope.mli
@@ -28,7 +28,8 @@ open Cil_types
type lscope_var =
| Lvs_let of logic_var * term (* the expression to which the lv is binded *)
- | Lvs_quantif of term (* min *) * logic_var * term (* max *)
+ | Lvs_quantif of term * relation * logic_var * relation * term
+ (* Take good note *)
| Lvs_formal of logic_var * logic_info (* the logic definition *)
| Lvs_global of logic_var * term (* same as Lvs_let *)
diff --git a/src/plugins/e-acsl/quantif.ml b/src/plugins/e-acsl/quantif.ml
index 223c6b7da99..c0910b7eda7 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,49 +103,31 @@ 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
- (* Update logic scope *)
- let env = List.fold_left
- (fun env (t1, rel1, lv, rel2, t2) ->
- (* The following normalization is done here:
- all the inequalities are large *)
- let tone = Cil.lone ~loc () in
- let t1 = match rel1 with
- | Rle -> t1
- | Rlt -> Logic_const.term
- ~loc
- (TBinOp(PlusA, t1, tone))
- Linteger
- | Rgt | Rge | Req | Rneq -> assert false
- in
- let t2 = match rel2 with
- | Rle -> t2
- | Rlt -> Logic_const.term
- ~loc
- (TBinOp(MinusA, t2, tone))
- Linteger
- | Rgt | Rge | Req | Rneq -> assert false
- in
- let lvs = Lscope.Lvs_quantif(t1, lv, t2) in
- Env.Logic_scope.extend env lvs)
- env
+ (* transform [guards] into [lscope_var list],
+ and update logic scope in the process *)
+ let env_ref = ref env in
+ let lvs_guards = List.map
+ (fun (t1, rel1, lv, rel2, t2) ->
+ let lvs = Lscope.Lvs_quantif(t1, rel1, lv, rel2, t2) in
+ env_ref := Env.Logic_scope.extend !env_ref lvs;
+ lvs)
guards
in
+ let env = !env_ref in
let var_res, res, env =
(* variable storing the result of the quantifier *)
let name = if is_forall then "forall" else "exists" in
@@ -160,149 +138,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 = 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_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
@@ -311,16 +179,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 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 6ace647e813..d8e8b9819c9 100644
--- a/src/plugins/e-acsl/quantif.mli
+++ b/src/plugins/e-acsl/quantif.mli
@@ -32,12 +32,9 @@ val quantif_to_exp:
(** {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
index bd8d99e51fc..ef6ee47e377 100644
--- 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
@@ -49,6 +49,15 @@ int main(void) {
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
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
index f84b17a3b0c..c0ae2df3d3e 100644
--- 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
@@ -1,10 +1,10 @@
[e-acsl] beginning translation.
-[e-acsl] tests/gmp/at_on-purely-logic-variables.c:55: Warning:
+[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:56: Warning:
+[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.
@@ -19,6 +19,8 @@
__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:
@@ -42,27 +44,29 @@
starting to merge loop iterations
[eva:alarm] tests/gmp/at_on-purely-logic-variables.c:28: Warning:
out of bounds write. assert \valid(__gen_e_acsl_at + 0);
+[eva:alarm] tests/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:57:
+ starting to merge loop iterations
[eva:alarm] tests/gmp/at_on-purely-logic-variables.c:45: Warning:
out of bounds write.
assert
\valid(__gen_e_acsl_at_6 +
(int)((int)((int)(__gen_e_acsl_u_4 - 9) * 32) +
- (int)(__gen_e_acsl_v_4 - -4)));
+ (int)((int)(__gen_e_acsl_v_4 - -5) - 1)));
[eva] tests/gmp/at_on-purely-logic-variables.c:45:
starting to merge loop iterations
-[eva:alarm] tests/gmp/at_on-purely-logic-variables.c:45: Warning:
- signed overflow. assert __gen_e_acsl_v_4 - -4 ≤ 2147483647;
-[eva:alarm] tests/gmp/at_on-purely-logic-variables.c:45: Warning:
- signed overflow.
- assert
- (int)((int)(__gen_e_acsl_u_4 - 9) * 32) + (int)(__gen_e_acsl_v_4 - -4) ≤
- 2147483647;
[eva:alarm] tests/gmp/at_on-purely-logic-variables.c:34: Warning:
out of bounds write.
assert
\valid(__gen_e_acsl_at_3 +
(int)((int)((int)(__gen_e_acsl_u_2 - 9) * 11) +
- (int)(__gen_e_acsl_v_2 - -4)));
+ (int)((int)(__gen_e_acsl_v_2 - -5) - 1)));
[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:
@@ -91,20 +95,20 @@
accessing uninitialized left-value.
assert
\initialized(__gen_e_acsl_at_3 +
- ((__gen_e_acsl_u - 9) * 11 + (__gen_e_acsl_v - -4)));
+ ((__gen_e_acsl_u - 9) * 11 + ((__gen_e_acsl_v - -5) - 1)));
[eva:alarm] tests/gmp/at_on-purely-logic-variables.c:33: Warning:
out of bounds read.
assert
\valid_read(__gen_e_acsl_at_3 +
(int)((int)((int)(__gen_e_acsl_u - 9) * 11) +
- (int)(__gen_e_acsl_v - -4)));
+ (int)((int)(__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:37: Warning:
assertion got status unknown.
[eva:alarm] tests/gmp/at_on-purely-logic-variables.c:41: Warning:
out of bounds write.
- assert \valid(__gen_e_acsl_at_5 + (int)(__gen_e_acsl_k_4 - -8));
+ assert \valid(__gen_e_acsl_at_5 + (int)((int)(__gen_e_acsl_k_4 - -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:
@@ -113,10 +117,11 @@
function __e_acsl_assert: precondition 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 - -8));
+ assert \initialized(__gen_e_acsl_at_5 + ((__gen_e_acsl_k_3 - -9) - 1));
[eva:alarm] tests/gmp/at_on-purely-logic-variables.c:41: Warning:
out of bounds read.
- assert \valid_read(__gen_e_acsl_at_5 + (int)(__gen_e_acsl_k_3 - -8));
+ assert
+ \valid_read(__gen_e_acsl_at_5 + (int)((int)(__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:
@@ -129,13 +134,13 @@
accessing uninitialized left-value.
assert
\initialized(__gen_e_acsl_at_6 +
- ((__gen_e_acsl_u_3 - 9) * 32 + (__gen_e_acsl_v_3 - -4)));
+ ((__gen_e_acsl_u_3 - 9) * 32 + ((__gen_e_acsl_v_3 - -5) - 1)));
[eva:alarm] tests/gmp/at_on-purely-logic-variables.c:44: Warning:
out of bounds read.
assert
\valid_read(__gen_e_acsl_at_6 +
(int)((int)((int)(__gen_e_acsl_u_3 - 9) * 32) +
- (int)(__gen_e_acsl_v_3 - -4)));
+ (int)((int)(__gen_e_acsl_v_3 - -5) - 1)));
[eva] tests/gmp/at_on-purely-logic-variables.c:44:
starting to merge loop iterations
[eva] tests/gmp/at_on-purely-logic-variables.c:8:
@@ -152,12 +157,12 @@
out of bounds write. assert \valid(__gen_e_acsl_at_3 + 0);
[eva:alarm] tests/gmp/at_on-purely-logic-variables.c:7: Warning:
out of bounds write.
- assert \valid(__gen_e_acsl_at_2 + (int)(__gen_e_acsl_n_3 - 2));
+ assert \valid(__gen_e_acsl_at_2 + (int)((int)(__gen_e_acsl_n_3 - 1) - 1));
[eva] tests/gmp/at_on-purely-logic-variables.c:7:
starting to merge loop iterations
[eva:alarm] tests/gmp/at_on-purely-logic-variables.c:7: Warning:
out of bounds write.
- assert \valid(__gen_e_acsl_at + (int)(__gen_e_acsl_n_2 - 2));
+ assert \valid(__gen_e_acsl_at + (int)((int)(__gen_e_acsl_n_2 - 1) - 1));
[eva] tests/gmp/at_on-purely-logic-variables.c:7:
starting to merge loop iterations
[eva] using specification for function __e_acsl_delete_block
@@ -165,18 +170,18 @@
function __e_acsl_assert: precondition got status unknown.
[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 - 2));
+ assert \initialized(__gen_e_acsl_at + ((__gen_e_acsl_n - 1) - 1));
[eva:alarm] tests/gmp/at_on-purely-logic-variables.c:7: Warning:
out of bounds read.
- assert \valid_read(__gen_e_acsl_at + (int)(__gen_e_acsl_n - 2));
+ assert \valid_read(__gen_e_acsl_at + (int)((int)(__gen_e_acsl_n - 1) - 1));
[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:
accessing uninitialized left-value.
- assert \initialized(__gen_e_acsl_at_2 + (__gen_e_acsl_n - 2));
+ assert \initialized(__gen_e_acsl_at_2 + ((__gen_e_acsl_n - 1) - 1));
[eva:alarm] tests/gmp/at_on-purely-logic-variables.c:7: Warning:
out of bounds read.
- assert \valid_read(__gen_e_acsl_at_2 + (int)(__gen_e_acsl_n - 2));
+ assert \valid_read(__gen_e_acsl_at_2 + (int)((int)(__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:6: Warning:
@@ -206,7 +211,25 @@
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:57: Warning:
+ function __e_acsl_assert: precondition 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:56: Warning:
+ out of bounds read.
+ assert
+ \valid_read(__gen_e_acsl_at_7 +
+ (int)((int)((int)(__gen_e_acsl_u_5 - 10) * 300) +
+ (int)((int)((int)((int)(__gen_e_acsl_v_5 - -10) - 1) * 100)
+ + (int)((int)(__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
index 6cd8b6b75df..1e6a8533f45 100644
--- 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
@@ -32,12 +32,17 @@
`\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:55: Warning:
+[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:56: Warning:
+[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.
@@ -85,7 +90,9 @@
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:56: Warning:
+[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
index 8fdcd544b06..fa086a5115b 100644
--- 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
@@ -26,16 +26,15 @@ void g(void)
{
int __gen_e_acsl_w_2;
__gen_e_acsl_w_2 = 3;
- while (1)
- if (__gen_e_acsl_w_2 <= 5) {
- /*@ assert
- Value: mem_access:
- \valid(__gen_e_acsl_at + (int)(__gen_e_acsl_w_2 - 3));
- */
- *(__gen_e_acsl_at + (__gen_e_acsl_w_2 - 3)) = m + (long)__gen_e_acsl_w_2 == 12L;
- __gen_e_acsl_w_2 ++;
- }
- else break;
+ while (1) {
+ if (__gen_e_acsl_w_2 < 6) ; else break;
+ /*@ assert
+ Value: mem_access:
+ \valid(__gen_e_acsl_at + (int)(__gen_e_acsl_w_2 - 3));
+ */
+ *(__gen_e_acsl_at + (__gen_e_acsl_w_2 - 3)) = m + (long)__gen_e_acsl_w_2 == 12L;
+ __gen_e_acsl_w_2 ++;
+ }
}
;
}
@@ -85,6 +84,7 @@ void g(void)
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;
@@ -94,6 +94,7 @@ int main(void)
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);
@@ -114,16 +115,15 @@ int main(void)
{
int __gen_e_acsl_j_2;
__gen_e_acsl_j_2 = 2;
- while (1)
- if (__gen_e_acsl_j_2 <= 4) {
- /*@ assert
- Value: mem_access:
- \valid(__gen_e_acsl_at_2 + (int)(__gen_e_acsl_j_2 - 2));
- */
- *(__gen_e_acsl_at_2 + (__gen_e_acsl_j_2 - 2)) = n + (long)__gen_e_acsl_j_2 == 11L;
- __gen_e_acsl_j_2 ++;
- }
- else break;
+ while (1) {
+ if (__gen_e_acsl_j_2 < 5) ; else break;
+ /*@ assert
+ Value: mem_access:
+ \valid(__gen_e_acsl_at_2 + (int)(__gen_e_acsl_j_2 - 2));
+ */
+ *(__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;
@@ -137,78 +137,104 @@ int main(void)
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 <= 20) {
+ while (1) {
+ if (__gen_e_acsl_u_4 < 21) ; else break;
+ __gen_e_acsl_v_4 = -5 + 1;
+ while (1) {
{
- int __gen_e_acsl_v_4;
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;
- __gen_e_acsl_v_4 = -5 + 1;
- while (1)
- if (__gen_e_acsl_v_4 <= __gen_e_acsl_if_2) {
- /*@ assert
- Value: mem_access:
- \valid(__gen_e_acsl_at_6 +
- (int)((int)((int)(__gen_e_acsl_u_4 - 9) * 32) +
- (int)(__gen_e_acsl_v_4 - -4)));
- */
- /*@ assert
- Value: signed_overflow:
- __gen_e_acsl_v_4 - -4 ≤ 2147483647;
- */
- /*@ assert
- Value: signed_overflow:
- (int)((int)(__gen_e_acsl_u_4 - 9) * 32) +
- (int)(__gen_e_acsl_v_4 - -4) ≤ 2147483647;
- */
- *(__gen_e_acsl_at_6 + ((__gen_e_acsl_u_4 - 9) * 32 + (
- __gen_e_acsl_v_4 - -4))) = (n + (long)__gen_e_acsl_u_4) + n > 0L;
- __gen_e_acsl_v_4 ++;
- }
- else break;
+ if (__gen_e_acsl_v_4 <= __gen_e_acsl_if_2) ; else break;
}
- __gen_e_acsl_u_4 ++;
+ /*@ assert
+ Value: mem_access:
+ \valid(__gen_e_acsl_at_6 +
+ (int)((int)((int)(__gen_e_acsl_u_4 - 9) * 32) +
+ (int)((int)(__gen_e_acsl_v_4 - -5) - 1)));
+ */
+ *(__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) + n > 0L;
+ __gen_e_acsl_v_4 ++;
}
- else break;
+ __gen_e_acsl_u_4 ++;
+ }
}
{
int __gen_e_acsl_k_2;
- {
- int __gen_e_acsl_u_2;
- __gen_e_acsl_k_2 = -7;
- __gen_e_acsl_u_2 = 9;
- while (1)
- if (__gen_e_acsl_u_2 <= 20) {
- {
- int __gen_e_acsl_v_2;
- __gen_e_acsl_v_2 = -5 + 1;
- while (1)
- if (__gen_e_acsl_v_2 <= 6) {
- {
- 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;
- /*@ assert
- Value: mem_access:
- \valid(__gen_e_acsl_at_3 +
- (int)((int)((int)(__gen_e_acsl_u_2 - 9) * 11)
- + (int)(__gen_e_acsl_v_2 - -4)));
- */
- *(__gen_e_acsl_at_3 + ((__gen_e_acsl_u_2 - 9) * 11 + (
- __gen_e_acsl_v_2 - -4))) =
- __gen_e_acsl_if > 0L;
- }
- __gen_e_acsl_v_2 ++;
- }
- else break;
- }
- __gen_e_acsl_u_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;
+ /*@ assert
+ Value: mem_access:
+ \valid(__gen_e_acsl_at_3 +
+ (int)((int)((int)(__gen_e_acsl_u_2 - 9) * 11) +
+ (int)((int)(__gen_e_acsl_v_2 - -5) - 1)));
+ */
+ *(__gen_e_acsl_at_3 + ((__gen_e_acsl_u_2 - 9) * 11 + ((__gen_e_acsl_v_2 - -5) - 1))) =
+ __gen_e_acsl_if > 0L;
}
- else break;
+ __gen_e_acsl_v_2 ++;
+ }
+ __gen_e_acsl_u_2 ++;
}
}
;
@@ -299,27 +325,28 @@ int main(void)
(long)((int)(
(long)((int)(
__gen_e_acsl_u - 9L)) * 11L)) + (int)(
- __gen_e_acsl_v - -4L))),
+ (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)(__gen_e_acsl_v - -4)))",
+ (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 - -4)));
+ ((__gen_e_acsl_v - -5) - 1)));
*/
/*@ assert
Value: mem_access:
\valid_read(__gen_e_acsl_at_3 +
(int)((int)((int)(__gen_e_acsl_u - 9) * 11) +
- (int)(__gen_e_acsl_v - -4)));
+ (int)((int)(__gen_e_acsl_v - -5) - 1)));
*/
- if (*(__gen_e_acsl_at_3 + ((__gen_e_acsl_u - 9) * 11 + (__gen_e_acsl_v - -4))))
+ if (*(__gen_e_acsl_at_3 + ((__gen_e_acsl_u - 9) * 11 + ((
+ __gen_e_acsl_v - -5) - 1))))
;
else {
__gen_e_acsl_forall = 0;
@@ -364,16 +391,16 @@ int main(void)
{
int __gen_e_acsl_k_4;
__gen_e_acsl_k_4 = -9 + 1;
- while (1)
- if (__gen_e_acsl_k_4 <= -1) {
- /*@ assert
- Value: mem_access:
- \valid(__gen_e_acsl_at_5 + (int)(__gen_e_acsl_k_4 - -8));
- */
- *(__gen_e_acsl_at_5 + (__gen_e_acsl_k_4 - -8)) = m + (long)__gen_e_acsl_k_4;
- __gen_e_acsl_k_4 ++;
- }
- else break;
+ while (1) {
+ if (__gen_e_acsl_k_4 < 0) ; else break;
+ /*@ assert
+ Value: mem_access:
+ \valid(__gen_e_acsl_at_5 +
+ (int)((int)(__gen_e_acsl_k_4 - -9) - 1));
+ */
+ *(__gen_e_acsl_at_5 + ((__gen_e_acsl_k_4 - -9) - 1)) = m + (long)__gen_e_acsl_k_4;
+ __gen_e_acsl_k_4 ++;
+ }
}
;
}
@@ -388,24 +415,26 @@ int main(void)
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 - -8L)),
+ __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: \\valid_read(__gen_e_acsl_at_5 + (int)(__gen_e_acsl_k_3 - -8))",
+ (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 - -8));
+ \initialized(__gen_e_acsl_at_5 + ((__gen_e_acsl_k_3 - -9) - 1));
*/
/*@ assert
Value: mem_access:
- \valid_read(__gen_e_acsl_at_5 + (int)(__gen_e_acsl_k_3 - -8));
+ \valid_read(__gen_e_acsl_at_5 +
+ (int)((int)(__gen_e_acsl_k_3 - -9) - 1));
*/
- if (! (*(__gen_e_acsl_at_5 + (__gen_e_acsl_k_3 - -8)) == 0L))
+ if (! (*(__gen_e_acsl_at_5 + ((__gen_e_acsl_k_3 - -9) - 1)) == 0L))
;
else {
__gen_e_acsl_exists_3 = 1;
@@ -450,28 +479,29 @@ int main(void)
(long)((int)(
(long)((int)(
__gen_e_acsl_u_3 - 9L)) * 32L)) + (int)(
- __gen_e_acsl_v_3 - -4L))),
+ (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)(__gen_e_acsl_v_3 - -4)))",
+ (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 - -4)));
+ ((__gen_e_acsl_v_3 - -5) - 1)));
*/
/*@ assert
Value: mem_access:
\valid_read(__gen_e_acsl_at_6 +
(int)((int)((int)(__gen_e_acsl_u_3 - 9) * 32) +
- (int)(__gen_e_acsl_v_3 - -4)));
+ (int)((int)(__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 - -4)))) ;
+ (__gen_e_acsl_v_3 - -5) - 1))))
+ ;
else {
__gen_e_acsl_forall_2 = 0;
goto e_acsl_end_loop6;
@@ -498,6 +528,116 @@ int main(void)
__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))));
+ */
+ /*@ assert
+ Value: mem_access:
+ \valid_read(__gen_e_acsl_at_7 +
+ (int)((int)((int)(__gen_e_acsl_u_5 - 10) *
+ 300)
+ +
+ (int)((int)((int)((int)(__gen_e_acsl_v_5
+ - -10)
+ - 1)
+ * 100)
+ +
+ (int)((int)(__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);
*/
;
@@ -505,6 +645,7 @@ int main(void)
__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);
@@ -545,30 +686,28 @@ void __gen_e_acsl_f(int *t)
{
int __gen_e_acsl_n_3;
__gen_e_acsl_n_3 = 1 + 1;
- while (1)
- if (__gen_e_acsl_n_3 <= 3) {
- /*@ assert
- Value: mem_access:
- \valid(__gen_e_acsl_at_2 + (int)(__gen_e_acsl_n_3 - 2));
- */
- *(__gen_e_acsl_at_2 + (__gen_e_acsl_n_3 - 2)) = *(t + (__gen_e_acsl_n_3 - 1)) > 5;
- __gen_e_acsl_n_3 ++;
- }
- else break;
+ while (1) {
+ if (__gen_e_acsl_n_3 <= 3) ; else break;
+ /*@ assert
+ Value: mem_access:
+ \valid(__gen_e_acsl_at_2 + (int)((int)(__gen_e_acsl_n_3 - 1) - 1));
+ */
+ *(__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) {
- /*@ assert
- Value: mem_access:
- \valid(__gen_e_acsl_at + (int)(__gen_e_acsl_n_2 - 2));
- */
- *(__gen_e_acsl_at + (__gen_e_acsl_n_2 - 2)) = *(t + __gen_e_acsl_n_2) == 12;
- __gen_e_acsl_n_2 ++;
- }
- else break;
+ while (1) {
+ if (__gen_e_acsl_n_2 <= 3) ; else break;
+ /*@ assert
+ Value: mem_access:
+ \valid(__gen_e_acsl_at + (int)((int)(__gen_e_acsl_n_2 - 1) - 1));
+ */
+ *(__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);
@@ -586,52 +725,56 @@ void __gen_e_acsl_f(int *t)
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)(
- __gen_e_acsl_n - 2L)),
+ (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: \\valid_read(__gen_e_acsl_at + (int)(__gen_e_acsl_n - 2))",
+ (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 - 2));
+ \initialized(__gen_e_acsl_at + ((__gen_e_acsl_n - 1) - 1));
*/
/*@ assert
Value: mem_access:
- \valid_read(__gen_e_acsl_at + (int)(__gen_e_acsl_n - 2));
+ \valid_read(__gen_e_acsl_at +
+ (int)((int)(__gen_e_acsl_n - 1) - 1));
*/
- if (*(__gen_e_acsl_at + (__gen_e_acsl_n - 2))) {
+ 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)(
- __gen_e_acsl_n - 2L)),
+ (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: \\valid_read(__gen_e_acsl_at_2 + (int)(__gen_e_acsl_n - 2))",
+ (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 - 2));
+ \initialized(__gen_e_acsl_at_2 + ((__gen_e_acsl_n - 1) - 1));
*/
/*@ assert
Value: mem_access:
- \valid_read(__gen_e_acsl_at_2 + (int)(__gen_e_acsl_n - 2));
+ \valid_read(__gen_e_acsl_at_2 +
+ (int)((int)(__gen_e_acsl_n - 1) - 1));
*/
- __gen_e_acsl_and = *(__gen_e_acsl_at_2 + (__gen_e_acsl_n - 2));
+ __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_loop8;
+ goto e_acsl_end_loop11;
}
}
__gen_e_acsl_n ++;
}
- e_acsl_end_loop8: ;
+ 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);
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
index e30789c329d..771df194b25 100644
--- 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
@@ -65,6 +65,17 @@ int main(void)
__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);
*/
;
diff --git a/src/plugins/e-acsl/translate.ml b/src/plugins/e-acsl/translate.ml
index 0597e767c07..4d28939e123 100644
--- a/src/plugins/e-acsl/translate.ml
+++ b/src/plugins/e-acsl/translate.ml
@@ -1125,7 +1125,8 @@ 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;
+ 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
diff --git a/src/plugins/e-acsl/translate.mli b/src/plugins/e-acsl/translate.mli
index 77207f00872..4f8540341fa 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
--
GitLab