Module Frama_c_kernel.Floating_point

Rounding modes

type rounding =
  1. | Nearest_even
    (*

    Rounding to nearest, tie to even.

    *)
  2. | Upward
    (*

    Rounding toward +∞.

    *)
  3. | Downward
    (*

    Rounding toward -∞.

    *)
  4. | Toward_zero
    (*

    Rounding toward zero.

    *)
val set_rounding_mode : rounding -> unit

Set the current rounding mode.

val get_rounding_mode : unit -> rounding

Get the current rounding mode.

val round_to_single_precision : float -> float

Rounds the given float to a single precision float.

val round_if_single_precision : Cil_types.fkind -> float -> float

Rounds the given float to a single precision float if fkind = FFloat.

Floating-point operations

type truncated_to_integer =
  1. | Integer of Integer.t
    (*

    The given float has been succesfully truncated.

    *)
  2. | Underflow
    (*

    The given float would underflow if truncated.

    *)
  3. | Overflow
    (*

    The given float would overflow if truncated.

    *)
val truncate_to_integer : float -> truncated_to_integer

Truncates a given floating point number, i.e returns the closest integer rounded toward zero, regardless of the current rounding mode. The truncate_to_integer function converts the given number into an 64 bits integer it it fits or a token specifying if the conversion is impossible due to an underflow or an overflow.

val is_finite : float -> bool

True if the given float is finite (not infinite or a NaN).

val is_infinite : float -> bool

True if the given float is infinite (but not a NaN).

val is_nan : float -> bool

True if the given float is a NaN.

Pretty printers

The function pretty_normal implements a custom printer. The function pretty relies on kernel's options to decide between using the OCaml printer or the pretty_normal one.

val pretty_normal : use_hex:bool -> Format.formatter -> float -> unit
val pretty : Format.formatter -> float -> unit
val has_suffix : Cil_types.fkind -> string -> bool

True if the given string's last character corresponds to the given format, i.e 'F' for single precision, 'D' for double precision and 'L' for extended precision.

Format based constants

type format =
  1. | Single
  2. | Double

The significant size of a given format is denoted m. The exponent size of a given format is denoted e.

val largest_finite_float_of : format -> float

Returns the largest positive finite floating point number of a given format. It is computed as :

\left({2 - 2 ^ {1 - m}}\right) ^ {2 ^ {e - 1} - 1}
val finite_range_of : format -> float * float

Returns the bounds of the finite range of a given format, i.e the largest negative finite floating point number and the largest positive finite floating point number of a given format.

val smallest_normal_float_of : format -> float

Returns the smallest positive normalized floating point number of a given format. It is computed as :

 {2} ^ {2 - {2} ^ {e - 1}}
val smallest_denormal_float_of : format -> float

Returns the smallest positive denormalized floating point number of a given format. It is simply computed by setting the least significant bit to one, as this bit corresponds to the last bit of the significant.

val unit_in_the_last_place_of : format -> float

Returns the unit in the last place of a given format, i.e the value of the least significant bit of a floating point number with an exponent set at zero. It is primally used to overapproximate rounding errors. It is computed as 2 ^ {-m}.

val minimal_exponent_of : format -> int
val maximal_exponent_of : format -> int