From 22203ac6f98dc926b65013797558953d03f3ae39 Mon Sep 17 00:00:00 2001
From: "Fonenantsoa Maurica (fmaurica)" <maurica.fonenantsoa@gmail.com>
Date: Wed, 28 Mar 2018 00:02:29 +0200
Subject: [PATCH] Clear environment.
---
src/plugins/e-acsl/interval.ml | 8 ++++++--
src/plugins/e-acsl/interval.mli | 1 +
src/plugins/e-acsl/translate.ml | 5 ++++-
3 files changed, 11 insertions(+), 3 deletions(-)
diff --git a/src/plugins/e-acsl/interval.ml b/src/plugins/e-acsl/interval.ml
index 8cd31ce13cc..d38f8c36f5c 100644
--- a/src/plugins/e-acsl/interval.ml
+++ b/src/plugins/e-acsl/interval.ml
@@ -60,6 +60,7 @@ module Env = struct
let tbl: Ival.t Logic_var.Hashtbl.t = Logic_var.Hashtbl.create 7
let clear () = Logic_var.Hashtbl.clear tbl
let add = Logic_var.Hashtbl.add tbl
+ let remove = Logic_var.Hashtbl.remove tbl
let find = Logic_var.Hashtbl.find tbl
end
@@ -193,9 +194,12 @@ let rec infer t =
| Tlet (li,t) ->
let li_t = Misc.term_of_li li in
+ let li_v = li.l_var_info in
let i = infer li_t in
- Env.add li.l_var_info i;
- infer t
+ Env.add li_v i;
+ let i = infer t in
+ Env.remove li_v;
+ i
| TConst (LStr _ | LWStr _ | LReal _)
| TBinOp (PlusPI,_,_)
| TBinOp (IndexPI,_,_)
diff --git a/src/plugins/e-acsl/interval.mli b/src/plugins/e-acsl/interval.mli
index 6fc70d29a62..b14769feb50 100644
--- a/src/plugins/e-acsl/interval.mli
+++ b/src/plugins/e-acsl/interval.mli
@@ -65,6 +65,7 @@ val interv_of_typ: Cil_types.typ -> Ival.t
module Env: sig
val clear: unit -> unit
val add: Cil_types.logic_var -> Ival.t -> unit
+ val remove: Cil_types.logic_var -> unit
end
(* ************************************************************************** *)
diff --git a/src/plugins/e-acsl/translate.ml b/src/plugins/e-acsl/translate.ml
index d092f7ced5d..f746f2dbb8f 100644
--- a/src/plugins/e-acsl/translate.ml
+++ b/src/plugins/e-acsl/translate.ml
@@ -501,6 +501,7 @@ and context_insensitive_term_to_exp kf env t =
| Tlet(li, t) ->
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;
e, env, false, ""
(* Convert an ACSL term into a corresponding C expression (if any) in the given
@@ -735,7 +736,9 @@ and named_predicate_content_to_exp ?name kf env p =
conditional_to_exp loc None e1 res2 res3
| Plet(li, p) ->
let env = env_of_li li kf env loc in
- named_predicate_to_exp kf env p
+ let e, env = named_predicate_to_exp kf env p in
+ Interval.Env.remove li.l_var_info;
+ e, env
| Pforall _ | Pexists _ -> Quantif.quantif_to_exp kf env p
| Pat(p, BuiltinLabel Here) ->
named_predicate_to_exp kf env p
--
GitLab