package mopsa
Install
dune-project
Dependency
Authors
Maintainers
Sources
md5=37966e98ffeebcedc09bd6e9b2b81f69
sha512=40d4d826c25f680766c07eccbabdf5e8a4fa023016e8a164e4e4f6b3781c8484dc4df437055721dfd19b9db8fb7fe3b61236c4833186d346fc7204a68d01eaaa
doc/mopsa.mopsa_utils/Mopsa_utils/ItvUtils/IntItv/index.html
Module ItvUtils.IntItv
IntItv - Intervals for arbitrary precision integers.
We rely on Zarith for arithmetic operations, and IntBounds to represent unbounded intervals.
module B = ItvUtils.IntBound
Types
type t_with_bot = t Core.Bot.with_bot
The type of possibly empty intervals.
val is_valid : t -> bool
Constructors
val of_int : int -> int -> t
val of_int64 : int64 -> int64 -> t
Constructs a non-empty interval.
val of_float : float -> float -> t
Constructs a non-empty interval.
val of_bound_bot : B.t -> B.t -> t_with_bot
val of_range_bot : Z.t -> Z.t -> t_with_bot
val of_int_bot : int -> int -> t_with_bot
val of_int64_bot : int64 -> int64 -> t_with_bot
Constructs a possibly empty interval.
val of_float_bot : float -> float -> t_with_bot
Constructs a possibly empty interval.
val cst_int : int -> t
val cst_int64 : int64 -> t
val zero : t
0,0
val one : t
1,1
val mone : t
-1,-1
val zero_one : t
0,1
val mone_zero : t
-1,0
val mone_one : t
-1,1
val zero_inf : t
0,+∞
val minf_zero : t
-∞,0
val minf_inf : t
-∞,+∞
val unsigned : int -> t
val unsigned8 : t
val unsigned16 : t
val unsigned32 : t
val unsigned64 : t
Intervals of unsigned integers with the specified bitsize.
val signed : int -> t
val signed8 : t
val signed16 : t
val signed32 : t
val signed64 : t
Intervals of two compement's integers with the specified bitsize.
Predicates
val equal_bot : t_with_bot -> t_with_bot -> bool
val included_bot : t_with_bot -> t_with_bot -> bool
val intersect_bot : t_with_bot -> t_with_bot -> bool
A total ordering (lexical ordering) returning -1, 0, or 1. Can be used as compare for sets, maps, etc.
val compare_bot : t Core.Bot.with_bot -> t Core.Bot.with_bot -> int
Total ordering on possibly empty intervals.
val contains_zero : t -> bool
a,b
contains 0.
val contains_one : t -> bool
a,b
contains 1.
val contains_nonzero : t -> bool
a,b
contains a non-zero value.
val is_zero : t -> bool
val is_one : t -> bool
val is_positive : t -> bool
val is_negative : t -> bool
val is_positive_strict : t -> bool
val is_negative_strict : t -> bool
val is_nonzero : t -> bool
Interval sign.
val is_singleton : t -> bool
a,b
contains a single element.
val is_bounded : t -> bool
a,b
has finite bounds.
val is_minf_inf : t -> bool
a,b
represents -∞,+∞
.
Printing
val to_string : t -> string
val print : out_channel -> t -> unit
val fprint : Format.formatter -> t -> unit
val to_string_bot : t Core.Bot.with_bot -> string
val print_bot : out_channel -> t Core.Bot.with_bot -> unit
val fprint_bot : Format.formatter -> t Core.Bot.with_bot -> unit
val bprint_bot : Buffer.t -> t Core.Bot.with_bot -> unit
Enumeration
List of elements, in increasing order. Raises an invalid argument if it is unbounded.
Set operations
val join_bot : t_with_bot -> t_with_bot -> t_with_bot
Join of possibly empty intervals.
val join_list : t list -> t_with_bot
Join of a list of (non-empty) intervals.
val meet : t -> t -> t_with_bot
Intersection of non-emtpty intervals (possibly empty)
val meet_bot : t_with_bot -> t_with_bot -> t_with_bot
Intersection of possibly empty intervals.
val meet_list : t list -> t_with_bot
Meet of a list of (non-empty) intervals.
val widen_bot : t_with_bot -> t_with_bot -> t_with_bot
val positive : t -> t_with_bot
val negative : t -> t_with_bot
Positive and negative part.
val meet_zero : t -> t_with_bot
Intersects with
.
val meet_nonzero : t -> t_with_bot
Keeps only non-zero elements.
Forward operations
Given one or two interval argument(s), return the interval result.
Division (with truncation). Returns a list of 0, 1, or 2 intervals to remain precise.
Euclidian division (towards -oo). Returns a list of 0, 1, or 2 intervals to remain precise.
val div : t -> t -> t_with_bot
Division (with truncation). Returns a single (possibly empty) overapproximating interval.
val ediv : t -> t -> t_with_bot
Division (euclidian, towards -oo) Returns a single (possibly empty) overapproximating interval.
val rem : t -> t -> t_with_bot
Remainder. Uses the C semantics for remainder (%).
val erem : t -> t -> t_with_bot
Euclidian remainder. rounding towards -oo
Put back the interval inside lo,up
by modular arithmetics. Useful to model the effect of arithmetic or conversion overflow.
val to_bool : bool -> bool -> t
Conversion from integer to boolean in 0,1
: maps 0 to 0 (false) and non-zero to 1 (true).
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.
Bit operations
val shift_left : t -> t -> t_with_bot
Bitshift left: multiplication by a power of 2.
val shift_right : t -> t -> t_with_bot
Bitshift right: division by a power of 2 rounding towards -∞.
val shift_right_trunc : t -> t -> t_with_bot
Unsigned bitshift right: division by a power of 2 with truncation.
Internal functions
Interval functions, based on the previous ones
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_default_unary : t -> t -> t_with_bot
Fallback for backward unary operators
Fallback for backward binary operators
val bwd_neg : t -> t -> t_with_bot
val bwd_abs : t -> t -> t_with_bot
val bwd_succ : t -> t -> t_with_bot
val bwd_pred : t -> t -> t_with_bot
val bwd_bit_not : t -> t -> t_with_bot
Backward join: both arguments are intersected with the result.
val bwd_wrap : t -> (Z.t * Z.t) -> t -> t_with_bot
val pos_mod : ItvUtils.IntBound.t -> ItvUtils.IntBound.t -> ItvUtils.IntBound.t