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/FloatItvNan/index.html

Module ItvUtils.FloatItvNanSource

FloatItvNan - Floating-point intervals with special IEEE numbers.

Adds special IEEE number managenement (NaN, infinities) to FloatItv.

Sourcemodule F = Float
Sourcemodule FI = FloatItv
Sourcemodule B = IntBound
Sourcemodule II = IntItv

Types

Sourcetype t = {
  1. itv : FI.t Utils_core.Bot.with_bot;
    (*

    Interval of non-special values. Bounds cannot be NaN. Bounds can be infinities to represent non-infinity floats outside the range of doubles.

    *)
  2. nan : bool;
    (*

    Whether to include NaN.

    *)
  3. pinf : bool;
    (*

    Whether to include +∞.

    *)
  4. minf : bool;
    (*

    Whether to include -∞.

    *)
}

A set of IEEE floating-point values. Represented as a set of non-special values, and boolean flags to indicate the presence of each special IEEE value. The value 0 in the interval represents both IEEE +0 and -0. Note: the type can naturally represent the empty set.

Sourceval is_valid : t -> bool

All elements of type t whould satisfy this predicate.

Sourcetype prec = [
  1. | `SINGLE
    (*

    32-bit single precision

    *)
  2. | `DOUBLE
    (*

    64-bit double precision

    *)
  3. | `EXTRA
    (*

    anything larger than 64-bit double precision floats

    *)
  4. | `REAL
    (*

    real arithmetic

    *)
]

Precision. All bounds are represented as double, whatever the precision.

Sourcetype round = [
  1. | `NEAR
    (*

    To nearest

    *)
  2. | `UP
    (*

    Upwards

    *)
  3. | `DOWN
    (*

    Downwards

    *)
  4. | `ZERO
    (*

    Towards 0

    *)
  5. | `ANY
    (*

    Any rounding mode

    *)
]

Rounding direction.

Constructors

Sourceval bot : t

Empty float set.

Sourceval pinf : t
Sourceval minf : t
Sourceval nan : t
Sourceval infinities : t
Sourceval specials : t

Special values.

Sourceval of_float : float -> float -> t

Float set reduced to an interval of non-special values. lo should not be +oo nor NaN. up should not be -oo nor NaN. We can have lo = -oo and up = +oo to represent sets of non-infinity floats larger than the range of double.

Sourceval of_interval : FI.t -> t
Sourceval of_interval_bot : FI.t_with_bot -> t
Sourceval hull : float -> float -> t

Constructs the smallest interval containing a and b.

Sourceval cst : float -> t

Singleton (possibly infinity or NaN).

Sourceval zero : t
Sourceval one : t
Sourceval two : t
Sourceval mone : t
Sourceval zero_one : t
Sourceval mone_zero : t
Sourceval mone_one : t
Sourceval mhalf_half : t

Useful intervals.

Sourceval add_special : t -> t

Adds NaN and infinities to a set.

Sourceval remove_special : t -> t

Removes NaN and infinities from a set.

Sourceval single : t

Non-special single precision floats.

Sourceval double : t

Non-special double precision floats.

Sourceval extra : t

Non-special extra (> double) precision.

Sourceval real : t

Reals.

Sourceval single_special : t

Single precision floats with specials.

Sourceval double_special : t

Double precision floats with specials.

Sourceval extra_special : t

Extra (> double) precision floats with specials.

Set-theoretic

Sourceval equal : t -> t -> bool

Set equality. = also works.

Sourceval included : t -> t -> bool

Set inclusion.

Sourceval intersect_finite : t -> t -> bool

Whether the finite parts of the sets have a non-empty intersection.

Sourceval intersect : t -> t -> bool

Whether the sets have an non-empty intersection.

Sourceval contains : float -> t -> bool

Whether the set contains a certain (finite, infinite or NaN) value.

Sourceval compare : t -> t -> int

A total ordering returning -1, 0, or 1.

Sourceval is_bot : t -> bool

Whether the argument is the empty set.

Sourceval is_finite : t -> bool

Whether the argument contains only finite values (or is empty).

Sourceval is_infinity : t -> bool

Whether the argument contains only infinities (or is empty).

Sourceval is_special : t -> bool

Whether the argument contains only special values (or is empty).

Sourceval is_zero : t -> bool

Whether the argument is the singleton 0.

Sourceval is_null : t -> bool

Whether the argument contains only 0 (or is empty).

Sourceval is_positive : t -> bool

Whether the argument contains only (possibly infinite) positive non-NaN values (or is empty).

Sourceval is_negative : t -> bool

Whether the argument contains only (possibly infinite) negative non-NaN values (or is empty).

Sourceval is_positive_strict : t -> bool

Whether the argument contains only (possibly infinite) strictly positive non-NaN values (or is empty).

Sourceval is_negative_strict : t -> bool

Whether the argument contains only (possibly infinite) strictly negative non-NaN values (or is empty).

Sourceval is_nonzero : t -> bool

Whether the argument contains only (possibly infinite or NaN) non-zero values (or is empty).

Sourceval approx_size : t -> int
Sourceval is_singleton : t -> bool

Whether the argument contains only a single element.

Sourceval contains_finite : t -> bool

Whether the argument contains at least one finite value.

Sourceval contains_infinity : t -> bool

Whether the argument contains an infinity.

Sourceval contains_special : t -> bool

Whether the argument contains an infinity or NaN.

Sourceval contains_zero : t -> bool

Whether the argument contains 0.

Sourceval contains_nonzero : t -> bool

Whether the argument contains a (possibly NaN or infinite) non-0 value.

Sourceval contains_positive : t -> bool

Whether the argument contains a (possibly infinite) positive value.

Sourceval contains_negative : t -> bool

Whether the argument contains a (possibly infinite) negative value.

Sourceval contains_positive_strict : t -> bool

Whether the argument contains a (possibly infinite) strictly positive value.

Sourceval contains_negative_strict : t -> bool

Whether the argument contains a (possibly infinite) strictly negative value.

Sourceval contains_non_nan : t -> bool

Whether the argument contains a non-NaN value.

Sourceval is_in_range : t -> float -> float -> bool

Whether the argument contains only finite values, and they are included in the range lo,up.

Sourceval join : t -> t -> t
Sourceval join_list : t list -> t
Sourceval meet : t -> t -> t
Sourceval widen : t -> t -> t
Sourceval positive : t -> t

Positive part of the argument, excluding NaN.

Sourceval negative : t -> t

Negative part of the argument, excluding NaN.

Sourceval meet_zero : t -> t

Intersects with

(excluding infinities and NaN).

Printing

Sourcetype print_format = FI.print_format
Sourceval to_string : print_format -> t -> string
Sourceval print : print_format -> Stdlib.out_channel -> t -> unit
Sourceval fprint : print_format -> Stdlib.Format.formatter -> t -> unit
Sourceval bprint : print_format -> Stdlib.Buffer.t -> t -> unit

C predicates

Sourceval is_log_eq : t -> t -> bool
Sourceval is_log_leq : t -> t -> bool
Sourceval is_log_lt : t -> t -> bool
Sourceval is_log_geq : t -> t -> bool
Sourceval is_log_gt : t -> t -> bool
Sourceval is_log_neq : t -> t -> bool

C comparison tests. Returns true if the test may succeed, false if it cannot. Note that NaN always compares different to all values (including NaN).

Sourceval is_log_leq_false : t -> t -> bool
Sourceval is_log_lt_false : t -> t -> bool
Sourceval is_log_geq_false : t -> t -> bool
Sourceval is_log_gt_false : t -> t -> bool
Sourceval is_log_eq_false : t -> t -> bool
Sourceval is_log_neq_false : t -> t -> bool

Returns true if the test may fail, false if it cannot. Due to NaN, which compare always different, <= (resp. >) do not return the boolean negation of > (resp. <). However, == is the negation of != even for NaN.

Forward arithmetic

Sourceval fix_itv : prec -> t -> t
Sourceval neg : t -> t

Negation.

Sourceval abs : t -> t

Absolute value.

Sourceval fix_prec : prec -> FI.prec
Sourceval add : prec -> round -> t -> t -> t

Addition.

Sourceval sub : prec -> round -> t -> t -> t

Subtraction.

Sourceval mul : prec -> round -> t -> t -> t

Multiplication.

Sourceval div : prec -> round -> t -> t -> t

Division.

Sourceval fmod : prec -> round -> t -> t -> t

Remainder (modulo).

Sourceval square : prec -> round -> t -> t

Square.

Sourceval sqrt : prec -> round -> t -> t

Square root.

Sourceval round_int : prec -> round -> t -> t

Round to integer.

Sourceval round : prec -> round -> t -> t

Round to float.

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

Conversion from integer range.

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

Conversion from int64 range.

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

Conversion from integer range.

Sourceval to_z : t -> (Z.t * Z.t) Utils_core.Bot.with_bot

Conversion to integer range with truncation. NaN and infinities are discarded.

Sourceval of_float_prec : prec -> round -> float -> float -> t

From bounds, with rounding, precision and handling of specials.

Sourceval of_int_itv : prec -> round -> II.t -> t

Conversion from integer intervals (handling overflows to infinities).

Sourceval of_int_itv_bot : prec -> round -> II.t Utils_core.Bot.with_bot -> t

Conversion from integer intervals (handling overflows to infinities).

Conversion to integer interval with truncation. Handles infinities.

Filters

Sourceval filter_eq : prec -> t -> t -> t * t
Sourceval lift_filter_itv : (FI.t -> FI.t -> ('a * 'b) Utils_core.Bot.with_bot) -> t -> t -> 'a Utils_core.Bot.with_bot * 'b Utils_core.Bot.with_bot
Sourceval filter_leq : prec -> t -> t -> t * t
Sourceval filter_lt : prec -> t -> t -> t * t

C comparison filters. Keep the parts of the arguments that can satisfy the condition. NaN is assumed to be different from any value (including NaN).

Sourceval filter_geq : prec -> t -> t -> t * t
Sourceval filter_gt : prec -> t -> t -> t * t
Sourceval filter_neq : prec -> t -> t -> t * t
Sourceval filter_nonzero : prec -> t -> t
Sourceval filter_zero : prec -> t -> t

Refine both arguments assuming that the test is true.

Sourceval filter_leq_false : prec -> t -> t -> t * t
Sourceval filter_lt_false : prec -> t -> t -> t * t
Sourceval filter_geq_false : prec -> t -> t -> t * t
Sourceval filter_gt_false : prec -> t -> t -> t * t
Sourceval filter_eq_false : prec -> t -> t -> t * t
Sourceval filter_neq_false : prec -> t -> t -> t * t
Sourceval filter_zero_false : prec -> t -> t
Sourceval filter_nonzero_false : prec -> t -> t

Refine both arguments assuming that the test is false.

Backward arithmetic

Sourceval bwd_neg : t -> t -> t

Backward negation.

Sourceval bwd_abs : t -> t -> t

Backward absolute value.

Sourceval bwd_generic2 : prec -> round -> (FI.prec -> round -> FI.t -> FI.t -> FI.t -> (FI.t * FI.t) Utils_core.Bot.with_bot) -> t -> t -> t -> t * t
Sourceval bwd_add : prec -> round -> t -> t -> t -> t * t

Backward addition.

Sourceval bwd_sub : prec -> round -> t -> t -> t -> t * t

Backward subtraction.

Sourceval bwd_mul : prec -> round -> t -> t -> t -> t * t

Backward multiplication.

Sourceval bwd_div : prec -> round -> t -> t -> t -> t * t

Backward division.

Sourceval bwd_fmod : prec -> round -> t -> t -> t -> t * t

Backward modulo.

Sourceval bwd_generic1 : prec -> round -> (FI.prec -> round -> FI.t -> FI.t -> FI.t Utils_core.Bot.with_bot) -> t -> t -> t
Sourceval bwd_round_int : prec -> round -> t -> t -> t

Backward rounding to int.

Sourceval bwd_round : prec -> round -> t -> t -> t

Backward rounding to float.

Sourceval bwd_square : prec -> round -> t -> t -> t

Backward square.

Sourceval bwd_sqrt : prec -> round -> t -> t -> t

Backward square root.

Sourceval bwd_of_int_itv : prec -> round -> II.t -> t -> II.t_with_bot

Backward conversion from integer interval.

Sourceval bwd_to_int_itv : t -> II.t -> t

Backward conversion to integer interval (with truncation).

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