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.