sig
  val compute : (unit -> unit) Stdlib.ref
  val annotate_kf : (Cil_types.kernel_function -> unit) Stdlib.ref
  val do_all_rte : (Cil_types.kernel_function -> unit) Stdlib.ref
  val do_rte : (Cil_types.kernel_function -> unit) Stdlib.ref
  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 -> Db.RteGen.status_accessor list) Stdlib.ref
  val get_divMod_status : (unit -> Db.RteGen.status_accessor) Stdlib.ref
  val get_initialized_status : (unit -> Db.RteGen.status_accessor) Stdlib.ref
  val get_memAccess_status : (unit -> Db.RteGen.status_accessor) Stdlib.ref
  val get_pointerCall_status : (unit -> Db.RteGen.status_accessor) Stdlib.ref
  val get_signedOv_status : (unit -> Db.RteGen.status_accessor) Stdlib.ref
  val get_signed_downCast_status :
    (unit -> Db.RteGen.status_accessor) Stdlib.ref
  val get_unsignedOv_status : (unit -> Db.RteGen.status_accessor) Stdlib.ref
  val get_unsignedDownCast_status :
    (unit -> Db.RteGen.status_accessor) Stdlib.ref
  val get_pointer_downcast_status :
    (unit -> Db.RteGen.status_accessor) Stdlib.ref
  val get_float_to_int_status :
    (unit -> Db.RteGen.status_accessor) Stdlib.ref
  val get_finite_float_status :
    (unit -> Db.RteGen.status_accessor) Stdlib.ref
  val get_pointer_value_status :
    (unit -> Db.RteGen.status_accessor) Stdlib.ref
  val get_bool_value_status : (unit -> Db.RteGen.status_accessor) Stdlib.ref
end