From 3994d21bb7f9153b6ba2ea9f4c8c95d1ff82a134 Mon Sep 17 00:00:00 2001
From: Basile Desloges <basile.desloges@cea.fr>
Date: Fri, 11 Feb 2022 17:49:04 +0100
Subject: [PATCH] [eacsl] Add a function to allow visiting global_annotation in
E_acsl_visitor
---
src/plugins/e-acsl/src/analyses/e_acsl_visitor.ml | 10 +++++++++-
src/plugins/e-acsl/src/analyses/e_acsl_visitor.mli | 3 +++
2 files changed, 12 insertions(+), 1 deletion(-)
diff --git a/src/plugins/e-acsl/src/analyses/e_acsl_visitor.ml b/src/plugins/e-acsl/src/analyses/e_acsl_visitor.ml
index fea87f8c78f..a706022893e 100644
--- a/src/plugins/e-acsl/src/analyses/e_acsl_visitor.ml
+++ b/src/plugins/e-acsl/src/analyses/e_acsl_visitor.ml
@@ -31,6 +31,7 @@ let case_globals
?(var_fun_decl = fun _ -> default ())
?(var_init = fun _ -> default ())
?(var_def = fun _ _ -> default ())
+ ?(glob_annot = fun _ -> default ())
~fun_def
= function
(* library functions and built-ins *)
@@ -65,6 +66,10 @@ let case_globals
| GFun(fundec, _) ->
fun_def fundec
+ (* global annotation *)
+ | GAnnot (ga, _) ->
+ glob_annot ga
+
(* other globals: nothing to do *)
| GType _
| GCompTag _
@@ -74,7 +79,6 @@ let case_globals
| GAsm _
| GPragma _
| GText _
- | GAnnot _ (* do never read annotation from sources *)
->
default ()
@@ -106,6 +110,9 @@ class visitor
method var_def : varinfo -> init -> global list Cil.visitAction =
fun _ _ -> self#default ()
+ method glob_annot: global_annotation -> global list Cil.visitAction =
+ fun _ -> self#default ()
+
method fun_def ({svar = vi}) =
let kf = try Globals.Functions.get vi with Not_found -> assert false in
if Functions.check kf then Cil.DoChildren else Cil.SkipChildren
@@ -120,5 +127,6 @@ class visitor
~var_fun_decl:self#var_fun_decl
~var_init:self#var_init
~var_def:self#var_def
+ ~glob_annot:self#glob_annot
~fun_def:self#fun_def
end
diff --git a/src/plugins/e-acsl/src/analyses/e_acsl_visitor.mli b/src/plugins/e-acsl/src/analyses/e_acsl_visitor.mli
index b1f50d9faaf..21ca0fea5d1 100644
--- a/src/plugins/e-acsl/src/analyses/e_acsl_visitor.mli
+++ b/src/plugins/e-acsl/src/analyses/e_acsl_visitor.mli
@@ -31,6 +31,7 @@ val case_globals :
?var_fun_decl:(varinfo -> 'a) ->
?var_init:(varinfo -> 'a) ->
?var_def:(varinfo -> init -> 'a) ->
+ ?glob_annot:(global_annotation -> 'a) ->
fun_def:(fundec -> 'a) ->
global -> 'a
(** Function to descend into the root of the ast according to the various cases
@@ -47,6 +48,7 @@ val case_globals :
value
- [var_def] is the case for variable definitions with an initialization
value
+ - [glob_annot] is the case for global annotations
- [fun_def] is the case for function definition. *)
(** Visitor for managing the root of the AST, on the globals level, with the
@@ -64,5 +66,6 @@ class visitor :
method var_fun_decl: varinfo -> global list Cil.visitAction
method var_init: varinfo -> global list Cil.visitAction
method var_def: varinfo -> init -> global list Cil.visitAction
+ method glob_annot: global_annotation -> global list Cil.visitAction
method fun_def: fundec -> global list Cil.visitAction
end
--
GitLab