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/congUtils/CongUtils/IntCong/index.html

Module CongUtils.IntCongSource

IntCong - Integer congruences.

We rely on Zarith for arithmetic operations.

Types

Sourcetype t = Z.t * Z.t

offset

The type of possibly empty congruence sets.

Sourceval is_valid : t -> bool
module I = ItvUtils.IntItv

Arithmetic utilities

Sourceval gcd : Z.t -> Z.t -> Z.t

Greatest common divisor of |a| and |b|. 0 is neutral.

Sourceval gcd3 : Z.t -> Z.t -> Z.t -> Z.t
Sourceval gcd_ext : Z.t -> Z.t -> Z.t * Z.t * Z.t * Z.t

Returns the gcd, lcm and cofactors u, v such that ua+vb=gcd. Undefined if a or b is 0.

Sourceval divides : Z.t -> Z.t -> bool

Wheter b is a multiple of a. Always true if b = 0.

Sourceval rem_zero : Z.t -> Z.t -> Z.t

As Z.erem, but rem_zero a 0 = a.

Constructors

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

Returns aℤ + b.

Sourceval of_int : int -> int -> t
Sourceval of_int64 : int64 -> int64 -> t
Sourceval cst : Z.t -> t

Returns 0ℤ + b

Sourceval cst_int : int -> t
Sourceval cst_int64 : int64 -> t
Sourceval zero : t

0ℤ+0

Sourceval one : t

0ℤ+1

Sourceval mone : t

0ℤ-1

Sourceval minf_inf : t

1ℤ+0

Sourceval of_range : Z.t -> Z.t -> t
Sourceval of_range_bot : Z.t -> Z.t -> t Utils_core.Bot.with_bot
Sourceval of_bound : B.t -> B.t -> t
Sourceval of_bound_bot : B.t -> B.t -> t Utils_core.Bot.with_bot

Congruence overapproximating an interval.

Predicates

Sourceval equal : t -> t -> bool

Equality. = also works.

Sourceval equal_bot : t_with_bot -> t_with_bot -> bool
Sourceval included : t -> t -> bool

Set ordering.

Sourceval included_bot : t_with_bot -> t_with_bot -> bool
Sourceval intersect : t -> t -> bool

Whether the intersection is non-empty.

Sourceval intersect_bot : t_with_bot -> t_with_bot -> bool
Sourceval contains : Z.t -> t -> bool

Whether the set contains some value x.

Sourceval compare : t -> t -> int

A total ordering (lexical ordering) returning -1, 0, or 1. Can be used as compare for sets, maps, etc.

Total ordering on possibly empty congruences.

Sourceval contains_zero : t -> bool

Whether the congruence contains zero.

Sourceval contains_one : t -> bool

Whether the congruence contains one.

Sourceval contains_nonzero : t -> bool

Whether the congruence contains a non-zero value.

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

Sign.

Sourceval is_minf_inf : t -> bool

The congruence represents -∞,+∞.

Sourceval is_singleton : t -> bool

Whether the congruence contains a single element.

Sourceval is_bounded : t -> bool

Whether the congruence contains a finite number of elements.

Sourceval is_in_range : t -> Z.t -> Z.t -> bool

Whether the congruence is included in the range lo,up.

Printing

Sourceval to_string : t -> string
Sourceval print : Stdlib.out_channel -> t -> unit
Sourceval fprint : Stdlib.Format.formatter -> t -> unit
Sourceval bprint : Stdlib.Buffer.t -> t -> unit
Sourceval to_string_bot : t Utils_core.Bot.with_bot -> string
Sourceval print_bot : Stdlib.out_channel -> t Utils_core.Bot.with_bot -> unit
Sourceval fprint_bot : Stdlib.Format.formatter -> t Utils_core.Bot.with_bot -> unit
Sourceval bprint_bot : Stdlib.Buffer.t -> t Utils_core.Bot.with_bot -> unit

Set operations

Sourceval join : t -> t -> t

Abstract union.

Sourceval join_list : t list -> t_with_bot
Sourceval meet : t -> t -> t_with_bot

Abstract intersection.

Sourceval meet_list : t list -> t_with_bot
Sourceval meet_range : t -> Z.t -> Z.t -> t_with_bot

Abstract intersection with lo,up.

Sourceval positive : t -> t_with_bot
Sourceval negative : t -> t_with_bot

Positive and negative part.

Sourceval meet_zero : t -> t_with_bot

Intersects with

.

Sourceval meet_nonzero : t -> t_with_bot

Keeps only non-zero elements.

Forward operations

Sourceval neg : t -> t

Negation.

Sourceval abs : t -> t

Absolute value.

Sourceval succ : t -> t

Adding 1.

Sourceval pred : t -> t

Subtracting 1.

Sourceval add : t -> t -> t

Addition.

Sourceval sub : t -> t -> t

Subtraction.

Sourceval mul : t -> t -> t

Multiplication.

Sourceval div : t -> t -> t_with_bot

Division (with truncation).

Sourceval rem : t -> t -> t_with_bot

Remainder. Uses the C semantics for remainder (%).

Sourceval wrap : t -> Z.t -> Z.t -> t

Put back inside lo,up by modular arithmetics.

Sourceval to_bool : bool -> bool -> t
Sourceval log_cast : t -> t

Conversion from integer to boolean in 0,1: maps 0 to 0 (false) and non-zero to 1 (true). 0;1 is over-approximated as ℤ.

Sourceval log_not : t -> t

Logical negation. Logical operation use the C semantics: they accept 0 and non-0 respectively as false and true, but they always return 0 and 1 respectively for false and true. 0;1 is over-approximated as ℤ.

Sourceval log_and : t -> t -> t

Logical and.

Sourceval log_or : t -> t -> t

Logical or.

Sourceval log_xor : t -> t -> t

Logical exclusive or.

Sourceval log_eq : t -> t -> t
Sourceval log_neq : t -> t -> t
Sourceval log_sgl : (Z.t -> Z.t -> bool) -> t -> t -> t
Sourceval log_leq : t -> t -> t
Sourceval log_geq : t -> t -> t
Sourceval log_lt : t -> t -> t
Sourceval log_gt : t -> t -> t

C comparison tests. Returns an interval included in 0,1 (a boolean)

Sourceval is_log_eq : t -> t -> bool
Sourceval is_log_neq : t -> t -> bool
Sourceval is_log_sgl : (Z.t -> Z.t -> bool) -> t -> t -> bool
Sourceval is_log_leq : t -> t -> bool
Sourceval is_log_geq : t -> t -> bool
Sourceval is_log_lt : t -> t -> bool
Sourceval is_log_gt : t -> t -> bool

C comparison tests. Returns a boolean if the test may succeed

Sourceval shift_left : t -> t -> t_with_bot

Bitshift left: multiplication by a power of 2.

Sourceval shift_right : t -> t -> t_with_bot

Bitshift right: division by a power of 2 rounding towards -∞.

Sourceval shift_right_trunc : t -> t -> t_with_bot

Unsigned bitshift right: division by a power of 2 with truncation.

Sourceval bit_not : t -> t

Bitwise negation: ~x = -x-1

Filters

Given two interval aruments, return the arguments assuming that the predicate holds.

Sourceval filter_eq : t -> t -> (t * t) Utils_core.Bot.with_bot
Sourceval filter_sgl : (Z.t -> Z.t -> bool) -> t -> t -> (t * t) Utils_core.Bot.with_bot
Sourceval filter_neq : t -> t -> (t * t) Utils_core.Bot.with_bot
Sourceval filter_leq : t -> t -> (t * t) Utils_core.Bot.with_bot
Sourceval filter_geq : t -> t -> (t * t) Utils_core.Bot.with_bot
Sourceval filter_lt : t -> t -> (t * t) Utils_core.Bot.with_bot
Sourceval filter_gt : t -> t -> (t * t) Utils_core.Bot.with_bot

Backward operations

Given one or two interval argument(s) and a result interval, return the argument(s) assuming the result in the operation is in the given result.

Sourceval bwd_neg : t -> t -> t_with_bot
Sourceval bwd_abs : t -> t -> t_with_bot
Sourceval bwd_succ : t -> t -> t_with_bot
Sourceval bwd_pred : t -> t -> t_with_bot
Sourceval bwd_add : t -> t -> t -> (t * t) Utils_core.Bot.with_bot
Sourceval bwd_sub : t -> t -> t -> (t * t) Utils_core.Bot.with_bot
Sourceval bwd_mul : t -> t -> t -> (t * t) Utils_core.Bot.with_bot
Sourceval bwd_bit_not : t -> t -> t_with_bot
Sourceval bwd_join : t -> t -> t -> (t * t) Utils_core.Bot.with_bot

Backward join: both arguments and intersected with the result.

Sourceval bwd_rem : t -> t -> t -> (t * (Z.t * Z.t)) Utils_core.Bot.with_bot
Sourceval bwd_div : t -> t -> t -> (t * t) Utils_core.Bot.with_bot
Sourceval bwd_wrap : t -> 'a -> t -> t_with_bot
Sourceval bwd_shift_left : t -> t -> t -> (t * t) Utils_core.Bot.with_bot
Sourceval bwd_shift_right : t -> t -> t -> (t * t) Utils_core.Bot.with_bot
Sourceval bwd_shift_right_trunc : t -> t -> t -> (t * t) Utils_core.Bot.with_bot

Reduction

Sourceval meet_inter : t -> I.t -> (t * I.t) Utils_core.Bot.with_bot

Intersects a congruence with an interval, and returns the set represented both as a congruence and as an interval. Useful to implement reductions.

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