diff --git a/src/plugins/e-acsl/at_with_lscope.ml b/src/plugins/e-acsl/at_with_lscope.ml
index 6f01e99b7091bbbad80bcff24e2c71173cf71f75..b266dff47c569425190f3ba6912993c39d50e996 100644
--- a/src/plugins/e-acsl/at_with_lscope.ml
+++ b/src/plugins/e-acsl/at_with_lscope.ml
@@ -42,9 +42,10 @@ let term_to_exp_ref
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
- (Cil_datatype.Kf.Hashtbl.remove tbl kf;
- 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
diff --git a/src/plugins/e-acsl/env.ml b/src/plugins/e-acsl/env.ml
index af52b7caf1727639568307e8dfde8728f331fd09..aeb9cc143e247a31d4abaf5747dd76a4e2ce4708 100644
--- a/src/plugins/e-acsl/env.ml
+++ b/src/plugins/e-acsl/env.ml
@@ -61,7 +61,7 @@ type t =
global_mpz_tbl: mpz_tbl;
env_stack: local_env list;
init_env: local_env;
- var_mapping: (Varinfo.t list) Logic_var.Map.t;
+ 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 *)
@@ -302,35 +302,33 @@ module Logic_binding = struct
ty
(fun _ _ -> [])
in
- let bindings =
- try v :: (Logic_var.Map.find logic_v env.var_mapping)
- with Not_found -> [ v ]
+ 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 bindings env.var_mapping }
+ v, e, env
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 remove env v =
- let map = env.var_mapping in
- let bindings =
- try Logic_var.Map.find v env.var_mapping
- with Not_found -> assert false
- in
- match bindings with
- | [] ->
+ 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 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
- | [ _ ] ->
- { 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/loops.ml b/src/plugins/e-acsl/loops.ml
index 9f982de071a9bca5c257ab8e7508b34c796bdb58..b359b7beb1d82d9b23977ef0977a608a08ab8379 100644
--- a/src/plugins/e-acsl/loops.ml
+++ b/src/plugins/e-acsl/loops.ml
@@ -173,7 +173,7 @@ let rec mk_nested_loops ~loc mk_innermost_block kf env lscope_vars =
Env.Middle
in
(* generate the guard [x bop t2] *)
- let stmts_block b = [ mkStmt ~valid_sid:true (Block b) ] in
+ 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 *)
@@ -195,7 +195,7 @@ let rec mk_nested_loops ~loc mk_innermost_block kf env lscope_vars =
~global_clear:false
Env.Middle
in
- let guard = stmts_block guard_blk 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
@@ -211,18 +211,18 @@ let rec mk_nested_loops ~loc mk_innermost_block kf env lscope_vars =
(* 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 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),
+ mkBlock (guard :: body @ [ next ]),
loc,
None,
Some break_stmt))
in
- start @ [ stmt ], env
+ [ 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
diff --git a/src/plugins/e-acsl/loops.mli b/src/plugins/e-acsl/loops.mli
index ba113cea4dbef7ee7be3b9f53d4a2bb508141977..1f2d658a8e25528cc3367cbb4906ba003e331271 100644
--- a/src/plugins/e-acsl/loops.mli
+++ b/src/plugins/e-acsl/loops.mli
@@ -49,7 +49,7 @@ 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)
+ 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
diff --git a/src/plugins/e-acsl/lscope.ml b/src/plugins/e-acsl/lscope.ml
index a14a42fa1c9dcd4c1b0551bdc179cc081d4292bf..e3c50676d35aa7e0f3c9aea1ecbc1ccd8aac5e50 100644
--- a/src/plugins/e-acsl/lscope.ml
+++ b/src/plugins/e-acsl/lscope.ml
@@ -51,8 +51,8 @@ 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.DoChildren
- | None -> if exists lv lscope then raise Lscope_used else Cil.DoChildren
+ | Some _ -> Cil.SkipChildren
+ | None -> if exists lv lscope then raise Lscope_used else Cil.SkipChildren
end
in
try
diff --git a/src/plugins/e-acsl/lscope.mli b/src/plugins/e-acsl/lscope.mli
index dbc8a2560f34e3cd7cd615d820887c4426802802..d3c80d15fe87391bc9ec129f10fad2c0201bd5a6 100644
--- a/src/plugins/e-acsl/lscope.mli
+++ b/src/plugins/e-acsl/lscope.mli
@@ -29,7 +29,6 @@ open Cil_types
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
- (* 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 c0910b7eda764b44bc87928bd5e36832312aaab7..fa8fc69a5ef68fe8f93d9ae7f14cafd5a645804f 100644
--- a/src/plugins/e-acsl/quantif.ml
+++ b/src/plugins/e-acsl/quantif.ml
@@ -119,15 +119,14 @@ let convert kf env loc is_forall p bounded_vars hyps goal =
let guards = compute_quantif_guards p bounded_vars hyps in
(* 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_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
- env_ref := Env.Logic_scope.extend !env_ref lvs;
- lvs)
+ let env = Env.Logic_scope.extend env lvs in
+ lvs :: lvs_guards, env)
guards
+ ([], env)
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
@@ -138,8 +137,8 @@ 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
(* innermost block *)
diff --git a/src/plugins/e-acsl/translate.ml b/src/plugins/e-acsl/translate.ml
index 4d28939e1234d478b6a8a02c0e401277abf4cabc..8afed8ab60fd26c4412c5a6d3b2fa3d27ac2deee 100644
--- a/src/plugins/e-acsl/translate.ml
+++ b/src/plugins/e-acsl/translate.ml
@@ -552,14 +552,13 @@ and context_insensitive_term_to_exp kf env t =
| Tat(t', label) ->
let lscope = Env.Logic_scope.get env in
let pot = Misc.PoT_term t' in
- if not (Lscope.is_used lscope pot) then begin
+ 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, ""
- end else begin
- let e, env = At_with_lscope.to_exp ~loc kf env pot label in
- e, env, false, ""
- end
| Tbase_addr(BuiltinLabel Here, t) ->
mmodel_call ~loc kf "base_addr" Cil.voidPtrType env t
| Tbase_addr _ -> not_yet env "labeled \\base_addr"
@@ -1005,14 +1004,15 @@ and named_predicate_content_to_exp ?name kf env p =
| Pat(p', label) ->
let lscope = Env.Logic_scope.get env in
let pot = Misc.PoT_pred p' in
- if not (Lscope.is_used lscope pot) then begin
+ 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 else
- At_with_lscope.to_exp ~loc kf env pot label
+ end
| Pvalid_read(BuiltinLabel Here as llabel, t) as pc
| (Pvalid(BuiltinLabel Here as llabel, t) as pc) ->
let call_valid t =