module RteGen:sig
..end
val do_all_rte : Cil_datatype.Kf.t -> unit
Generate all RTE annotations in the given function.
Dynamic.get ~plugin:"RteGen" "do_all_rte" (Datatype.func Kernel_function.ty Datatype.unit)
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.
Dynamic.get ~plugin:"RteGen" "stmt_annotations" (Datatype.func Kernel_function.ty (Datatype.func Cil_datatype.Stmt.ty (Datatype.list Cil_datatype.Code_annotation.ty)))
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.
Dynamic.get ~plugin:"RteGen" "exp_annotations" (Datatype.func Kernel_function.ty (Datatype.func Cil_datatype.Stmt.ty (Datatype.func Cil_datatype.Exp.ty (Datatype.list Cil_datatype.Code_annotation.ty))))
val emitter : Emitter.t
The emitter used for generating RTE annotations
Dynamic.get ~plugin:"RteGen" "emitter" (Emitter.ty)
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.
Dynamic.get ~plugin:"RteGen" "get_rte_annotations" (Datatype.func Cil_datatype.Stmt.ty (Datatype.list Cil_datatype.Code_annotation.ty))