[rte] low-level visitor API

src/plugins/rte/RteGen.mli

@@ -20,4 +20,52 @@
 (*                                                                        *)
 (**************************************************************************)
 
-(** No function is directly exported: they are registered in {!Db.Value}. *)
+(** Some functions are also registered in {!Db.Value}. *)
+
+open Cil_types
+
+module Visit :
+sig
+
+  (** Low-level iterator
+
+      [generator ~options:... on_alarm kf stmt element] iterates over
+      potential alarms for Cil element, located in the given
+      kernel_function and stmt.
+
+      The [on_alarm ki ?status alarm] callback is invoked with
+      the k-instruction originating the alarm and the already known status,
+      if any.
+
+      Potential alarms can be specified by the provided options,
+      with defaults generated from the Kernel options and the RTE plug-in
+      options.
+  *)
+  type 'a generator =
+    ?remove_trivial:bool ->
+    ?initialized:Options.DoInitialized.t ->
+    ?mem_access:Options.DoMemAccess.t ->
+    ?div_mod:Options.DoDivMod.t ->
+    ?shift:Options.DoShift.t ->
+    ?left_shift_negative:Kernel.LeftShiftNegative.t ->
+    ?right_shift_negative:Kernel.RightShiftNegative.t ->
+    ?signed_overflow:Kernel.SignedOverflow.t ->
+    ?unsigned_overflow:Kernel.UnsignedOverflow.t ->
+    ?signed_downcast:Kernel.SignedDowncast.t ->
+    ?unsigned_downcast:Kernel.UnsignedDowncast.t ->
+    ?float_to_int:Options.DoFloatToInt.t ->
+    ?finite_float:bool ->
+    ?pointer_call:Options.DoPointerCall.t ->
+    ?bool_value:Kernel.InvalidBool.t ->
+    (Cil_types.kinstr ->
+     ?status:Property_status.emitted_status -> Alarms.alarm -> unit) ->
+    Kernel_function.t ->
+    Cil_types.stmt ->
+    'a -> unit
+
+  val iter_lval : lval generator
+  val iter_exp : exp generator
+  val iter_instr : instr generator
+  val iter_stmt : stmt generator
+
+end

src/plugins/rte/visit.ml

@@ -445,6 +445,49 @@ let rte_annotations stmt =
     stmt
     []
 
+(** {2 Iterate over Alarms on Cil elements} *)
+
+type 'a generator =
+  ?remove_trivial:bool ->
+  ?initialized:Options.DoInitialized.t ->
+  ?mem_access:Options.DoMemAccess.t ->
+  ?div_mod:Options.DoDivMod.t ->
+  ?shift:Options.DoShift.t ->
+  ?left_shift_negative:Kernel.LeftShiftNegative.t ->
+  ?right_shift_negative:Kernel.RightShiftNegative.t ->
+  ?signed_overflow:Kernel.SignedOverflow.t ->
+  ?unsigned_overflow:Kernel.UnsignedOverflow.t ->
+  ?signed_downcast:Kernel.SignedDowncast.t ->
+  ?unsigned_downcast:Kernel.UnsignedDowncast.t ->
+  ?float_to_int:Options.DoFloatToInt.t ->
+  ?finite_float:bool ->
+  ?pointer_call:Options.DoPointerCall.t ->
+  ?bool_value:Kernel.InvalidBool.t ->
+  (Cil_types.kinstr ->
+   ?status:Property_status.emitted_status -> Alarms.alarm -> unit) ->
+  Kernel_function.t ->
+  Cil_types.stmt ->
+  'a -> unit
+
+let iter_alarms visit to_annot on_alarm kf stmt element =
+  let visitor = object (self)
+    inherit annot_visitor kf to_annot on_alarm
+    initializer self#push_stmt stmt
+  end in
+  ignore (visit (visitor :> Cil.cilVisitor) element)
+
+let iter_lval : lval generator =
+  annotate_from_options (iter_alarms Cil.visitCilLval)
+
+let iter_exp : exp generator =
+  annotate_from_options (iter_alarms Cil.visitCilExpr)
+
+let iter_instr : instr generator =
+  annotate_from_options (iter_alarms Cil.visitCilInstr)
+
+let iter_stmt : stmt generator =
+  annotate_from_options (iter_alarms Cil.visitCilStmt)
+
 (** {2 List of all RTEs on a given Cil object} *)
 
 let get_annotations from kf stmt x =

src/plugins/rte/visit.mli

@@ -22,6 +22,47 @@
 
 open Cil_types
 
+(** Low-level iterator
+
+    [generator ~options:... on_alarm kf stmt element] iterates over
+    potential alarms for Cil element, located in the given
+    kernel_function and stmt.
+
+    The [on_alarm ki ?status alarm] callback is invoked with
+    the k-instruction originating the alarm and the already known status,
+    if any.
+
+    Potential alarms can be specified by the provided options,
+    with defaults generated from the Kernel options and the RTE plug-in
+    options.
+*)
+type 'a generator =
+  ?remove_trivial:bool ->
+  ?initialized:Options.DoInitialized.t ->
+  ?mem_access:Options.DoMemAccess.t ->
+  ?div_mod:Options.DoDivMod.t ->
+  ?shift:Options.DoShift.t ->
+  ?left_shift_negative:Kernel.LeftShiftNegative.t ->
+  ?right_shift_negative:Kernel.RightShiftNegative.t ->
+  ?signed_overflow:Kernel.SignedOverflow.t ->
+  ?unsigned_overflow:Kernel.UnsignedOverflow.t ->
+  ?signed_downcast:Kernel.SignedDowncast.t ->
+  ?unsigned_downcast:Kernel.UnsignedDowncast.t ->
+  ?float_to_int:Options.DoFloatToInt.t ->
+  ?finite_float:bool ->
+  ?pointer_call:Options.DoPointerCall.t ->
+  ?bool_value:Kernel.InvalidBool.t ->
+  (Cil_types.kinstr ->
+   ?status:Property_status.emitted_status -> Alarms.alarm -> unit) ->
+  Kernel_function.t ->
+  Cil_types.stmt ->
+  'a -> unit
+
+val iter_lval : lval generator
+val iter_exp : exp generator
+val iter_instr : instr generator
+val iter_stmt : stmt generator
+
 (** Generates RTE for a single function. Uses the status of the various
       RTE options do decide which kinds of annotations must be generated.
 *)