Module Single_value_abstractionSource

A Single-value abstraction consists of Operator over Lattices.

There are two kinds of transfer functions:

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

Sourcemodule Sig : sig ... end

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

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

Sourcemodule Quadrivalent : sig ... end

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

Sourcemodule Ival : sig ... end

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

Sourcemodule 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.

Sourcemodule Known_bits : sig ... end

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

Sourcemodule 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.

Sourcemodule Log : sig ... end

Automatically log the calls to a basis in the trace.

Sourcemodule Stats : sig ... end

Automatically computes stats about the number of calls.