Gmp.Zval name_arith_bop : Frama_c_kernel.Cil_types.binop -> stringname_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.varinfo * Frama_c_kernel.Cil_types.exp * Env.tSame 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.tCreate 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.tAssumes 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.tApplies 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.tCompares two expressions according to the given binop. The optional term indicates whether the comparison has a correspondance in the logic.