Module Dynamic_plugins.RteGen

module RteGen: sig .. end

val do_all_rte : Cil_datatype.Kf.t -> unit

Generate all RTE annotations in the given function.

val stmt_annotations : Cil_datatype.Kf.t ->
Cil_datatype.Stmt.t -> Cil_datatype.Code_annotation.t list

Generate RTE annotations corresponding to the given stmt of the given function.

val exp_annotations : Cil_datatype.Kf.t ->
Cil_datatype.Stmt.t ->
Cil_datatype.Exp.t -> Cil_datatype.Code_annotation.t list

Generate RTE annotations corresponding to the given exp of the given stmt in the given function.

val emitter : Emitter.t

The emitter used for generating RTE annotations

val get_rte_annotations : Cil_datatype.Stmt.t -> Cil_datatype.Code_annotation.t list

Get the list of annotations previously emitted by RTE for the given statement.