sig
val for_stmt :
Env.t -> Cil_types.kernel_function -> Cil_types.stmt -> Env.t
val to_exp :
loc:Cil_types.location ->
adata:Assert.t ->
Cil_types.kernel_function ->
Env.t ->
Analyses_types.pred_or_term ->
Cil_types.logic_label -> Cil_types.exp * Assert.t * Env.t
val reset : unit -> unit
module Malloc :
sig
val find_all : Cil_types.kernel_function -> Cil_types.stmt list
val remove_all : Cil_types.kernel_function -> unit
end
module Free :
sig
val find_all : Cil_types.kernel_function -> Cil_types.stmt list
val remove_all : Cil_types.kernel_function -> unit
end
val term_to_exp_ref :
(adata:Assert.t ->
?inplace:bool ->
Cil_types.kernel_function ->
Env.t -> Cil_types.term -> Cil_types.exp * Assert.t * Env.t)
Stdlib.ref
val predicate_to_exp_ref :
(adata:Assert.t ->
?inplace:bool ->
?name:string ->
Cil_types.kernel_function ->
?rte:bool ->
Env.t -> Cil_types.predicate -> Cil_types.exp * Assert.t * Env.t)
Stdlib.ref
end