sig
type round = Up | Down | Near | Zero
type prec = Single | Double | Long_Double | Real
module type Widen_Hints =
sig
type elt = Cil_datatype.Logic_real.t
type t
val empty : t
val is_empty : t -> bool
val mem : elt -> t -> bool
val add : elt -> t -> t
val singleton : elt -> t
val remove : elt -> t -> t
val union : t -> t -> t
val inter : t -> t -> t
val disjoint : t -> t -> bool
val diff : t -> t -> t
val subset : t -> t -> bool
val iter : (elt -> unit) -> t -> unit
val map : (elt -> elt) -> t -> t
val fold : (elt -> 'a -> 'a) -> t -> 'a -> 'a
val for_all : (elt -> bool) -> t -> bool
val exists : (elt -> bool) -> t -> bool
val filter : (elt -> bool) -> t -> t
val filter_map : (elt -> elt option) -> t -> t
val partition : (elt -> bool) -> t -> t * t
val cardinal : t -> int
val elements : t -> elt list
val min_elt : t -> elt
val min_elt_opt : t -> elt option
val max_elt : t -> elt
val max_elt_opt : t -> elt option
val choose : t -> elt
val choose_opt : t -> elt option
val split : elt -> t -> t * bool * t
val find : elt -> t -> elt
val find_opt : elt -> t -> elt option
val find_first : (elt -> bool) -> t -> elt
val find_first_opt : (elt -> bool) -> t -> elt option
val find_last : (elt -> bool) -> t -> elt
val find_last_opt : (elt -> bool) -> t -> elt option
val of_list : elt list -> t
val to_seq_from : elt -> t -> elt Seq.t
val to_seq : t -> elt Seq.t
val add_seq : elt Seq.t -> t -> t
val of_seq : elt Seq.t -> t
val nearest_elt_le : elt -> t -> elt
val nearest_elt_ge : elt -> t -> elt
val ty : t Type.t
val name : string
val descr : t Descr.t
val packed_descr : Structural_descr.pack
val reprs : t list
val equal : t -> t -> bool
val compare : t -> t -> int
val hash : t -> int
val pretty_code : Format.formatter -> t -> unit
val internal_pretty_code :
Type.precedence -> Format.formatter -> t -> unit
val pretty : Format.formatter -> t -> unit
val varname : t -> string
val mem_project : (Project_skeleton.t -> bool) -> t -> bool
val copy : t -> t
val default_widen_hints : t
end
module type S =
sig
type t
val packed_descr : Structural_descr.pack
val hash : Float_sig.S.t -> int
val pretty : Stdlib.Format.formatter -> Float_sig.S.t -> unit
val is_exact : Float_sig.prec -> bool
val of_float :
Float_sig.round -> Float_sig.prec -> float -> Float_sig.S.t
val to_float : Float_sig.S.t -> float
val cmp_ieee : Float_sig.S.t -> Float_sig.S.t -> int
val compare : Float_sig.S.t -> Float_sig.S.t -> int
val is_nan : Float_sig.S.t -> bool
val is_finite : Float_sig.S.t -> bool
val is_infinite : Float_sig.S.t -> bool
val is_negative : Float_sig.S.t -> bool
val round_to_precision :
Float_sig.round -> Float_sig.prec -> Float_sig.S.t -> Float_sig.S.t
val next_float : Float_sig.prec -> Float_sig.S.t -> Float_sig.S.t
val prev_float : Float_sig.prec -> Float_sig.S.t -> Float_sig.S.t
module Widen_Hints : Widen_Hints
type widen_hints = Float_sig.Widen_Hints.t
val widen_up :
Float_sig.S.widen_hints ->
Float_sig.prec -> Float_sig.S.t -> Float_sig.S.t
val widen_down :
Float_sig.S.widen_hints ->
Float_sig.prec -> Float_sig.S.t -> Float_sig.S.t
val neg : Float_sig.S.t -> Float_sig.S.t
val abs : Float_sig.S.t -> Float_sig.S.t
val floor : Float_sig.S.t -> Float_sig.S.t
val ceil : Float_sig.S.t -> Float_sig.S.t
val trunc : Float_sig.S.t -> Float_sig.S.t
val fround : Float_sig.S.t -> Float_sig.S.t
val add :
Float_sig.round ->
Float_sig.prec -> Float_sig.S.t -> Float_sig.S.t -> Float_sig.S.t
val sub :
Float_sig.round ->
Float_sig.prec -> Float_sig.S.t -> Float_sig.S.t -> Float_sig.S.t
val mul :
Float_sig.round ->
Float_sig.prec -> Float_sig.S.t -> Float_sig.S.t -> Float_sig.S.t
val div :
Float_sig.round ->
Float_sig.prec -> Float_sig.S.t -> Float_sig.S.t -> Float_sig.S.t
val fmod :
Float_sig.round ->
Float_sig.prec -> Float_sig.S.t -> Float_sig.S.t -> Float_sig.S.t
val exp :
Float_sig.round -> Float_sig.prec -> Float_sig.S.t -> Float_sig.S.t
val log :
Float_sig.round -> Float_sig.prec -> Float_sig.S.t -> Float_sig.S.t
val log10 :
Float_sig.round -> Float_sig.prec -> Float_sig.S.t -> Float_sig.S.t
val sqrt :
Float_sig.round -> Float_sig.prec -> Float_sig.S.t -> Float_sig.S.t
val pow :
Float_sig.round ->
Float_sig.prec -> Float_sig.S.t -> Float_sig.S.t -> Float_sig.S.t
val cos :
Float_sig.round -> Float_sig.prec -> Float_sig.S.t -> Float_sig.S.t
val sin :
Float_sig.round -> Float_sig.prec -> Float_sig.S.t -> Float_sig.S.t
val acos :
Float_sig.round -> Float_sig.prec -> Float_sig.S.t -> Float_sig.S.t
val asin :
Float_sig.round -> Float_sig.prec -> Float_sig.S.t -> Float_sig.S.t
val atan :
Float_sig.round -> Float_sig.prec -> Float_sig.S.t -> Float_sig.S.t
val atan2 :
Float_sig.round ->
Float_sig.prec -> Float_sig.S.t -> Float_sig.S.t -> Float_sig.S.t
end
end