Frama-C API - Z
val 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.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 correspondence 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 correspondence in the logic.