E_ACSL.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