module Memory_translate: sig
.. end
val call : adata:Assert.t ->
loc:Cil_types.location ->
Cil_types.kernel_function ->
string ->
Cil_types.typ -> Env.t -> Cil_types.term -> Cil_types.exp * Assert.t * Env.t
val call_with_size : adata:Assert.t ->
loc:Cil_types.location ->
Cil_types.kernel_function ->
string ->
Cil_types.typ ->
Env.t ->
Cil_types.term list ->
Cil_types.predicate -> Cil_types.exp * Assert.t * Env.t
val call_valid : adata:Assert.t ->
loc:Cil_types.location ->
Cil_types.kernel_function ->
string ->
Cil_types.typ ->
Env.t ->
Cil_types.term -> Cil_types.predicate -> Cil_types.exp * Assert.t * Env.t
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
val gmp_to_sizet_ref : (adata:Assert.t ->
loc:Cil_types.location ->
name:string ->
?check_lower_bound:bool ->
?pp:Cil_types.term ->
Cil_types.kernel_function ->
Env.t -> Cil_types.term -> Cil_types.exp * Assert.t * Env.t)
Stdlib.ref