From 687f1bf2a82e2e7080cf6528b05d06255a3c8ce4 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Loi=CC=88c=20Correnson?= <loic.correnson@cea.fr>
Date: Wed, 20 Feb 2019 17:07:53 +0100
Subject: [PATCH] [rte] move rte_annotations to generator
---
src/plugins/rte/generator.ml | 6 ++++++
src/plugins/rte/generator.mli | 10 +++++++++-
src/plugins/rte/register.ml | 2 +-
src/plugins/rte/visit.ml | 6 ------
src/plugins/rte/visit.mli | 1 -
5 files changed, 16 insertions(+), 9 deletions(-)
diff --git a/src/plugins/rte/generator.ml b/src/plugins/rte/generator.ml
index e72328ab527..2a944b6c6cd 100644
--- a/src/plugins/rte/generator.ml
+++ b/src/plugins/rte/generator.ml
@@ -197,6 +197,12 @@ let emitter =
~correctness:[ Kernel.SafeArrays.parameter ]
~tuning:[]
+let get_registered_annotations stmt =
+ Annotations.fold_code_annot
+ (fun e a acc -> if Emitter.equal e emitter then a ::acc else acc)
+ stmt
+ []
+
(*
Local Variables:
compile-command: "make -C ../../.."
diff --git a/src/plugins/rte/generator.mli b/src/plugins/rte/generator.mli
index 2ed6fe38a32..ae903fb0bc8 100644
--- a/src/plugins/rte/generator.mli
+++ b/src/plugins/rte/generator.mli
@@ -26,6 +26,8 @@ module type S = sig
val accessor: Db.RteGen.status_accessor
end
+(* No module for Trivial: dependency added for generators below *)
+
module Initialized: S
module Mem_access: S
module Pointer_call: S
@@ -41,9 +43,15 @@ module Float_to_int: S
module Finite_float: S
module Bool_value: S
+val all_statuses: Db.RteGen.status_accessor list
+
+(** The Emitter for Annotations registered by RTE *)
val emitter: Emitter.t
-val all_statuses: Db.RteGen.status_accessor list
+open Cil_types
+
+(** Returns all annotations actually {i registered} by RTE so far *)
+val get_registered_annotations: stmt -> code_annotation list
(*
Local Variables:
diff --git a/src/plugins/rte/register.ml b/src/plugins/rte/register.ml
index 8831d66b29b..e5b0281e856 100644
--- a/src/plugins/rte/register.ml
+++ b/src/plugins/rte/register.ml
@@ -83,7 +83,7 @@ let _ =
Cil_datatype.Stmt.ty
(let module L = Datatype.List(Cil_datatype.Code_annotation) in L.ty))
~journalize:true
- Visit.rte_annotations
+ Generator.get_registered_annotations
let _ =
Dynamic.register
diff --git a/src/plugins/rte/visit.ml b/src/plugins/rte/visit.ml
index dea0d52eeee..a4746447501 100644
--- a/src/plugins/rte/visit.ml
+++ b/src/plugins/rte/visit.ml
@@ -457,12 +457,6 @@ class annot_visitor kf flags on_alarm = object (self)
end
-let rte_annotations stmt =
- Annotations.fold_code_annot
- (fun e a acc -> if Emitter.equal e Generator.emitter then a ::acc else acc)
- stmt
- []
-
(** {2 Iterate over Alarms on Cil elements} *)
type on_alarm = kernel_function -> stmt -> invalid:bool -> Alarms.alarm -> unit
diff --git a/src/plugins/rte/visit.mli b/src/plugins/rte/visit.mli
index 1f75de9bd22..1127c3c52b9 100644
--- a/src/plugins/rte/visit.mli
+++ b/src/plugins/rte/visit.mli
@@ -40,7 +40,6 @@ val do_all_rte: kernel_function -> unit
(** Generates all RTEs except preconditions for a given function. *)
val do_rte: kernel_function -> unit
-val rte_annotations: stmt -> code_annotation list
val do_stmt_annotations: kernel_function -> stmt -> code_annotation list
val do_exp_annotations: kernel_function -> stmt -> exp -> code_annotation list
--
GitLab