Module Db.RteGen

module RteGen: sig .. end

Runtime Error Annotation Generation plugin.

val compute : (unit -> unit) Stdlib.ref

Same result as having -rte on the command line

val annotate_kf : (Cil_types.kernel_function -> unit) Stdlib.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_all_rte : (Cil_types.kernel_function -> unit) Stdlib.ref

Generates all possible RTE for a given function.

val do_rte : (Cil_types.kernel_function -> unit) Stdlib.ref

Generates all possible RTE except pre-conditions for a given function.

val self : State.t Stdlib.ref

type status_accessor = string * (Cil_types.kernel_function -> bool -> unit) *
       (Cil_types.kernel_function -> bool)

val get_all_status : (unit -> status_accessor list) Stdlib.ref

val get_divMod_status : (unit -> status_accessor) Stdlib.ref

val get_initialized_status : (unit -> status_accessor) Stdlib.ref

val get_memAccess_status : (unit -> status_accessor) Stdlib.ref

val get_pointerCall_status : (unit -> status_accessor) Stdlib.ref

val get_signedOv_status : (unit -> status_accessor) Stdlib.ref

val get_signed_downCast_status : (unit -> status_accessor) Stdlib.ref

val get_unsignedOv_status : (unit -> status_accessor) Stdlib.ref

val get_unsignedDownCast_status : (unit -> status_accessor) Stdlib.ref

val get_pointer_downcast_status : (unit -> status_accessor) Stdlib.ref

val get_float_to_int_status : (unit -> status_accessor) Stdlib.ref

val get_finite_float_status : (unit -> status_accessor) Stdlib.ref

val get_pointer_value_status : (unit -> status_accessor) Stdlib.ref

val get_bool_value_status : (unit -> status_accessor) Stdlib.ref