diff --git a/src/plugins/rte/RteGen.mli b/src/plugins/rte/RteGen.mli index 9926f78e4a0920cb8cc90aa4c4082d8b86e8dad7..bd2f3ac38d51ba56733598f5708b949fcbcd64cc 100644 --- a/src/plugins/rte/RteGen.mli +++ b/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 diff --git a/src/plugins/rte/visit.ml b/src/plugins/rte/visit.ml index 869f57889865bba6ee633d16fc9cf13246127f4f..7b28afc6cd8c16fab08c89b5d9d6a138baac0840 100644 --- a/src/plugins/rte/visit.ml +++ b/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 = diff --git a/src/plugins/rte/visit.mli b/src/plugins/rte/visit.mli index 1413e3b8f7bf3411f312dd1401f8664fa1c4d521..4dc723cc58c2f82e073fde39fcef262376f54ac3 100644 --- a/src/plugins/rte/visit.mli +++ b/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. *)