Module Rational

module Rational: sig .. end
Generation of rational numbers.

val create : loc:Cil_types.location ->
?name:string ->
Cil_types.exp ->
Env.t ->
Cil_types.kernel_function -> Cil_types.term option -> Cil_types.exp * Env.t
Create a real
val init_set : loc:Cil_types.location ->
Cil_types.lval -> Cil_types.exp -> Cil_types.exp -> Cil_types.stmt
init_set lval lval_as_exp exp sets lval to exp while guranteeing that lval is properly initialized wrt the underlying real library.
val normalize_str : string -> string
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:Cil_types.location ->
?name:string -> Cil_types.exp -> Env.t -> Cil_types.exp * Env.t
Assumes that the given exp is of real type and casts it into Z
val add_cast : loc:Cil_types.location ->
?name:string ->
Cil_types.exp ->
Env.t -> Cil_types.kernel_function -> Cil_types.typ -> Cil_types.exp * Env.t
Assumes that the given exp is of real type and casts it into the given typ
val binop : loc:Cil_types.location ->
Cil_types.binop ->
Cil_types.exp ->
Cil_types.exp ->
Env.t ->
Cil_types.kernel_function -> Cil_types.term option -> 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:Cil_types.location ->
Cil_types.binop ->
Cil_types.exp ->
Cil_types.exp ->
Env.t ->
Cil_types.kernel_function -> Cil_types.term option -> 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.