Module Single_value_abstraction

A Single-value abstraction consists of Operator over Lattices.

There are two kinds of transfer functions:

• Forward transfer functions take lattice as arguments and returns a lattice as result;
• Backward transfer functions take lattice as arguments, a lattice as the known result, and returns a new version of the arguments that match the result and other argument values.

The transfer functions are multi-sorted, and we have an implicit order on the types:

• Boolean values are standalone;
• Enum values depend on boolean;
• Integer values depend on boolean;
• Bitvector values depend on boolean (it could also depend on integer).
• (Block and Memory are currently not used).

module Sig : sig ... end

The signature of all single-value abstractions. Start here.

A basic abstraction, featuring only transfer function over abstract booleans.

module Quadrivalent : sig ... end

The lattice for four-valued boolean logic. It represents the powerset of {true,false}. See Lattices.Quadrivalent.

module Ival : sig ... end

Our main bitvector abstraction: interval and congruence abstraction, for both the signed and unsigned interpretation of bitvectors.

module Bitfield : sig ... end

The most precise abstraction for finite enumerations: a bitfield, with a bit for each possible value, compactly representing a set of values.

module Known_bits : sig ... end

A bitvector abstraction representing information known about the known and unknown bits.

module Dummy : sig ... end

Code when you need new transfer functions that fail when they are called. Start here when you implement a new single-value abstraction.

module Log : sig ... end

Automatically log the calls to a basis in the trace.

module Stats : sig ... end

Automatically computes stats about the number of calls.