From b5532c1b2983bd7486ec6dc87ec366e04c619569 Mon Sep 17 00:00:00 2001
From: Basile Desloges <basile.desloges@cea.fr>
Date: Wed, 12 Jan 2022 16:31:54 +0100
Subject: [PATCH] [eacsl] Fix \let translation
The term corresponding to the logic var introduced is translated without
the logic var in the logic scope.
---
src/plugins/e-acsl/src/analyses/lscope.ml | 3 +++
src/plugins/e-acsl/src/analyses/lscope.mli | 5 +++++
src/plugins/e-acsl/src/code_generator/env.ml | 1 +
src/plugins/e-acsl/src/code_generator/env.mli | 4 ++++
.../e-acsl/src/code_generator/translate_predicates.ml | 7 ++++++-
src/plugins/e-acsl/src/code_generator/translate_terms.ml | 7 ++++++-
6 files changed, 25 insertions(+), 2 deletions(-)
diff --git a/src/plugins/e-acsl/src/analyses/lscope.ml b/src/plugins/e-acsl/src/analyses/lscope.ml
index 3f9c07423ae..3c6db344d75 100644
--- a/src/plugins/e-acsl/src/analyses/lscope.ml
+++ b/src/plugins/e-acsl/src/analyses/lscope.ml
@@ -33,6 +33,9 @@ let is_empty = function [] -> true | _ :: _ -> false
let add lscope_var t = lscope_var :: t
+let remove lscope_var t =
+ List.filter (fun elt -> elt != lscope_var) t
+
let get_all t = t
let exists lv t =
diff --git a/src/plugins/e-acsl/src/analyses/lscope.mli b/src/plugins/e-acsl/src/analyses/lscope.mli
index e3a17b42b52..3b3eba63e48 100644
--- a/src/plugins/e-acsl/src/analyses/lscope.mli
+++ b/src/plugins/e-acsl/src/analyses/lscope.mli
@@ -39,6 +39,11 @@ val is_empty: t -> bool
val add: lscope_var -> t -> t
(* Return a new logic scope in which the given [lscope_var] has been added. *)
+val remove: lscope_var -> t -> t
+(** @return a new logic scope in which the given [lscope_var] has been removed
+ if it was present. Use physical equality to check if the [lscope_var]Â is
+ present. *)
+
val get_all: t -> lscope_var list
(* Return the list of [lscope_var] of the given logic scope.
The first element is the last [lscope_var] that was added to [t], the
diff --git a/src/plugins/e-acsl/src/code_generator/env.ml b/src/plugins/e-acsl/src/code_generator/env.ml
index 5abf328e729..a0c70db9491 100644
--- a/src/plugins/e-acsl/src/code_generator/env.ml
+++ b/src/plugins/e-acsl/src/code_generator/env.ml
@@ -375,6 +375,7 @@ end
module Logic_scope = struct
let get env = env.lscope
let extend env lvs = { env with lscope = Lscope.add lvs env.lscope }
+ let remove env lvs = { env with lscope = Lscope.remove lvs env.lscope }
let set_reset env bool = { env with lscope_reset = bool }
let get_reset env = env.lscope_reset
let reset env =
diff --git a/src/plugins/e-acsl/src/code_generator/env.mli b/src/plugins/e-acsl/src/code_generator/env.mli
index 04117ede82a..7805d06efcb 100644
--- a/src/plugins/e-acsl/src/code_generator/env.mli
+++ b/src/plugins/e-acsl/src/code_generator/env.mli
@@ -131,6 +131,10 @@ module Logic_scope: sig
(** Add a new logic variable with its associated information in the
logic scope of the environment. *)
+ val remove: t -> lscope_var -> t
+ (** Remove a logic variable and its associated information from 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. *)
diff --git a/src/plugins/e-acsl/src/code_generator/translate_predicates.ml b/src/plugins/e-acsl/src/code_generator/translate_predicates.ml
index b9cc28a77dd..d369220466f 100644
--- a/src/plugins/e-acsl/src/code_generator/translate_predicates.ml
+++ b/src/plugins/e-acsl/src/code_generator/translate_predicates.ml
@@ -187,10 +187,15 @@ let rec predicate_content_to_exp ~adata ?name kf env p =
)
env)
| Plet(li, p) ->
+ (* Translate the term registered to the \let logic variable *)
+ let adata, env = Translate_utils.env_of_li ~adata ~loc kf env li in
+ (* Register the logic var to the logic scope *)
let lvs = Lvs_let(li.l_var_info, Misc.term_of_li li) in
let env = Env.Logic_scope.extend env lvs in
- let adata, env = Translate_utils.env_of_li ~adata ~loc kf env li in
+ (* Translate the body of the \let *)
let e, adata, env = to_exp ~adata kf env p in
+ (* Remove the logic var from the logic scope *)
+ let env = Env.Logic_scope.remove env lvs in
Interval.Env.remove li.l_var_info;
e, adata, env
| Pforall _ | Pexists _ ->
diff --git a/src/plugins/e-acsl/src/code_generator/translate_terms.ml b/src/plugins/e-acsl/src/code_generator/translate_terms.ml
index c83b2e2ca84..a1e55e5d0eb 100644
--- a/src/plugins/e-acsl/src/code_generator/translate_terms.ml
+++ b/src/plugins/e-acsl/src/code_generator/translate_terms.ml
@@ -861,10 +861,15 @@ and context_insensitive_term_to_exp ~adata kf env t =
| Tcomprehension _ -> Env.not_yet env "tset comprehension"
| Trange _ -> Env.not_yet env "range"
| Tlet(li, t) ->
+ (* Translate the term registered to the \let logic variable *)
+ let adata, env = Translate_utils.env_of_li ~adata ~loc kf env li in
+ (* Register the logic var to the logic scope *)
let lvs = Lvs_let(li.l_var_info, Misc.term_of_li li) in
let env = Env.Logic_scope.extend env lvs in
- let adata, env = Translate_utils.env_of_li ~adata ~loc kf env li in
+ (* Translate the body of the \let *)
let e, adata, env = to_exp ~adata kf env t in
+ (* Remove the logic var from the logic scope *)
+ let env = Env.Logic_scope.remove env lvs in
Interval.Env.remove li.l_var_info;
e, adata, env, Typed_number.C_number, ""
--
GitLab