package mopsa

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

Install

Dune Dependency

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

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.1.tar.gz
md5=fdee20e988343751de440b4f6b67c0f4
sha512=f5cbf1328785d3f5ce40155dada2d95e5de5cce4f084ea30cfb04d1ab10cc9403a26cfb3fa55d0f9da72244482130fdb89c286a9aed0d640bba46b7c00e09500

doc/itvUtils/ItvUtils/Float/Single/index.html

Module Float.SingleSource

Single precision operations.

Single precision numbers are stored inside OCaml's floats, that are actually double precion, but rounding is done to single precision.

Operations

Sourceval add_near : t -> t -> t
Sourceval add_up : t -> t -> t
Sourceval add_down : t -> t -> t
Sourceval add_zero : t -> t -> t

Addition

Sourceval sub_near : t -> t -> t
Sourceval sub_up : t -> t -> t
Sourceval sub_down : t -> t -> t
Sourceval sub_zero : t -> t -> t

Subtraction

Sourceval mul_near : t -> t -> t
Sourceval mul_up : t -> t -> t
Sourceval mul_down : t -> t -> t
Sourceval mul_zero : t -> t -> t

Multiplication

Sourceval mulz_near : t -> t -> t
Sourceval mulz_up : t -> t -> t
Sourceval mulz_down : t -> t -> t
Sourceval mulz_zero : t -> t -> t

Special multiplication where 0 times an infinity is 0, not NaN. This is particularly useful for interal bounds.

Sourceval div_near : t -> t -> t
Sourceval div_up : t -> t -> t
Sourceval div_down : t -> t -> t
Sourceval div_zero : t -> t -> t

Division

Sourceval divz_near : t -> t -> t
Sourceval divz_up : t -> t -> t
Sourceval divz_down : t -> t -> t
Sourceval divz_zero : t -> t -> t

Special division where 0 / 0 is 0, not NaN. This is particularly useful for interal bounds.

Sourceval mod_near : t -> t -> t
Sourceval mod_up : t -> t -> t
Sourceval mod_down : t -> t -> t
Sourceval mod_zero : t -> t -> t

Remainder.

Sourceval square_near : t -> t
Sourceval square_up : t -> t
Sourceval square_down : t -> t
Sourceval square_zero : t -> t

Square.

Sourceval sqrt_near : t -> t
Sourceval sqrt_up : t -> t
Sourceval sqrt_down : t -> t
Sourceval sqrt_zero : t -> t

Square root.

Sourceval round_int_near : t -> t
Sourceval round_int_up : t -> t
Sourceval round_int_down : t -> t
Sourceval round_int_zero : t -> t

Rounding to an integer.

Sourceval of_double_near : t -> t
Sourceval of_double_up : t -> t
Sourceval of_double_down : t -> t
Sourceval of_double_zero : t -> t

Rounding from double to single precision.

Sourceval of_int_near : int -> t
Sourceval of_int_up : int -> t
Sourceval of_int_down : int -> t
Sourceval of_int_zero : int -> t
Sourceval of_int_cur : int -> t

Conversion from int with rounding.

Sourceval of_int64_near : int64 -> t
Sourceval of_int64_up : int64 -> t
Sourceval of_int64_down : int64 -> t
Sourceval of_int64_zero : int64 -> t
Sourceval of_int64_cur : int64 -> t

Conversion from int64 with rounding.

Code from Zarith to convert from Z.t to float using the current rounding mode. We add a version for single precision rounding.

Sourceval round_z_to_single : Z.t -> bool -> t
Sourceval z_to_single : Z.t -> t
Sourceval of_z_near : Z.t -> t
Sourceval of_z_up : Z.t -> t
Sourceval of_z_down : Z.t -> t
Sourceval of_z_zero : Z.t -> t

Conversion from Zarith with rounding.

Floating-point format characteristics

Sourceval mantissa_bits : int
Sourceval exponent_bits : int
Sourceval exponent_bias : int
Sourceval min_exponent : int
Sourceval max_exponent : int
Sourceval nan_infinity_exponent : int
Sourceval min_denormal : t
Sourceval min_normal : t
Sourceval max_normal : t
Sourceval max_exact : t
Sourceval ulp : t

Units in the last place (relative precision).

Sourceval rep_of_bits : int32 -> bit_float
Sourceval bits_of_rep : bit_float -> int32
Sourceval to_bits : t -> int32
Sourceval of_bits : int32 -> t
Sourceval succ : t -> t
Sourceval pred : t -> t

Returns the float immediately follownig or preceeding the argument.

Sourceval succ_zero : t -> t
Sourceval pred_zero : t -> t

As succ and pred, but does not cross zero.

Sourceval of_string_up : string -> t
Sourceval of_string_down : string -> t

Conversion from string.

OCaml

Innovation. Community. Security.

GitHub Discord Twitter Peertube RSS
About
Changelog Releases Industrial Users Academic Users Why OCaml
Ecosystem
Packages Community Events OCaml Planet Jobs
Resources
Install OCaml Get Started Platform Tools Language Manual Standard Library API Books Exercises Papers OCaml Playground Logo
Policies
Carbon Footprint Governance Privacy Code of Conduct