sig
  val get_data_scope_at_stmt :
    (Cil_types.kernel_function ->
     Cil_types.stmt ->
     Cil_types.lval ->
     Cil_datatype.Stmt.Hptset.t *
     (Cil_datatype.Stmt.Hptset.t * Cil_datatype.Stmt.Hptset.t))
    Pervasives.ref
  val get_prop_scope_at_stmt :
    (Cil_types.kernel_function ->
     Cil_types.stmt ->
     Cil_types.code_annotation ->
     Cil_datatype.Stmt.Hptset.t * Cil_types.code_annotation list)
    Pervasives.ref
  val check_asserts : (unit -> Cil_types.code_annotation list) Pervasives.ref
  val rm_asserts : (unit -> unit) Pervasives.ref
  val get_defs :
    (Cil_types.kernel_function ->
     Cil_types.stmt ->
     Cil_types.lval ->
     (Cil_datatype.Stmt.Hptset.t * Locations.Zone.t option) option)
    Pervasives.ref
  val get_defs_with_type :
    (Cil_types.kernel_function ->
     Cil_types.stmt ->
     Cil_types.lval ->
     ((bool * bool) Cil_datatype.Stmt.Map.t * Locations.Zone.t option) option)
    Pervasives.ref
  type t_zones = Locations.Zone.t Cil_datatype.Stmt.Hashtbl.t
  val build_zones :
    (Cil_types.kernel_function ->
     Cil_types.stmt ->
     Cil_types.lval -> Cil_datatype.Stmt.Hptset.t * Db.Scope.t_zones)
    Pervasives.ref
  val pretty_zones :
    (Format.formatter -> Db.Scope.t_zones -> unit) Pervasives.ref
  val get_zones :
    (Db.Scope.t_zones -> Cil_types.stmt -> Locations.Zone.t) Pervasives.ref
end