Module Visit

module Visit: sig .. end

Generates RTE for a single function. Uses the status of the various RTE options do decide which kinds of annotations must be generated.

Runtime Error annotation generation plugin

val annotate_kf : Cil_types.kernel_function -> unit

Generates RTE for a single function. Uses the status of the various RTE options do decide which kinds of annotations must be generated.

val do_precond : Cil_types.kernel_function -> unit

Generates preconditions RTE for a given function.

val do_all_rte : Cil_types.kernel_function -> unit

Generates all RTEs for a given function.

val do_rte : Cil_types.kernel_function -> unit

Generates all RTEs except preconditions for a given function.

val rte_annotations : Cil_types.stmt -> Cil_types.code_annotation list

val do_stmt_annotations : Cil_types.kernel_function -> Cil_types.stmt -> Cil_types.code_annotation list

val do_exp_annotations : Cil_types.kernel_function ->
       Cil_types.stmt -> Cil_types.exp -> Cil_types.code_annotation list

val compute : unit -> unit

Main entry point of the plug-in, used by -rte option: computes RTE on the whole AST. Which kind of RTE is generated depends on the options given on the command line.