sig
  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 : Wp.Cfloat.model -> Wp.WpContext.rollback
  val ftau : Wp.Ctypes.c_float -> Wp.Lang.F.tau
  val tau_of_float : Wp.Ctypes.c_float -> Wp.Lang.F.tau
  type op =
      LT
    | EQ
    | LE
    | NE
    | NEG
    | ADD
    | SUB
    | MUL
    | DIV
    | REAL
    | ROUND
    | EXACT
  val find : Wp.Lang.lfun -> Wp.Cfloat.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
  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
end