sig
val compute : (unit -> unit) Pervasives.ref
val annotate_kf : (Cil_types.kernel_function -> unit) Pervasives.ref
val do_all_rte : (Cil_types.kernel_function -> unit) Pervasives.ref
val do_rte : (Cil_types.kernel_function -> unit) Pervasives.ref
val self : State.t Pervasives.ref
type status_accessor =
string * (Cil_types.kernel_function -> bool -> unit) *
(Cil_types.kernel_function -> bool)
val get_all_status :
(unit -> Db.RteGen.status_accessor list) Pervasives.ref
val get_divMod_status : (unit -> Db.RteGen.status_accessor) Pervasives.ref
val get_initialized_status :
(unit -> Db.RteGen.status_accessor) Pervasives.ref
val get_memAccess_status :
(unit -> Db.RteGen.status_accessor) Pervasives.ref
val get_pointerCall_status :
(unit -> Db.RteGen.status_accessor) Pervasives.ref
val get_signedOv_status :
(unit -> Db.RteGen.status_accessor) Pervasives.ref
val get_signed_downCast_status :
(unit -> Db.RteGen.status_accessor) Pervasives.ref
val get_unsignedOv_status :
(unit -> Db.RteGen.status_accessor) Pervasives.ref
val get_unsignedDownCast_status :
(unit -> Db.RteGen.status_accessor) Pervasives.ref
val get_float_to_int_status :
(unit -> Db.RteGen.status_accessor) Pervasives.ref
val get_finite_float_status :
(unit -> Db.RteGen.status_accessor) Pervasives.ref
val get_bool_value_status :
(unit -> Db.RteGen.status_accessor) Pervasives.ref
end