From 3f31f5e37ddc602a1a8904dfaacb418b5c48037e Mon Sep 17 00:00:00 2001
From: Basile Desloges <basile.desloges@cea.fr>
Date: Mon, 14 Feb 2022 16:10:00 +0100
Subject: [PATCH] [eacsl] Update Bound_variables to visit global logic
functions and predicates
---
.../e-acsl/src/analyses/bound_variables.ml | 19 +++++++------------
1 file changed, 7 insertions(+), 12 deletions(-)
diff --git a/src/plugins/e-acsl/src/analyses/bound_variables.ml b/src/plugins/e-acsl/src/analyses/bound_variables.ml
index 8f953694307..2d9306e5d21 100644
--- a/src/plugins/e-acsl/src/analyses/bound_variables.ml
+++ b/src/plugins/e-acsl/src/analyses/bound_variables.ml
@@ -696,19 +696,15 @@ end
(Result.Error (Error.make_not_yet "unguarded \\exists quantification"))
| _ -> ()
- let do_user_predicates () =
- let gannot a =
- match a with
- | Dfun_or_pred ({l_body = LBpred p},loc) ->
- let p = Logic_normalizer.get_pred p in
- process_quantif ~loc p
- | _ -> ()
- in
- Annotations.iter_global (fun _ a -> gannot a)
-
let preprocessor = object
inherit E_acsl_visitor.visitor
+ method !glob_annot _ = Cil.DoChildren
+ method !vannotation annot =
+ match annot with
+ | Dfun_or_pred _ -> Cil.DoChildren
+ | _ -> Cil.SkipChildren
+
method !vpredicate p =
let loc = p.pred_loc in
let p = Logic_normalizer.get_pred p in
@@ -720,8 +716,7 @@ end
let compute ast =
Visitor.visitFramacFileSameGlobals
(preprocessor :> Visitor.frama_c_inplace)
- ast;
- do_user_predicates ()
+ ast
let compute_annot annot =
ignore
--
GitLab