module Visit:sig
..end
Runtime Error annotation generation plugin
val annotate_kf : Cil_types.kernel_function -> unit
val do_precond : Cil_types.kernel_function -> unit
val do_all_rte : Cil_types.kernel_function -> unit
val do_rte : Cil_types.kernel_function -> unit
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
-rte
option: computes
RTE on the whole AST. Which kind of RTE is generated depends on the
options given on the command line.