package mopsa

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

Install

Dune Dependency

gitlab.com 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.0.tar.gz
md5=9f673f79708b44a7effb3b6bb3618d2c
sha512=cb91cb428e43a22f1abbcb8219710d0c10a5b3756d0da392d4084b3b3a6157350776c596983e63def344f617d39964e91f244f60c07958695ee5c8c809a9f0f4

doc/itvUtils/ItvUtils/FloatItv/Double/index.html

Module FloatItv.DoubleSource

Intervals with rounding to double.

Sourcemodule FF = F.Double

Arithmetic

Sourceval add_near : t -> t -> t
Sourceval add_up : t -> t -> t
Sourceval add_down : t -> t -> t
Sourceval add_zero : t -> t -> t
Sourceval add_outer : t -> t -> t
Sourceval add_inner : t -> t -> t_with_bot

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
Sourceval sub_outer : t -> t -> t
Sourceval sub_inner : t -> t -> t_with_bot

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
Sourceval mul_outer : t -> t -> t
Sourceval mul_inner : t -> t -> t_with_bot

Multiplication.

Sourceval divpos_near : t -> t -> t
Sourceval divpos_up : t -> t -> t
Sourceval divpos_down : t -> t -> t
Sourceval divpos_zero : t -> t -> t
Sourceval divpos_outer : t -> t -> t
Sourceval divpos_inner : t -> t -> t_with_bot
Sourceval div_unmerged_near : t -> t -> t list
Sourceval div_unmerged_up : t -> t -> t list
Sourceval div_unmerged_down : t -> t -> t list
Sourceval div_unmerged_zero : t -> t -> t list
Sourceval div_unmerged_outer : t -> t -> t list
Sourceval div_unmerged_inner : t -> t -> t list

Division. Returns a list of 0, 1, or 2 intervals to remain precise.

Sourceval div_near : t -> t -> t_with_bot
Sourceval div_up : t -> t -> t_with_bot
Sourceval div_down : t -> t -> t_with_bot
Sourceval div_zero : t -> t -> t_with_bot
Sourceval div_outer : t -> t -> t_with_bot
Sourceval div_inner : t -> t -> t_with_bot

Division. Returns a single interval.

Sourceval square_near : t -> t
Sourceval square_up : t -> t
Sourceval square_down : t -> t
Sourceval square_zero : t -> t
Sourceval square_outer : t -> t
Sourceval square_inner : t -> t_with_bot

Square.

Sourceval sqrt_near : t -> t_with_bot
Sourceval sqrt_up : t -> t_with_bot
Sourceval sqrt_down : t -> t_with_bot
Sourceval sqrt_zero : t -> t_with_bot
Sourceval sqrt_outer : t -> t_with_bot
Sourceval sqrt_inner : t -> t_with_bot

Square root. Returns the square root of the positive part, possibly ⊥.

Sourceval round_int_near : t -> t
Sourceval round_int_up : t -> t
Sourceval round_int_down : t -> t
Sourceval round_int_zero : t -> t
Sourceval round_int_outer : t -> t
Sourceval round_int_inner : t -> t_with_bot

Round to integer.

Sourceval unround_int_near : t -> t
Sourceval unround_int_up : t -> t
Sourceval unround_int_down : t -> t
Sourceval unround_int_zero : t -> t
Sourceval unround_int_any : t -> t

Values that, after rounding to integer in the specified direction, may be in the argument interval. Useful for backward operators.

Sourceval unround_near : t -> t
Sourceval unround_up : t -> t
Sourceval unround_down : t -> t
Sourceval unround_zero : t -> t
Sourceval unround_any : t -> t

Values that, after rounding to float, may be in the argument interval. Useful for backward operators.

Sourceval of_int_near : int -> int -> t
Sourceval of_int_up : int -> int -> t
Sourceval of_int_down : int -> int -> t
Sourceval of_int_zero : int -> int -> t
Sourceval of_int_outer : int -> int -> t
Sourceval of_int_inner : int -> int -> t_with_bot

Conversion from int.

Sourceval of_int64_near : int64 -> int64 -> t
Sourceval of_int64_up : int64 -> int64 -> t
Sourceval of_int64_down : int64 -> int64 -> t
Sourceval of_int64_zero : int64 -> int64 -> t
Sourceval of_int64_outer : int64 -> int64 -> t
Sourceval of_int64_inner : int64 -> int64 -> t_with_bot

Conversion from int64.

Sourceval of_z_near : Z.t -> Z.t -> t
Sourceval of_z_up : Z.t -> Z.t -> t
Sourceval of_z_down : Z.t -> Z.t -> t
Sourceval of_z_zero : Z.t -> Z.t -> t
Sourceval of_z_outer : Z.t -> Z.t -> t
Sourceval of_z_inner : Z.t -> Z.t -> t_with_bot

Conversion from Z.t.

Filters

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

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
Sourceval filter_eq : t -> t -> (t * t) Utils_core.Bot.with_bot
Sourceval filter_neq : 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_add : t -> t -> t -> (t * t) Utils_core.Bot.with_bot
Sourceval bwd_add_near : t -> t -> t -> (t * t) Utils_core.Bot.with_bot
Sourceval bwd_add_up : t -> t -> t -> (t * t) Utils_core.Bot.with_bot
Sourceval bwd_add_down : t -> t -> t -> (t * t) Utils_core.Bot.with_bot
Sourceval bwd_add_zero : t -> t -> t -> (t * t) Utils_core.Bot.with_bot
Sourceval bwd_add_any : t -> t -> t -> (t * t) Utils_core.Bot.with_bot
Sourceval bwd_add_noround : t -> t -> t -> (t * t) Utils_core.Bot.with_bot

Backward addition.

Sourceval bwd_sub : t -> t -> t -> (t * t) Utils_core.Bot.with_bot
Sourceval bwd_sub_near : t -> t -> t -> (t * t) Utils_core.Bot.with_bot
Sourceval bwd_sub_up : t -> t -> t -> (t * t) Utils_core.Bot.with_bot
Sourceval bwd_sub_down : t -> t -> t -> (t * t) Utils_core.Bot.with_bot
Sourceval bwd_sub_zero : t -> t -> t -> (t * t) Utils_core.Bot.with_bot
Sourceval bwd_sub_any : t -> t -> t -> (t * t) Utils_core.Bot.with_bot
Sourceval bwd_sub_noround : t -> t -> t -> (t * t) Utils_core.Bot.with_bot

Backward subtraction.

Sourceval bwd_mul : t -> t -> t -> (t * t) Utils_core.Bot.with_bot
Sourceval bwd_mul_near : t -> t -> t -> (t * t) Utils_core.Bot.with_bot
Sourceval bwd_mul_up : t -> t -> t -> (t * t) Utils_core.Bot.with_bot
Sourceval bwd_mul_down : t -> t -> t -> (t * t) Utils_core.Bot.with_bot
Sourceval bwd_mul_zero : t -> t -> t -> (t * t) Utils_core.Bot.with_bot
Sourceval bwd_mul_any : t -> t -> t -> (t * t) Utils_core.Bot.with_bot
Sourceval bwd_mul_noround : t -> t -> t -> (t * t) Utils_core.Bot.with_bot

Backward multiplication.

Sourceval bwd_div : t -> t -> t -> (t * t) Utils_core.Bot.with_bot
Sourceval bwd_div_near : t -> t -> t -> (t * t) Utils_core.Bot.with_bot
Sourceval bwd_div_up : t -> t -> t -> (t * t) Utils_core.Bot.with_bot
Sourceval bwd_div_down : t -> t -> t -> (t * t) Utils_core.Bot.with_bot
Sourceval bwd_div_zero : t -> t -> t -> (t * t) Utils_core.Bot.with_bot
Sourceval bwd_div_any : t -> t -> t -> (t * t) Utils_core.Bot.with_bot
Sourceval bwd_div_noround : t -> t -> t -> (t * t) Utils_core.Bot.with_bot

Backward division.

Sourceval bwd_round_int_near : t -> t -> t_with_bot
Sourceval bwd_round_int_up : t -> t -> t_with_bot
Sourceval bwd_round_int_down : t -> t -> t_with_bot
Sourceval bwd_round_int_zero : t -> t -> t_with_bot
Sourceval bwd_round_int_any : t -> t -> t_with_bot
Sourceval bwd_round_int_noround : t -> t -> t_with_bot

Backward rounding to int.

Sourceval bwd_round_near : t -> t -> t_with_bot
Sourceval bwd_round_up : t -> t -> t_with_bot
Sourceval bwd_round_down : t -> t -> t_with_bot
Sourceval bwd_round_zero : t -> t -> t_with_bot
Sourceval bwd_round_any : t -> t -> t_with_bot
Sourceval bwd_round_noround : t -> t -> t_with_bot

Backward rounding from real.

Sourceval bwd_square : t -> t -> t_with_bot
Sourceval bwd_square_near : t -> t -> t_with_bot
Sourceval bwd_square_up : t -> t -> t_with_bot
Sourceval bwd_square_down : t -> t -> t_with_bot
Sourceval bwd_square_zero : t -> t -> t_with_bot
Sourceval bwd_square_any : t -> t -> t_with_bot
Sourceval bwd_square_noround : t -> t -> t_with_bot

Backward square.

Sourceval bwd_sqrt : t -> t -> t_with_bot
Sourceval bwd_sqrt_near : t -> t -> t_with_bot
Sourceval bwd_sqrt_up : t -> t -> t_with_bot
Sourceval bwd_sqrt_down : t -> t -> t_with_bot
Sourceval bwd_sqrt_zero : t -> t -> t_with_bot
Sourceval bwd_sqrt_any : t -> t -> t_with_bot
Sourceval bwd_sqrt_noround : t -> t -> t_with_bot

Backward square root.

Sourceval bwd_of_z : ('a -> t) -> Z.t -> Z.t -> 'a -> (Z.t * Z.t) Utils_core.Bot.with_bot
Sourceval bwd_of_z_near : Z.t -> Z.t -> t -> (Z.t * Z.t) Utils_core.Bot.with_bot
Sourceval bwd_of_z_up : Z.t -> Z.t -> t -> (Z.t * Z.t) Utils_core.Bot.with_bot
Sourceval bwd_of_z_down : Z.t -> Z.t -> t -> (Z.t * Z.t) Utils_core.Bot.with_bot
Sourceval bwd_of_z_zero : Z.t -> Z.t -> t -> (Z.t * Z.t) Utils_core.Bot.with_bot
Sourceval bwd_of_z_any : Z.t -> Z.t -> t -> (Z.t * Z.t) Utils_core.Bot.with_bot
Sourceval bwd_of_z_noround : Z.t -> Z.t -> t -> (Z.t * Z.t) Utils_core.Bot.with_bot

Backward conversion from int.

Sourceval bwd_to_z : Z.t -> Z.t -> t -> t_with_bot

Backward conversion to int.

Sourceval meet_nonzero : t -> t_with_bot

Keeps only non-zero elements.

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