module RteGen:sig
..end
Runtime Error Annotation Generation plugin.
val compute : (unit -> unit) Pervasives.ref
Same result as having -rte
on the command line
val annotate_kf : (Cil_types.kernel_function -> unit) Pervasives.ref
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) Pervasives.ref
Only generates precond RTE for a given function
(see -rte-precond
for more information).
val do_all_rte : (Cil_types.kernel_function -> unit) Pervasives.ref
Generates all possible RTE for a given function.
val do_rte : (Cil_types.kernel_function -> unit) Pervasives.ref
Generates all possible RTE except pre-conditions for a given function.
val self : State.t Pervasives.ref
typestatus_accessor =
string * (Cil_types.kernel_function -> bool -> unit) *
(Cil_types.kernel_function -> bool)
val get_all_status : (unit -> status_accessor list) Pervasives.ref
val get_precond_status : (unit -> status_accessor) Pervasives.ref
val get_divMod_status : (unit -> status_accessor) Pervasives.ref
val get_initialized_status : (unit -> status_accessor) Pervasives.ref
val get_memAccess_status : (unit -> status_accessor) Pervasives.ref
val get_pointerCall_status : (unit -> status_accessor) Pervasives.ref
val get_signedOv_status : (unit -> status_accessor) Pervasives.ref
val get_signed_downCast_status : (unit -> status_accessor) Pervasives.ref
val get_unsignedOv_status : (unit -> status_accessor) Pervasives.ref
val get_unsignedDownCast_status : (unit -> status_accessor) Pervasives.ref
val get_float_to_int_status : (unit -> status_accessor) Pervasives.ref
val get_finite_float_status : (unit -> status_accessor) Pervasives.ref