Frama-C API - Memory_translate
val call : 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.exp * Assert.t * 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
val term_to_exp_ref : (adata:Assert.t -> 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
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