[rte] move rte_annotations to generator

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 ../../.."

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:

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

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

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