module Visit:sig
..end
Runtime Error annotation generation plugin
val annotate : ?flags:Flags.t -> Cil_types.kernel_function -> unit
Annotate kernel-function with respect to options and current generator status.
val get_annotations_kf : ?flags:Flags.t -> Cil_types.kernel_function -> Cil_types.code_annotation list
Returns annotations associated to alarms without registering them.
val get_annotations_stmt : ?flags:Flags.t ->
Cil_types.kernel_function -> Cil_types.stmt -> Cil_types.code_annotation list
Returns annotations associated to alarms without registering them.
val get_annotations_exp : ?flags:Flags.t ->
Cil_types.kernel_function ->
Cil_types.stmt -> Cil_types.exp -> Cil_types.code_annotation list
Returns annotations associated to alarms without registering them.
val get_annotations_lval : ?flags:Flags.t ->
Cil_types.kernel_function ->
Cil_types.stmt -> Cil_types.lval -> Cil_types.code_annotation list
Returns annotations associated to alarms without registering them.
RTE Iterators allow to traverse a Cil AST fragment (stmt, expr, l-value)
and reveal its potential Alarms. Each alarm will be presented to a callback
with type on_alarm
, that you can use in turn to generate an annotation
or perform any other treatment.
Flags can be used to select which alarm categories to visit, with defaults derived from Kernel and RTE plug-in parameters.
typeon_alarm =
Cil_types.kernel_function ->
Cil_types.stmt -> invalid:bool -> Alarms.alarm -> unit
Alarm callback.
The on_alarm kf stmt ~invalid alarm
callback is invoked on each
alarm visited by an RTE iterator, provided it fits the selected categories.
The kf
and stmt
designates the statement originating the alarm,
while ~invalid:true
is set when the alarm trivially evaluates to false.
In this later case, the corresponding annotation shall be assigned
the status False_if_reachable
.
type'a
iterator =?flags:Flags.t ->
on_alarm -> Kernel_function.t -> Cil_types.stmt -> 'a -> unit
Type of low-level iterators visiting an element 'a
of the AST
val iter_lval : Cil_types.lval iterator
val iter_exp : Cil_types.exp iterator
val iter_instr : Cil_types.instr iterator
val iter_stmt : Cil_types.stmt iterator
val status : invalid:bool -> Property_status.emitted_status option
Returns a False_if_reachable
status when invalid.
val register : Emitter.t ->
Cil_types.kernel_function ->
Cil_types.stmt ->
invalid:bool -> Alarms.alarm -> Cil_types.code_annotation * bool
Registers and returns the annotation associated with the alarm,
and a boolean flag indicating whether it has been freshly generated
or not. Simple wrapper over Alarms.register
.