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

Module ItvUtils.IntBound

IntBound - Enriches arbitrary precision integers with +∞ and -∞.

Useful as interval bounds.

Types

type t =
  1. | Finite of Z.t
  2. | MINF
    (*

    -∞

    *)
  3. | PINF
    (*

    +∞

    *)

Internal utilities

Constructors

val zero : t
val one : t
val minus_one : t

Useful constants

val of_int : int -> t
val of_int64 : int64 -> t

Exact conversion from machine integers.

val of_float : float -> t

Conversion with truncation from floats. Handles infinites. Raises an exception on NaNs.

val infinite : int -> t

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

val pow2 : int -> t

A power of two. The argument must be positive.

Predicates

val sign : t -> int

Sign of x: -1, 0, or 1.

val is_finite : t -> bool

Whether x is finite or not.

val equal : t -> t -> bool

Equality comparison. = also works.

val compare : t -> t -> int

Total order. Returns -1 (strictly smaller), 0 (equal), or 1 (strictly greater).

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.

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.

val hash : t -> int

Hashing function.

Printing

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

Operators

val succ : t -> t

+1. Infinities are left unchanged.

val pred : t -> t

-1. Infinities are left unchanged.

val neg : t -> t

Negation.

val abs : t -> t

Absolute value.

val add : t -> t -> t

Addition. +∞ + -∞ is undefined (invalid argument exception).

val sub : t -> t -> t

Subtraction. +∞ - +∞ is undefined (invalid argument exception).

val mul : t -> t -> t

Multiplication. Always defined: +∞ * 0 = 0

val div : t -> t -> t

Division. Always defined: 0 / 0 = 0, x / +∞ = 0, x / 0 = sign(x) * ∞

val ediv : t -> t -> t

Euclidian division. Always defined: 0 / 0 = 0, x / +∞ = 0, x / 0 = sign(x) * ∞

val rem : t -> t -> t

Remainder. rem x y has the sign of x, rem x (-y) = rem x y, and rem x +∞ = x. rem +∞ y and rem x 0 are undefined (invalid argument exception).

val erem : t -> t -> t

Euclidian remainder. erem x y >= 0, rem x y < |b| and a = b * ediv a b + erem a b. rem +∞ y and rem x 0 are undefined (invalid argument exception).

val shift_left : t -> t -> t

Left bitshift. Undefined if the second argument is negative (invalid argument exception). Returns an infinity if the second argument is too large.

val shift_right : t -> t -> t

Right bitshift, rounding towards -∞. Undefined if the second argument is negative (invalid argument exception). Returns zero if the second argument is too large.

val shift_right_trunc : t -> t -> t

Right bitshift, rounding towards 0 (truncation). Undefined if the second argument is negative (invalid argument exception). Returns zero if the second argument is too large.

val only_finite : string -> (Z.t -> Z.t -> Z.t) -> t -> t -> t
val bit_or : t -> t -> t
val bit_xor : t -> t -> t
val bit_and : t -> t -> t

Bitwise operations. Undefined for infinites (invalid argument exception).

val pow : t -> t -> t

Power. Undefined if the second argument is negative or too large.