Frama-C API - Q
val name_arith_bop : Frama_c_kernel.Cil_types.binop -> stringname_of_mpz_arith_bop bop returns the name of the GMP rational function corresponding to the bop arithmetic operation.
Normalize the string so that it fits the representation used by the underlying real library. For example, "0.1" is a real number in ACSL whereas it is considered as a double by libgmp because it is written in decimal expansion. In order to make libgmp consider it to be a rational, it must be converted into "1/10".
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 a rational number.
val cast_to_z : loc:Frama_c_kernel.Cil_types.location -> ?name:string -> Env.t -> Frama_c_kernel.Cil_types.exp -> Frama_c_kernel.Cil_types.exp * Env.tAssumes that the given exp is of real type and casts it into Z
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 real 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.