sig
  type t
  val empty :
    loc:Cil_types.location ->
    Cil_types.kernel_function -> Env.t -> Assert.t * Env.t
  val no_data : Assert.t
  val with_data_from :
    loc:Cil_types.location ->
    Cil_types.kernel_function -> Env.t -> Assert.t -> Assert.t * Env.t
  val merge_right :
    loc:Cil_types.location ->
    Env.t -> Assert.t -> Assert.t -> Assert.t * Env.t
  val clean : loc:Cil_types.location -> Env.t -> Assert.t -> Env.t
  val push_pending_register_data : unit -> unit
  val do_pending_register_data : Env.t -> Env.t
  val register :
    loc:Cil_types.location ->
    ?force:bool -> string -> Cil_types.exp -> Assert.t -> Assert.t
  val register_term :
    loc:Cil_types.location ->
    ?force:bool -> Cil_types.term -> Cil_types.exp -> Assert.t -> Assert.t
  val register_pred :
    loc:Cil_types.location ->
    Env.t ->
    ?force:bool ->
    Cil_types.predicate -> Cil_types.exp -> Assert.t -> Assert.t
  val register_pred_or_term :
    loc:Cil_types.location ->
    Env.t ->
    ?force:bool ->
    Analyses_types.pred_or_term -> Cil_types.exp -> Assert.t -> Assert.t
  val runtime_check :
    adata:Assert.t ->
    pred_kind:Cil_types.predicate_kind ->
    Analyses_types.annotation_kind ->
    Cil_types.kernel_function ->
    Env.t -> Cil_types.exp -> Cil_types.predicate -> Cil_types.stmt * Env.t
  val runtime_check_with_msg :
    adata:Assert.t ->
    loc:Cil_types.location ->
    ?name:string ->
    string ->
    pred_kind:Cil_types.predicate_kind ->
    Analyses_types.annotation_kind ->
    Cil_types.kernel_function ->
    Env.t -> Cil_types.exp -> Cil_types.stmt * Env.t
end