diff --git a/src/plugins/rte/generator.ml b/src/plugins/rte/generator.ml index e72328ab527209dcb2fb77f130ecc8b50d22e271..2a944b6c6cd35202120b084850912182623afb20 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 2ed6fe38a32711de556d8e0466b224b5050a7655..ae903fb0bc863326a6931efe17bf75d1c75fb9d0 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 8831d66b29bd97f63ed288741c8d83c607594568..e5b0281e856294890fce6be9e06be3a4c1b18d7f 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 dea0d52eeee985c6c0693ba1b6ac6231df4e5bf8..a47464475015f9df6a626f49e7e30309103b6bd8 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 1f75de9bd222c330dcaff8e224781f593ddfb688..1127c3c52b9a64d217b44f32edef1c817a21ce60 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