Module Visit

module Visit: sig .. end

RTE Generator API

Runtime Error annotation generation plugin



RTE Generator API


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.

Low-Level RTE Iterators

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.

type on_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

Alarm Helpers


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.