Memory_translate (frama-c-e-acsl.E_ACSL.Memory

val call : 
  loc:Frama_c_kernel.Cil_types.location ->
  Frama_c_kernel.Cil_types.kernel_function ->
  string ->
  Frama_c_kernel.Cil_types.typ ->
  Env.t ->
  Frama_c_kernel.Cil_types.exp list ->
  Frama_c_kernel.Cil_types.exp * Env.t

val call_with_size : 
  adata:Assert.t ->
  loc:Frama_c_kernel.Cil_types.location ->
  Frama_c_kernel.Cil_types.kernel_function ->
  string ->
  Frama_c_kernel.Cil_types.typ ->
  Env.t ->
  Frama_c_kernel.Cil_types.term list ->
  Frama_c_kernel.Cil_types.predicate ->
  Frama_c_kernel.Cil_types.exp * Assert.t * Env.t

val call_valid : 
  adata:Assert.t ->
  loc:Frama_c_kernel.Cil_types.location ->
  Frama_c_kernel.Cil_types.kernel_function ->
  string ->
  Frama_c_kernel.Cil_types.typ ->
  Env.t ->
  Frama_c_kernel.Cil_types.term ->
  Frama_c_kernel.Cil_types.predicate ->
  Frama_c_kernel.Cil_types.exp * Assert.t * Env.t

val predicate_to_exp_ref : 
  (adata:Assert.t ->
    Frama_c_kernel.Cil_types.kernel_function ->
    Env.t ->
    Frama_c_kernel.Cil_types.predicate ->
    Frama_c_kernel.Cil_types.exp * Assert.t * Env.t)
    Stdlib.ref

module Translate_terms : sig ... end

val gmp_to_sizet_ref : 
  (adata:Assert.t ->
    loc:Frama_c_kernel.Cil_types.location ->
    name:string ->
    ?check_lower_bound:bool ->
    ?pp:Frama_c_kernel.Cil_types.term ->
    Frama_c_kernel.Cil_types.kernel_function ->
    Env.t ->
    Frama_c_kernel.Cil_types.term ->
    Frama_c_kernel.Cil_types.exp * Assert.t * Env.t)
    Stdlib.ref