package codex

  1. Overview
  2. Docs
The Codex library for building static analysers based on abstract interpretation

Install 

dune-project
 Dependency

codex.top Edit opam file Versions (1)

Authors

  1. M
    Matthieu Lemerre
  2. J
    Julien Simonnet
  3. O
    Olivier Nicole
  4. P
    Paul Robert
  5. D
    Dorian Lesbre
  6. I
    Iker Canut
  7. C
    Corentin Gendreau
  8. G
    Guillaume Girol
  9. C
    Charles Babu
  10. J
    Jérôme Faucheux

Maintainers

  1. M
    Matthieu Lemerre <matthieu.lemerre@cea.fr>

Sources

1.0-rc4.tar.gz
md5=bc7266a140c6886add673ede90e335d3
sha512=8da42c0ff2c1098c5f9cb2b5b43b306faf7ac93b8f5ae00c176918cee761f249ff45b29309f31a05bbcf6312304f86a0d5a000eb3f1094d3d3c2b9b4c7f5c386

doc/codex.single_value_abstraction/Single_value_abstraction/index.html

Module Single_value_abstractionSource

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