E_ACSL.Rational
Generation of rational numbers.
val create :
loc:Frama_c_kernel.Cil_types.location ->
?name:string ->
Frama_c_kernel.Cil_types.exp ->
Env.t ->
Frama_c_kernel.Cil_types.kernel_function ->
Frama_c_kernel.Cil_types.term option ->
Frama_c_kernel.Cil_types.exp * Env.t
Create a real
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 cast_to_z :
loc:Frama_c_kernel.Cil_types.location ->
?name:string ->
Frama_c_kernel.Cil_types.exp ->
Env.t ->
Frama_c_kernel.Cil_types.exp * Env.t
Assumes 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 ->
Frama_c_kernel.Cil_types.exp ->
Env.t ->
Frama_c_kernel.Cil_types.kernel_function ->
Frama_c_kernel.Cil_types.typ ->
Frama_c_kernel.Cil_types.exp * Env.t
Assumes 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.binop ->
Frama_c_kernel.Cil_types.exp ->
Frama_c_kernel.Cil_types.exp ->
Env.t ->
Frama_c_kernel.Cil_types.kernel_function ->
Frama_c_kernel.Cil_types.term option ->
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 ->
Frama_c_kernel.Cil_types.binop ->
Frama_c_kernel.Cil_types.exp ->
Frama_c_kernel.Cil_types.exp ->
Env.t ->
Frama_c_kernel.Cil_types.kernel_function ->
Frama_c_kernel.Cil_types.term option ->
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.