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

Module FloatItv.Double

Intervals with rounding to double.

module FF = F.Double

Arithmetic

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

Addition.

val sub_near : t -> t -> t
val sub_up : t -> t -> t
val sub_down : t -> t -> t
val sub_zero : t -> t -> t
val sub_outer : t -> t -> t
val sub_inner : t -> t -> t_with_bot

Subtraction.

val mul_near : t -> t -> t
val mul_up : t -> t -> t
val mul_down : t -> t -> t
val mul_zero : t -> t -> t
val mul_outer : t -> t -> t
val mul_inner : t -> t -> t_with_bot

Multiplication.

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

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

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

Division. Returns a single interval.

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

Square.

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

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

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

Round to integer.

val unround_int_near : t -> t
val unround_int_up : t -> t
val unround_int_down : t -> t
val unround_int_zero : t -> t
val 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.

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

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

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

Conversion from int.

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

Conversion from int64.

val of_z_near : Z.t -> Z.t -> t
val of_z_up : Z.t -> Z.t -> t
val of_z_down : Z.t -> Z.t -> t
val of_z_zero : Z.t -> Z.t -> t
val of_z_outer : Z.t -> Z.t -> t
val 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.

val filter_leq : t -> t -> (t * t) Core.Bot.with_bot
val filter_geq : t -> t -> (t * t) Core.Bot.with_bot
val filter_lt : t -> t -> (t * t) Core.Bot.with_bot
val filter_gt : t -> t -> (t * t) Core.Bot.with_bot
val filter_eq : t -> t -> (t * t) Core.Bot.with_bot
val filter_neq : t -> t -> (t * t) 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.

val bwd_add : t -> t -> t -> (t * t) Core.Bot.with_bot
val bwd_add_near : t -> t -> t -> (t * t) Core.Bot.with_bot
val bwd_add_up : t -> t -> t -> (t * t) Core.Bot.with_bot
val bwd_add_down : t -> t -> t -> (t * t) Core.Bot.with_bot
val bwd_add_zero : t -> t -> t -> (t * t) Core.Bot.with_bot
val bwd_add_any : t -> t -> t -> (t * t) Core.Bot.with_bot
val bwd_add_noround : t -> t -> t -> (t * t) Core.Bot.with_bot

Backward addition.

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

Backward subtraction.

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

Backward multiplication.

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

Backward division.

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

Backward rounding to int.

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

Backward rounding from real.

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

Backward square.

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

Backward square root.

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

Backward conversion from int.

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

Backward conversion to int.

val meet_nonzero : t -> t_with_bot

Keeps only non-zero elements.