module Visit:sig
..end
Runtime Error annotation generation plugin
val annotate : ?flags:Flags.t -> Cil_types.kernel_function -> unit
val get_annotations_kf : ?flags:Flags.t -> Cil_types.kernel_function -> Cil_types.code_annotation list
val get_annotations_stmt : ?flags:Flags.t ->
Cil_types.kernel_function -> Cil_types.stmt -> Cil_types.code_annotation list
val get_annotations_exp : ?flags:Flags.t ->
Cil_types.kernel_function ->
Cil_types.stmt -> Cil_types.exp -> Cil_types.code_annotation list
val get_annotations_lval : ?flags:Flags.t ->
Cil_types.kernel_function ->
Cil_types.stmt -> Cil_types.lval -> Cil_types.code_annotation list
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
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
'a
of the ASTval 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
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
Alarms.register
.