package frama-c

You can search for identifiers within the package.

in-package search v0.2.0

On This Page

pretty modes
Rounding modes
Floating-point operations
Pretty printers
Format based constants

Platform dedicated to the analysis of source code written in C

Install

dune-project

Dependency

frama-c.com Edit opam file Versions (30)

Authors

Maintainers

F

frama-ci-bot@frama-c.com

Sources

frama-c-33.0-Arsenic.tar.gz

sha256=9c1cbffd28bb33c17a668107e39c96e4ae7378a3d8249f69b47afc7ee964e9b8

doc/frama-c.kernel/Frama_c_kernel/Floating_point/index.html

Module `Frama_c_kernel.Floating_point`

type fkind =

| FFloat
(*
float
*)
| FFloat32
(*
binary32
*)
| FFloat64
(*
binary64
*)
| FDouble
(*
double
*)
| FLongDouble
(*
long double
*)

Float kinds

since 33.0-Arsenic

pretty modes

type float_display =

| Default
| NormDec
| NormHex

Determine how floats will be printed.

since 32.0-Germanium

val set_float_display : float_display -> unit

Change the printer mode for floats.

since 32.0-Germanium

Rounding modes

type rounding =

| Nearest_even
(*
Rounding to nearest, tie to even.
*)
| Upward
(*
Rounding toward +∞.
*)
| Downward
(*
Rounding toward -∞.
*)
| 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 : fkind -> float -> float

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

Floating-point operations

type truncated_to_integer =

| Integer of Z.t
(*
The given float has been successfully truncated.
*)
| Underflow
(*
The given float would underflow if truncated.
*)
| 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 internal state float_display to decide between using the OCaml printer or the pretty_normal one. This mode can be changed using set_float_display.

val pretty_normal : use_hex:bool -> Format.formatter -> float -> unit

val pretty : Format.formatter -> float -> unit

val has_suffix : fkind -> string -> bool

True if the given string's suffix corresponds to the given format, i.e "F" for single precision (or "F32" for _Float32), "D" (or "F64") for double precision (_Float64), and "L" for extended precision.

before 33.0-Arsenic
"f32" and "f64" were not accepted.

val extract_suffix : string -> (string * string * fkind) option

extract_suffix s tries to find a floating-point suffix ("f", "F", "d", "l", "f32", etc) in s and returns Some (s_without_suffix, suffix, fkind). If s has no suffix, returns Some (s, "", FDouble). If the suffix is unknown, returns None.

since 33.0-Arsenic

Format based constants

type format =

| Single
| 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