LatticesSourceOur primary way of exchanging and information about the program is using lattices. Lattices should be the abstraction of a set of something (its concretization).
Note that many operations operate over several lattices (notably, transfer functions) are defined in the Single_value_abstraction module. Lattices operation defined here should be concerned only with a single lattice.
TODO: This is probably what we should be exporting for later display.
module Sig : sig ... endSignature for lattices, semi-lattices, and type-specific lattices.
The quadrivalent lattice for booleans, with four elements: Bottom, True, False, and Top.
Product lattice is a lattice that pairs two (or more) component lattices
A bitvector lattice based on “known bits”: tracks which bits are definitely 0 or definitely 1, leaving others unknown.
A lattice of finite sets of bitvectors. Best for small domains where explicit enumeration is feasible.
The congruence lattice: abstracts integers by modular constraints of the form x ≡ a (mod n). Captures properties like even/odd or divisibility.
Signed interval lattice: represents ranges of integers with signed semantics (e.g. -10, 42)