Module Abstract_domains.Bools

Copyright © Inria 2023-2024

Abstract domain for boolean values, i.e., subsets of \{\mathrm{true},\mathrm{false}\}

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 is_top : t -> bool

Tests whether this is the top element

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 singleton : bool -> t

singleton b represents the singleton set \{b\}