sig
val reset : unit -> unit
val app_to_exp :
adata:Assert.t ->
loc:Cil_types.location ->
?tapp:Cil_types.term ->
Cil_types.kernel_function ->
Env.t ->
?eargs:Cil_types.exp list ->
Cil_types.logic_info ->
Cil_types.term list -> Cil_types.exp * Assert.t * Env.t
val add_generated_functions :
Cil_types.global list -> Cil_types.global list
val predicate_to_exp_ref :
(adata:Assert.t ->
Cil_types.kernel_function ->
Env.t -> Cil_types.predicate -> Cil_types.exp * Assert.t * Env.t)
Stdlib.ref
val term_to_exp_ref :
(adata:Assert.t ->
Cil_types.kernel_function ->
Env.t -> Cil_types.term -> Cil_types.exp * Assert.t * Env.t)
Stdlib.ref
end