sig   type model = Real | Float   val configure : Wp.Cfloat.model -> unit   val code_lit : float -> Wp.Lang.F.term   val acsl_lit : Cil_types.logic_real -> Wp.Lang.F.term   val real_of_int : Wp.Lang.F.unop   val float_of_int : Wp.Ctypes.c_float -> Wp.Lang.F.unop   val convert : 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 f_iabs : Wp.Lang.lfun   val f_rabs : Wp.Lang.lfun   val f_sqrt : Wp.Lang.lfun   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   val flt_sqrt : Wp.Ctypes.c_float -> Wp.Lang.lfun end