Module Fval

module Fval: sig .. end
Floating-point intervals, used to construct arithmetic lattices. The interfaces of this module may change between Frama-C versions. Contact us if you need stable APIs.

module F: sig .. end
type t 
val packed_descr : Structural_descr.pack
exception Non_finite
Non_finite is produced when the result of a computation is entirely not-finite, such as +oo,+oo (results in Bottom).
type rounding_mode = 
| Any
| Nearest_Even
val top_single_precision_float : t
val round_to_single_precision_float : rounding_mode:rounding_mode -> t -> bool * t
val bits_of_float64 : signed:bool -> t -> Abstract_interp.Int.t * Abstract_interp.Int.t
val bits_of_float32 : signed:bool -> t -> Abstract_interp.Int.t * Abstract_interp.Int.t
val has_finite : t -> bool
has_finite f returns true iff f contains at least one finite element.
type builtin_alarm = 
| APosInf
| ANegInf
| ANaN of string
| AAssume of string
Floating-point builtins may produce three kinds of alarms:
module Builtin_alarms: Set.S  with type elt = builtin_alarm
type builtin_res = Builtin_alarms.t * t Bottom.or_bottom 
Builtins return structured alarms, in the guise of a set of string explaining the problem.
type float_kind = 
| Float32 (*
32 bits float (a.k.a 'float' C type)
*)
| Float64 (*
64 bits float (a.k.a 'double' C type)
*)
val next_after : float_kind -> F.t -> F.t -> F.t
Equivalent to the nextafter/nextafterf functions in C.
val inject : F.t -> F.t -> t
inject creates an abstract float interval. Does not handle infinities or NaN. Does not enlarge subnormals to handle flush-to-zero modes
val inject_r_f : float_kind -> F.t -> F.t -> bool * bool * t
inject_r_f creates an abstract float interval. It handles infinities and flush-to-zero (rounding subnormals if needed), but not NaN. The returned booleans are true if the lower/upper bound may be infinite. May raise Fval.Non_finite when no part of the result would be finite. Inputs must be compatible with float_kind.
val inject_r : F.t -> F.t -> bool * t
Alias for inject_r_f Float64.
val inject_f : float_kind -> F.t -> F.t -> t
Equivalent to inject_r_f, but ignores the boolean not_finite. The caller must emit appropriate warnings in the presence of non-finite values.
val inject_singleton : F.t -> t
val compare_min : t -> t -> int
val compare_max : t -> t -> int
val min_and_max : t -> F.t * F.t
val top : t
val add : rounding_mode -> t -> t -> bool * t
val sub : rounding_mode -> t -> t -> bool * t
val mul : rounding_mode -> t -> t -> bool * t
val div : rounding_mode -> t -> t -> bool * t
val is_a_zero : t -> bool
is_a_zero f returns true iff f ⊆ -0.0,+0.0
val contains_zero : t -> bool
val compare : t -> t -> int
val pretty : Format.formatter -> t -> unit
val pretty_overflow : Format.formatter -> t -> unit
This pretty-printer does not display -FLT_MAX and FLT_MAX as interval bounds. Instead, the special notation --. is used.
val hash : t -> int
val zero : t
val minus_zero : t
val zeros : t
Both positive and negative zero
val is_zero : t -> bool
val is_included : t -> t -> bool
val join : t -> t -> t
val meet : t -> t -> t Bottom.or_bottom
val narrow : t -> t -> t Bottom.or_bottom
val contains_a_zero : t -> bool
val is_singleton : t -> bool
exception Not_Singleton_Float
val project_float : t -> F.t
Raises Not_Singleton_Float when the interval is not a single float.
val minus_one_one : t
val subdiv_float_interval : size:float_kind option -> t -> t * t
val neg : t -> t
val cos : t -> t
val sin : t -> t
val atan2 : t -> t -> builtin_res
Returns atan2(y,x). Does not emit any alarms.
val pow : t -> t -> builtin_res
Returns pow(x,y).
val powf : t -> t -> builtin_res
Single-precision version of pow.
val fmod : t -> t -> builtin_res
Returns fmod(x,y). May return a "division by zero" alarm. Raises Builtin_invalid_domain if there is certainly a division by zero.
val sqrt : rounding_mode -> t -> builtin_res

Discussion regarding -all-rounding-modes and the functions below.

Support for fesetround(FE_UPWARD) and fesetround(FE_DOWNWARD) seems to be especially poor, including in not-so-old versions of Glibc (https://sourceware.org/bugzilla/show_bug.cgi?id=3976). The code for Fval.exp, Fval.log and Fval.log10 is correct wrt. -all-rounding-modes ONLY if the C implementation of these functions is correct in directed rounding modes. Otherwise, anything could happen, including crashes. For now, unless the Libc is known to be reliable, these functions should be called with rounding_mode=Nearest_Even only. Also note that there the Glibc does not guarantee that f(FE_DOWNWARD) <= f(FE_TONEAREST) <= f(FE_UPWARD), which implies that using different rounding modes to bound the final result does not ensure correct bounds. Here's an example where it does not hold (glibc 2.21): log10f(3, FE_TONEAREST) < log10f(3, FE_DOWNWARD).

val exp : rounding_mode -> t -> Builtin_alarms.t * t
val log : rounding_mode -> t -> builtin_res
val log10 : rounding_mode -> t -> builtin_res
All three functions may raise Fval.Non_finite. Can only be called to approximate a computation on double (float64).
val floor : rounding_mode -> t -> Builtin_alarms.t * t
val ceil : rounding_mode -> t -> Builtin_alarms.t * t
val trunc : rounding_mode -> t -> Builtin_alarms.t * t
val fround : rounding_mode -> t -> Builtin_alarms.t * t
val expf : rounding_mode -> t -> Builtin_alarms.t * t
val logf : rounding_mode -> t -> builtin_res
val log10f : rounding_mode -> t -> builtin_res
val sqrtf : rounding_mode -> t -> builtin_res
val floorf : rounding_mode -> t -> Builtin_alarms.t * t
val ceilf : rounding_mode -> t -> Builtin_alarms.t * t
val truncf : rounding_mode -> t -> Builtin_alarms.t * t
val froundf : rounding_mode -> t -> Builtin_alarms.t * t
Single-precision versions
val widen : t -> t -> t
val forward_comp : Abstract_interp.Comp.t -> t -> t -> Abstract_interp.Comp.result
val diff : t -> t -> t Bottom.or_bottom
val backward_comp_left : Abstract_interp.Comp.t ->
bool -> float_kind -> t -> t -> t Bottom.or_bottom
backward_comp op allroundingmodes fkind f1 f2 attempts to reduce f1 into f1' so that the relation f1' op f2 holds. fkind is the type of f1 and f1' (not necessarily of f2). If allroundingmodes is set, all possible rounding modes are taken into account. op must be Eq, Ne, Le, Ge, Lt or Gt
val cast_float_to_double_inverse : t -> t
cast_float_to_double_inverse d return all possible float32 f such that (double)f = d. The double of d that have no float32 equivalent are discarded.
val enlarge_1ulp : float_kind -> t -> t
enlarge the bounds of the interval by one ulp.
Raises Non_finite if the result is not fully finite.