Gmp.Z
val name_arith_bop : Frama_c_kernel.Cil_types.binop -> string
name_of_mpz_arith_bop bop
returns the name of the GMP integer function corresponding to the bop
arithmetic operation.
val new_var :
loc:Frama_c_kernel.Cil_types.location ->
?scope:Varname.scope ->
?name:string ->
Env.t ->
Frama_c_kernel.Cil_types.kernel_function ->
Frama_c_kernel.Cil_types.term option ->
(Frama_c_kernel.Cil_types.varinfo ->
Frama_c_kernel.Cil_types.exp ->
Frama_c_kernel.Cil_types.stmt list) ->
Frama_c_kernel.Cil_types.exp * Env.t
Same as Env.new_var
, but dedicated to mpz_t variables initialized by Mpz.init
.
val create :
loc:Frama_c_kernel.Cil_types.location ->
?name:string ->
Frama_c_kernel.Cil_types.term option ->
Env.t ->
Frama_c_kernel.Cil_types.kernel_function ->
Frama_c_kernel.Cil_types.exp ->
Frama_c_kernel.Cil_types.exp * Env.t
Create an integer number.
val add_cast :
loc:Frama_c_kernel.Cil_types.location ->
?name:string ->
Env.t ->
Frama_c_kernel.Cil_types.kernel_function ->
Frama_c_kernel.Cil_types.typ ->
Frama_c_kernel.Cil_types.exp ->
Frama_c_kernel.Cil_types.exp * Env.t
Assumes that the given exp is of integer type and casts it into the given typ
val binop :
loc:Frama_c_kernel.Cil_types.location ->
Frama_c_kernel.Cil_types.term option ->
Frama_c_kernel.Cil_types.binop ->
Env.t ->
Frama_c_kernel.Cil_types.kernel_function ->
Frama_c_kernel.Cil_types.exp ->
Frama_c_kernel.Cil_types.exp ->
Frama_c_kernel.Cil_types.exp * Env.t
Applies binop
to the given expressions. The optional term indicates whether the comparison has a correspondance in the logic.
val cmp :
loc:Frama_c_kernel.Cil_types.location ->
string ->
Frama_c_kernel.Cil_types.term option ->
Frama_c_kernel.Cil_types.binop ->
Env.t ->
Frama_c_kernel.Cil_types.kernel_function ->
Frama_c_kernel.Cil_types.exp ->
Frama_c_kernel.Cil_types.exp ->
Frama_c_kernel.Cil_types.exp * Env.t
Compares two expressions according to the given binop
. The optional term indicates whether the comparison has a correspondance in the logic.