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 ->
Cil_types.kernel_function ->
Env.t -> Assert.t -> Assert.t -> Assert.t * Env.t
val clean :
loc:Cil_types.location ->
Cil_types.kernel_function -> Env.t -> Assert.t -> Env.t
val register :
loc:Cil_types.location ->
Cil_types.kernel_function ->
Env.t ->
?force:bool -> string -> Cil_types.exp -> Assert.t -> Assert.t * Env.t
val register_term :
loc:Cil_types.location ->
Cil_types.kernel_function ->
Env.t ->
?force:bool ->
Cil_types.term -> Cil_types.exp -> Assert.t -> Assert.t * Env.t
val register_pred :
loc:Cil_types.location ->
Cil_types.kernel_function ->
Env.t ->
?force:bool ->
Cil_types.predicate -> Cil_types.exp -> Assert.t -> Assert.t * Env.t
val runtime_check :
adata:Assert.t ->
pred_kind:Cil_types.predicate_kind ->
Smart_stmt.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 ->
string ->
pred_kind:Cil_types.predicate_kind ->
Smart_stmt.annotation_kind ->
Cil_types.kernel_function ->
Env.t -> Cil_types.exp -> Cil_types.stmt * Env.t
end