From b6be8a9e97d727dcb877cf4bb30ee790a25c955c Mon Sep 17 00:00:00 2001
From: Thibaut Benjamin <thibaut.benjamin@gmail.com>
Date: Wed, 16 Mar 2022 11:20:03 +0100
Subject: [PATCH] [e-acsl] fix typing bug with at translations
---
.../e-acsl/src/analyses/bound_variables.ml | 1 -
.../e-acsl/src/code_generator/translate_ats.ml | 15 ++++++++++++++-
2 files changed, 14 insertions(+), 2 deletions(-)
diff --git a/src/plugins/e-acsl/src/analyses/bound_variables.ml b/src/plugins/e-acsl/src/analyses/bound_variables.ml
index 5199e4e6687..83f51025ce2 100644
--- a/src/plugins/e-acsl/src/analyses/bound_variables.ml
+++ b/src/plugins/e-acsl/src/analyses/bound_variables.ml
@@ -664,7 +664,6 @@ let normalize_guard ~loc (t1, rel1, lv, rel2, t2) =
in
t1, lv, t2
-
let compute_guards loc ~is_forall p bounded_vars hyps =
try
let guards,goal = compute_quantif_guards p ~is_forall bounded_vars hyps in
diff --git a/src/plugins/e-acsl/src/code_generator/translate_ats.ml b/src/plugins/e-acsl/src/code_generator/translate_ats.ml
index c8c3a4197ca..5ce9da77b62 100644
--- a/src/plugins/e-acsl/src/code_generator/translate_ats.ml
+++ b/src/plugins/e-acsl/src/code_generator/translate_ats.ml
@@ -305,11 +305,24 @@ let pretranslate_to_exp_with_lscope ~loc ~lscope kf env pot =
let term_to_exp = !term_to_exp_ref in
let lscope_vars = Lscope.get_all lscope in
let lscope_vars = List.rev lscope_vars in
+ let rec add_lscope_to_logic_env env = function
+ | [] -> env
+ | (Lvs_quantif(t1,_,x,_,t2)::lscope) ->
+ let logic_env = Env.Logic_env.get env in
+ let i = Interval.join
+ (Interval.get ~logic_env t1)
+ (Interval.get ~logic_env t2)
+ in
+ add_lscope_to_logic_env
+ (Env.Logic_env.add_let_quantif_binding env x i)
+ lscope
+ | _::_ -> env
+ in
+ let env = add_lscope_to_logic_env env lscope in
let logic_env = Env.Logic_env.get env in
let sizes_and_shifts =
sizes_and_shifts_from_quantifs ~loc ~logic_env kf lscope_vars []
in
- let logic_env = Env.Logic_env.get env in
(* Creating the pointer *)
let ty = match pot with
| PoT_pred _ ->
--
GitLab