sig
  val of_real : Wp.Ctypes.c_int -> Wp.Lang.F.unop
  val iconvert : Wp.Ctypes.c_int -> Wp.Lang.F.unop
  val irange : Wp.Ctypes.c_int -> Wp.Lang.F.term -> Wp.Lang.F.pred
  val to_cint : Wp.Lang.lfun -> Wp.Ctypes.c_int
  val is_cint : Wp.Lang.lfun -> Wp.Ctypes.c_int
  type model = NoRange | Natural | Machine
  val configure : Wp.Cint.model -> unit
  val iopp : Wp.Ctypes.c_int -> Wp.Lang.F.unop
  val iadd : Wp.Ctypes.c_int -> Wp.Lang.F.binop
  val isub : Wp.Ctypes.c_int -> Wp.Lang.F.binop
  val imul : Wp.Ctypes.c_int -> Wp.Lang.F.binop
  val idiv : Wp.Ctypes.c_int -> Wp.Lang.F.binop
  val imod : Wp.Ctypes.c_int -> Wp.Lang.F.binop
  val bnot : Wp.Ctypes.c_int -> Wp.Lang.F.unop
  val band : Wp.Ctypes.c_int -> Wp.Lang.F.binop
  val bxor : Wp.Ctypes.c_int -> Wp.Lang.F.binop
  val bor : Wp.Ctypes.c_int -> Wp.Lang.F.binop
  val blsl : Wp.Ctypes.c_int -> Wp.Lang.F.binop
  val blsr : Wp.Ctypes.c_int -> Wp.Lang.F.binop
  val l_not : Wp.Lang.F.unop
  val l_and : Wp.Lang.F.binop
  val l_xor : Wp.Lang.F.binop
  val l_or : Wp.Lang.F.binop
  val l_lsl : Wp.Lang.F.binop
  val l_lsr : Wp.Lang.F.binop
  val f_lnot : Wp.Lang.lfun
  val f_land : Wp.Lang.lfun
  val f_lxor : Wp.Lang.lfun
  val f_lor : Wp.Lang.lfun
  val f_lsl : Wp.Lang.lfun
  val f_lsr : Wp.Lang.lfun
  val f_bit : Wp.Lang.lfun
  val is_cint_simplifier : Wp.Conditions.simplifier
  val is_positive_or_null : Wp.Lang.F.term -> bool
end