package mopsa

  1. Overview
  2. Docs
MOPSA: A Modular and Open Platform for Static Analysis using Abstract Interpretation

Install 

dune-project
 Dependency

mopsa.lip6.fr Readme Changelog Edit opam file Versions (3)

Authors

  1. A
    Antoine Miné
  2. A
    Abdelraouf Ouadjaout
  3. M
    Matthieu Journault
  4. A
    Aymeric Fromherz
  5. R
    Raphaël Monat
  6. F
    Francesco Parolini
  7. M
    Marco Milanese
  8. J
    Jérôme Boillot

Maintainers

  1. A
    Antoine Miné <antoine.mine@lip6.fr>
  2. A
    Abdelraouf Ouadjaout <ouadjaout@gmail.com>
  3. R
    Raphaël Monat <raphael.monat@inria.fr>

Sources

mopsa-analyzer-v1.2.tar.gz
md5=37966e98ffeebcedc09bd6e9b2b81f69
sha512=40d4d826c25f680766c07eccbabdf5e8a4fa023016e8a164e4e4f6b3781c8484dc4df437055721dfd19b9db8fb7fe3b61236c4833186d346fc7204a68d01eaaa

doc/mopsa.mopsa_utils/Mopsa_utils/ItvUtils/Float/index.html

Module ItvUtils.Float

Float - Floating-point arihmetics with rounding.

We rely on C code to provide functions with correct rounding (rounding direction and rounding precision).

Types

type t = float
type bit_float = {
  1. sign : bool;
    (*

    sign bit (true means negative)

    *)
  2. fraction : Z.t;
    (*

    fraction bits

    *)
  3. exponent : int;
    (*

    exponent (positive, with bias)

    *)
}

Bit-representation of a float value.

Global rounding direction

val set_round_near : unit -> unit
val set_round_up : unit -> unit
val set_round_down : unit -> unit
val set_round_zero : unit -> unit

Set the rounding mode globally. This affects the behaviors of all floating-point operations, including OCaml's native float operations, but excluding the operations in this module (and the float interval module) that specify a rounding direction.

Note that the operations with specified rounding directions may change the rounding direction globally in some unspecified way, and not reset it to its former value (this is done for efficiency).

Operations without rounding

val neg : t -> t
val abs : t -> t
val fmod : t -> t -> t

Remainder (fmod, not equivalent to IEEE 754's float remainder).

val infinite : int -> t

Constructs an infinity with the given sign. Zero maps to zero.

Predicates

val is_nan : t -> bool
val is_finite : t -> bool

Whether x is finite or not (infinite or NaN).

val is_infinite : t -> bool
val is_normal : t -> bool
val is_denormal : t -> bool
val sign : t -> int

Sign of x: -1 (negative), 0 (zero or NaN), or 1 (positive).

val sign_zero : t -> int

As sign, but zero is signed. Returns -1 (negative or -0), 0 (NaN), or 1 (positive of +0)

val equal : t -> t -> bool

Equality comparison. Identical to =, i.e., NaN ≠ NaN

val equal_nan : t -> t -> bool

As equal, but NaN equals NaN (and NaN ≠ non-NaN).

val leq : t -> t -> bool
val geq : t -> t -> bool
val lt : t -> t -> bool
val gt : t -> t -> bool
val eq : t -> t -> bool
val neq : t -> t -> bool

Comparison predicates. Returns false if one argument is NaN.

val min : t -> t -> t
val max : t -> t -> t

Minimum and maximum.

val is_zero : t -> bool
val is_nonzero : t -> bool
val is_positive : t -> bool
val is_negative : t -> bool
val is_positive_strict : t -> bool
val is_negative_strict : t -> bool

Sign predicates.

Printing

type print_format =
  1. | Dfl
  2. | Hex
    (*

    Control the printing of a float (precision, rounding, etc.).

    *)
val dfl_fmt : print_format

Default format.

val hex_fmt : print_format
val to_string : print_format -> t -> string
val print : print_format -> out_channel -> t -> unit
val fprint : print_format -> Format.formatter -> t -> unit
val bprint : print_format -> Buffer.t -> t -> unit

Operations with specific rounding direction and precision

We provide the classic operations (and more) for single and double precision and all four rounding directions.

module Single : sig ... end

Single precision operations.

module Double : sig ... end

Double precision operations.

Operations with rounding mode as argument

type prec = [
  1. | `SINGLE
    (*

    32-bit single precision

    *)
  2. | `DOUBLE
    (*

    64-bit double precision

    *)
]

Precision.

type round = [
  1. | `NEAR
    (*

    To nearest

    *)
  2. | `UP
    (*

    Upwards

    *)
  3. | `DOWN
    (*

    Downwards

    *)
  4. | `ZERO
    (*

    Towards 0

    *)
]

Rounding direction.

val add : prec -> round -> t -> t -> t

Addition.

val sub : prec -> round -> t -> t -> t

Subtraction.

val mul : prec -> round -> t -> t -> t

Multiplication.

val mulz : prec -> round -> t -> t -> t

Multiplication, where 0 * infinity is 0, not Nan.

val div : prec -> round -> t -> t -> t

Division.

val divz : prec -> round -> t -> t -> t

Division, where 0 / 0 is 0, not Nan.

val rem : prec -> round -> t -> t -> t

Modulo.

val square : prec -> round -> t -> t

Square.

val sqrt : prec -> round -> t -> t

Square root.

val round : prec -> round -> t -> t
val round_int : prec -> round -> t -> t

Rounds to integer (the result remains a float).

val of_int : prec -> round -> int -> t

Conversion from int.

val of_int64 : prec -> round -> int64 -> t

Conversion from int64.

val of_z : prec -> round -> Z.t -> t

Conversion from Z.t

val of_string : prec -> [ `DOWN | `UP ] -> string -> t

Conversion from string, with safe rounding.

val succ : prec -> t -> t

Number immediately after.

val pred : prec -> t -> t

Number immediately before.

val succ_zero : prec -> t -> t

Number immediately after. Does not cross zero.

val pred_zero : prec -> t -> t

Number immediately before. Does not cross zero.

val mantissa_bits : prec -> int
val exponent_bits : prec -> int
val exponent_bias : prec -> int
val min_exponent : prec -> int
val max_exponent : prec -> int
val nan_infinity_exponent : prec -> int
val min_denormal : prec -> t
val min_normal : prec -> t
val max_normal : prec -> t
val max_exact : prec -> t
val ulp : prec -> t

Useful constants.

val to_bits : prec -> float -> bit_float
val of_bits : prec -> bit_float -> float

Bit-level extraction.