From 59a46b9366135a9df70f0daa5af4345b134c374b Mon Sep 17 00:00:00 2001
From: Thibaut Benjamin <thibaut.benjamin@cea.fr>
Date: Fri, 20 Aug 2021 10:28:59 +0200
Subject: [PATCH] [e-acsl] add the propagation of a local environment
---
src/plugins/e-acsl/src/analyses/typing.ml | 4 ++--
src/plugins/e-acsl/src/analyses/typing.mli | 2 +-
src/plugins/e-acsl/src/code_generator/translate.ml | 6 +++++-
3 files changed, 8 insertions(+), 4 deletions(-)
diff --git a/src/plugins/e-acsl/src/analyses/typing.ml b/src/plugins/e-acsl/src/analyses/typing.ml
index 0ceb31ebeff..1eea5272392 100644
--- a/src/plugins/e-acsl/src/analyses/typing.ml
+++ b/src/plugins/e-acsl/src/analyses/typing.ml
@@ -949,8 +949,8 @@ let get_cast ~lenv t =
try Option.map typ_of_number_ty info.cast
with Not_a_number -> None
-let get_cast_of_predicate p =
- let info = type_predicate p in
+let get_cast_of_predicate ~lenv p =
+ let info = type_predicate ~lenv p in
try Option.map typ_of_number_ty info.cast
with Not_a_number -> assert false
diff --git a/src/plugins/e-acsl/src/analyses/typing.mli b/src/plugins/e-acsl/src/analyses/typing.mli
index ac869b8770c..e56f54b73e9 100644
--- a/src/plugins/e-acsl/src/analyses/typing.mli
+++ b/src/plugins/e-acsl/src/analyses/typing.mli
@@ -138,7 +138,7 @@ val get_op: lenv:Function_params_ty.t -> term -> typ
val get_cast: lenv:Function_params_ty.t -> term -> typ option
(** Get the type which the given term must be converted to (if any). *)
-val get_cast_of_predicate: predicate -> typ option
+val get_cast_of_predicate: lenv:Function_params_ty.t -> predicate -> typ option
(** Like {!get_cast}, but for predicates. *)
val unsafe_set: term -> ?ctx:number_ty -> number_ty -> unit
diff --git a/src/plugins/e-acsl/src/code_generator/translate.ml b/src/plugins/e-acsl/src/code_generator/translate.ml
index 246079281d9..ad07712f4dc 100644
--- a/src/plugins/e-acsl/src/code_generator/translate.ml
+++ b/src/plugins/e-acsl/src/code_generator/translate.ml
@@ -1234,7 +1234,11 @@ and predicate_to_exp ~adata ?name kf ?rte env p =
predicate_content_to_exp ~adata ?name kf env p
in
let env = if rte then translate_rte kf env e else env in
- let cast = Typing.get_cast_of_predicate p in
+ let cast =
+ Typing.get_cast_of_predicate
+ ~lenv:(Env.Local_vars.get env)
+ p
+ in
Extlib.nest
adata
(Typed_number.add_cast
--
GitLab