sig
  val get_data_scope_at_stmt :
    Kernel_function.t ->
    Cil_types.stmt ->
    Cil_types.lval ->
    Cil_datatype.Stmt.Hptset.t *
    (Cil_datatype.Stmt.Hptset.t * Cil_datatype.Stmt.Hptset.t)
  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
  val check_asserts : unit -> Cil_types.code_annotation list
  val rm_asserts : unit -> unit
end