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