Module Memory_translate

module Memory_translate: sig .. end

val call : loc:Cil_types.location ->
Cil_types.kernel_function ->
string -> Cil_types.typ -> Env.t -> Cil_types.term -> Cil_types.exp * Env.t
val call_with_size : loc:Cil_types.location ->
Cil_types.kernel_function ->
string ->
Cil_types.typ ->
Env.t -> Cil_types.term list -> Cil_types.predicate -> Cil_types.exp * Env.t
val call_valid : loc:Cil_types.location ->
Cil_types.kernel_function ->
string ->
Cil_types.typ ->
Env.t -> Cil_types.term -> Cil_types.predicate -> Cil_types.exp * Env.t
val predicate_to_exp_ref : (Cil_types.kernel_function ->
Env.t -> Cil_types.predicate -> Cil_types.exp * Env.t)
Stdlib.ref
val term_to_exp_ref : (Cil_types.kernel_function ->
Env.t -> Cil_types.term -> Cil_types.exp * Env.t)
Stdlib.ref