From a01a97eceaf09badc24cc6f7021d62395b52138d Mon Sep 17 00:00:00 2001
From: Thibaut Benjamin <thibaut.benjamin@cea.fr>
Date: Wed, 10 Nov 2021 10:10:50 +0100
Subject: [PATCH] [e-acsl] second code review
---
src/plugins/e-acsl/src/analyses/bound_variables.ml | 12 ++++--------
src/plugins/e-acsl/src/code_generator/loops.ml | 7 ++++---
src/plugins/e-acsl/src/code_generator/translate.ml | 4 +---
3 files changed, 9 insertions(+), 14 deletions(-)
diff --git a/src/plugins/e-acsl/src/analyses/bound_variables.ml b/src/plugins/e-acsl/src/analyses/bound_variables.ml
index 286d38ebb20..b3d4452cdf8 100644
--- a/src/plugins/e-acsl/src/analyses/bound_variables.ml
+++ b/src/plugins/e-acsl/src/analyses/bound_variables.ml
@@ -697,14 +697,10 @@ end
let do_user_predicates () =
let gannot a =
match a with
- | Dfun_or_pred (li,loc) ->
- (match li.l_body with
- | LBpred p ->
- (match Logic_normalizer.get_pred p with
- | PoT_pred p -> process_quantif ~loc p
- | PoT_term _ -> ())
- | _ -> ())
-
+ | Dfun_or_pred ({l_body = LBpred p},loc) ->
+ (match Logic_normalizer.get_pred p with
+ | PoT_pred p -> process_quantif ~loc p
+ | PoT_term _ -> ())
| _ -> ()
in
Annotations.iter_global (fun _ a -> gannot a)
diff --git a/src/plugins/e-acsl/src/code_generator/loops.ml b/src/plugins/e-acsl/src/code_generator/loops.ml
index 1bd660bab3f..25f51fa0e06 100644
--- a/src/plugins/e-acsl/src/code_generator/loops.ml
+++ b/src/plugins/e-acsl/src/code_generator/loops.ml
@@ -65,9 +65,10 @@ let handle_annotations env kf stmt =
| Some (t, measure_opt) ->
let env = Env.set_annotation_kind env Smart_stmt.Variant in
let env = Env.push env in
- let lenv = Env.Local_vars.get env in
- Typing.type_term ~use_gmp_opt:true ~lenv t;
- let ty = Typing.get_typ ~lenv t in
+ (* There cannot be bound logical variables since we cannot write
+ loops inside logic functions or predicates, hence lenv is []*)
+ Typing.type_term ~use_gmp_opt:true ~lenv:[] t;
+ let ty = Typing.get_typ ~lenv:[] t in
if Gmp_types.is_t ty then Error.not_yet "loop variant using GMP";
let e, _, env = !term_to_exp_ref ~adata:Assert.no_data kf env t in
let vi_old, e_old, env =
diff --git a/src/plugins/e-acsl/src/code_generator/translate.ml b/src/plugins/e-acsl/src/code_generator/translate.ml
index a60a380c5f7..f38b09429a3 100644
--- a/src/plugins/e-acsl/src/code_generator/translate.ml
+++ b/src/plugins/e-acsl/src/code_generator/translate.ml
@@ -1056,9 +1056,7 @@ and predicate_content_to_exp ~adata ?name kf env p =
| Pvalid_function _ -> Env.not_yet env "\\valid_function"
| Prel(rel, t1, t2) ->
let ity =
- Typing.get_integer_op_of_predicate
- ~lenv
- p
+ Typing.get_integer_op_of_predicate ~lenv p
in
comparison_to_exp ~adata ~loc kf env ity (relation_to_binop rel) t1 t2 None
| Pand(p1, p2) ->
--
GitLab