Frama-C:
Plug-ins:
Libraries:

Frama-C API - Precisions

type t =
  1. | Simple
  2. | Double
  3. | Long_Double
  4. | Real

We handle the format defined in C. The Real constructor represents the precision of the floats used as real

val pretty : Stdlib.Format.formatter -> t -> unit

Returns the precision associated to the Cil construction fkind, which represents the C floating point type

val get : t -> int

Returns the number of bits of the significand of the given precision, counting the implicit one. This size is fixed by the option -eva-numerors-real-size for the Real precision.

val exponent : t -> int

Returns the number of bits of the exponent of the given precision. The exponent of the Real precision is set to max int arbitrally.

val denormalized : t -> int

Returns the integer corresponding to the exponent of the denormalized numbers of the given precision. The value 2^denormalized is the smallest denormalized number of the precision and is also the gap between two denormalized numbers. The returned integer is negative. For the Real precision, this integer is arbitrally set to min int.

val compare : t -> t -> int
val eq : t -> t -> bool
val max : t -> t -> t
val min : t -> t -> t