sig
module F :
sig
type t
val packed_descr : Structural_descr.pack
val of_float : float -> Fval.F.t
val to_float : Fval.F.t -> float
val compare : Fval.F.t -> Fval.F.t -> int
val equal : Fval.F.t -> Fval.F.t -> bool
val pretty : Format.formatter -> Fval.F.t -> unit
val pretty_normal :
use_hex:bool -> Format.formatter -> Fval.F.t -> unit
val zero : Fval.F.t
val next_float : float -> float
val prev_float : float -> float
end
type t
val packed_descr : Structural_descr.pack
exception Non_finite
type rounding_mode = Any | Nearest_Even
val top_single_precision_float : Fval.t
val round_to_single_precision_float :
rounding_mode:Fval.rounding_mode -> Fval.t -> bool * Fval.t
val bits_of_float64 :
signed:bool -> Fval.t -> Abstract_interp.Int.t * Abstract_interp.Int.t
val bits_of_float32 :
signed:bool -> Fval.t -> Abstract_interp.Int.t * Abstract_interp.Int.t
val has_finite : Fval.t -> bool
type builtin_alarm = APosInf | ANegInf | ANaN of string | AAssume of string
module Builtin_alarms :
sig
type elt = builtin_alarm
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 diff : t -> t -> t
val compare : t -> t -> int
val equal : t -> t -> bool
val subset : t -> t -> bool
val iter : (elt -> unit) -> t -> unit
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 partition : (elt -> bool) -> t -> t * t
val cardinal : t -> int
val elements : t -> elt list
val min_elt : t -> elt
val max_elt : t -> elt
val choose : t -> elt
val split : elt -> t -> t * bool * t
val find : elt -> t -> elt
val of_list : elt list -> t
end
type builtin_res = Fval.Builtin_alarms.t * Fval.t Bottom.or_bottom
type float_kind = Float32 | Float64
val next_after : Fval.float_kind -> Fval.F.t -> Fval.F.t -> Fval.F.t
val inject : Fval.F.t -> Fval.F.t -> Fval.t
val inject_r_f :
Fval.float_kind -> Fval.F.t -> Fval.F.t -> bool * bool * Fval.t
val inject_r : Fval.F.t -> Fval.F.t -> bool * Fval.t
val inject_f : Fval.float_kind -> Fval.F.t -> Fval.F.t -> Fval.t
val inject_singleton : Fval.F.t -> Fval.t
val compare_min : Fval.t -> Fval.t -> int
val compare_max : Fval.t -> Fval.t -> int
val min_and_max : Fval.t -> Fval.F.t * Fval.F.t
val top : Fval.t
val add : Fval.rounding_mode -> Fval.t -> Fval.t -> bool * Fval.t
val sub : Fval.rounding_mode -> Fval.t -> Fval.t -> bool * Fval.t
val mul : Fval.rounding_mode -> Fval.t -> Fval.t -> bool * Fval.t
val div : Fval.rounding_mode -> Fval.t -> Fval.t -> bool * Fval.t
val is_a_zero : Fval.t -> bool
val contains_zero : Fval.t -> bool
val compare : Fval.t -> Fval.t -> int
val pretty : Format.formatter -> Fval.t -> unit
val pretty_overflow : Format.formatter -> Fval.t -> unit
val hash : Fval.t -> int
val zero : Fval.t
val minus_zero : Fval.t
val zeros : Fval.t
val is_zero : Fval.t -> bool
val is_included : Fval.t -> Fval.t -> bool
val join : Fval.t -> Fval.t -> Fval.t
val meet : Fval.t -> Fval.t -> Fval.t Bottom.or_bottom
val narrow : Fval.t -> Fval.t -> Fval.t Bottom.or_bottom
val contains_a_zero : Fval.t -> bool
val is_singleton : Fval.t -> bool
exception Not_Singleton_Float
val project_float : Fval.t -> Fval.F.t
val minus_one_one : Fval.t
val subdiv_float_interval :
size:Fval.float_kind option -> Fval.t -> Fval.t * Fval.t
val neg : Fval.t -> Fval.t
val cos : Fval.t -> Fval.t
val sin : Fval.t -> Fval.t
val atan2 : Fval.t -> Fval.t -> Fval.builtin_res
val pow : Fval.t -> Fval.t -> Fval.builtin_res
val powf : Fval.t -> Fval.t -> Fval.builtin_res
val fmod : Fval.t -> Fval.t -> Fval.builtin_res
val sqrt : Fval.rounding_mode -> Fval.t -> Fval.builtin_res
val exp : Fval.rounding_mode -> Fval.t -> Fval.Builtin_alarms.t * Fval.t
val log : Fval.rounding_mode -> Fval.t -> Fval.builtin_res
val log10 : Fval.rounding_mode -> Fval.t -> Fval.builtin_res
val floor : Fval.rounding_mode -> Fval.t -> Fval.Builtin_alarms.t * Fval.t
val ceil : Fval.rounding_mode -> Fval.t -> Fval.Builtin_alarms.t * Fval.t
val trunc : Fval.rounding_mode -> Fval.t -> Fval.Builtin_alarms.t * Fval.t
val fround : Fval.rounding_mode -> Fval.t -> Fval.Builtin_alarms.t * Fval.t
val expf : Fval.rounding_mode -> Fval.t -> Fval.Builtin_alarms.t * Fval.t
val logf : Fval.rounding_mode -> Fval.t -> Fval.builtin_res
val log10f : Fval.rounding_mode -> Fval.t -> Fval.builtin_res
val sqrtf : Fval.rounding_mode -> Fval.t -> Fval.builtin_res
val floorf : Fval.rounding_mode -> Fval.t -> Fval.Builtin_alarms.t * Fval.t
val ceilf : Fval.rounding_mode -> Fval.t -> Fval.Builtin_alarms.t * Fval.t
val truncf : Fval.rounding_mode -> Fval.t -> Fval.Builtin_alarms.t * Fval.t
val froundf :
Fval.rounding_mode -> Fval.t -> Fval.Builtin_alarms.t * Fval.t
val widen : Fval.t -> Fval.t -> Fval.t
val forward_comp :
Abstract_interp.Comp.t -> Fval.t -> Fval.t -> Abstract_interp.Comp.result
val diff : Fval.t -> Fval.t -> Fval.t Bottom.or_bottom
val backward_comp_left :
Abstract_interp.Comp.t ->
bool -> Fval.float_kind -> Fval.t -> Fval.t -> Fval.t Bottom.or_bottom
val cast_float_to_double_inverse : Fval.t -> Fval.t
val enlarge_1ulp : Fval.float_kind -> Fval.t -> Fval.t
end