Module Wp.Cfloat

module Cfloat: sig .. end


Floating Arithmetic Model
val f32 : Wp.Lang.adt
val f64 : Wp.Lang.adt
val t32 : Wp.Lang.F.tau
val t64 : Wp.Lang.F.tau
val fq32 : Wp.Lang.lfun
val fq64 : Wp.Lang.lfun
type model = 
| Real
| Float
val configure : model -> Wp.WpContext.rollback
val ftau : Wp.Ctypes.c_float -> Wp.Lang.F.tau
model independant
val tau_of_float : Wp.Ctypes.c_float -> Wp.Lang.F.tau
with respect to model
type op = 
| LT
| EQ
| LE
| NE
| NEG
| ADD
| SUB
| MUL
| DIV
| REAL
| ROUND
| EXACT (*
same as round, but argument is exact representation
*)
val find : Wp.Lang.lfun -> op * Wp.Ctypes.c_float
val code_lit : Wp.Ctypes.c_float -> float -> string option -> Wp.Lang.F.term
val acsl_lit : Cil_types.logic_real -> Wp.Lang.F.term
val float_lit : Wp.Ctypes.c_float -> Q.t -> string
Returns a string literal in decimal notation (without suffix) that reparses to the same value (when added suffix).
val float_of_int : Wp.Ctypes.c_float -> Wp.Lang.F.unop
val float_of_real : Wp.Ctypes.c_float -> Wp.Lang.F.unop
val real_of_float : Wp.Ctypes.c_float -> Wp.Lang.F.unop
val fopp : Wp.Ctypes.c_float -> Wp.Lang.F.unop
val fadd : Wp.Ctypes.c_float -> Wp.Lang.F.binop
val fsub : Wp.Ctypes.c_float -> Wp.Lang.F.binop
val fmul : Wp.Ctypes.c_float -> Wp.Lang.F.binop
val fdiv : Wp.Ctypes.c_float -> Wp.Lang.F.binop
val flt : Wp.Ctypes.c_float -> Wp.Lang.F.cmp
val fle : Wp.Ctypes.c_float -> Wp.Lang.F.cmp
val feq : Wp.Ctypes.c_float -> Wp.Lang.F.cmp
val fneq : Wp.Ctypes.c_float -> Wp.Lang.F.cmp
val f_model : Wp.Ctypes.c_float -> Wp.Lang.lfun
val f_delta : Wp.Ctypes.c_float -> Wp.Lang.lfun
val f_epsilon : Wp.Ctypes.c_float -> Wp.Lang.lfun
val flt_of_real : Wp.Ctypes.c_float -> Wp.Lang.lfun
val real_of_flt : Wp.Ctypes.c_float -> Wp.Lang.lfun
val flt_add : Wp.Ctypes.c_float -> Wp.Lang.lfun
val flt_mul : Wp.Ctypes.c_float -> Wp.Lang.lfun
val flt_div : Wp.Ctypes.c_float -> Wp.Lang.lfun
val flt_neg : Wp.Ctypes.c_float -> Wp.Lang.lfun