sig   val compute : (unit -> unit) Pervasives.ref   val annotate_kf : (Cil_types.kernel_function -> unit) Pervasives.ref   val self : State.t Pervasives.ref   val do_precond : (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   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_precond_status : (unit -> Db.RteGen.status_accessor) Pervasives.ref   val get_divMod_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 end