Module Abstract_domains.Interval

Copyright © Inria 2023-2024

Abstract domain of intervals over integers (for testing purposes only). Integer over- and under-flows are not supported.

include Sigs.ABSTRACT_DOMAIN
type t

Type of abstract values

val bot : t

The bottom element \bot (most precise element)

val is_bot : t -> bool

Tests whether an element is \bot

val top : t

The top element \top (less precise element)

val leq : t -> t -> bool

Inclusion test between abstract values. Smaller elements are more precise; larger elements are less precise. This might not be a total order, and might not be anti-symmetric either.

val join : t -> t -> t

Abstract union of abstract values. This need not be the least upper bound for leq, nor an upper bound at all.

val widen : t -> t -> t

Widening operator, i.e., an approximation of the concrete union, that is used the ensure the convergence of Kleene-based iterations.

val meet : t -> t -> t

Abstract intersection of abstract values. This need not be the greatest lower bound for leq, nor a lower bound at all.

val pp : Stdlib.Format.formatter -> t -> unit

Pretty-printer for abstract values

val compare : t -> t -> int

Total order

val equal : t -> t -> bool

Syntactic equality

val hash_fold : Base.Hash.state -> t -> Base.Hash.state

Hashing

val is_top : t -> bool

Tests whether an interval is the largest interval

val singleton : int -> t

singleton n represents the singleton set \{n\}

val make : IntBar.t -> IntBar.t -> t

make l u is the interval [l,u]

val is_singleton : t -> bool

Tests whether an interval contains exactly one element

val plus : t -> t -> t

Transfer function for addition

val minus : t -> t -> t

Transfer function for subtraction

val mult : t -> t -> t

Transfer function for multiplication

val lower_bound : t -> IntBar.t

Extracts the lower bound of an interval. Returns +\infty if the interval is empty.

val upper_bound : t -> IntBar.t

Extracts the upper bound of an interval. Returns -\infty if the interval is empty.

val le : t -> t -> Bools.t

Transfer function for the "lesser or equal" arithmetic test

val lt : t -> t -> Bools.t

Transfer function for the "lesser than" arithmetic test

val eq : t -> t -> Bools.t

Transfer function for the equality arithmetic test