Module Wp.Cfloat

module Cfloat: sig .. end

Floating Arithmetic Model

type model = 
| Real
| Float
val configure : model -> unit
val code_lit : float -> Wp.Lang.F.term
val acsl_lit : Cil_types.logic_real -> Wp.Lang.F.term
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 range : Wp.Ctypes.c_float -> Wp.Lang.F.term -> Wp.Lang.F.pred
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.Lang.lfun
val f_delta : Wp.Lang.lfun
val f_epsilon : Wp.Lang.lfun
val flt_rnd : 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