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.fixpoint/Fixpoint/Fixpoint_wto/Make/argument-2-D/index.html

Parameter Make.D

type state

An abstract domain is a lattice representing abstract states state.

type transition = G.transition

The syntax for transiton between program points.

type loop_id

An identifier for the loop id. Can be unit if unused; it can be used as a widening ID in the symbolic expression domain (Lemerre, POPL'23; Lesbre & Lemerre, PLDI'24).

val copy : state -> state

Create an independant copy of the state, not sharing any mutable data

val join : state -> state -> state

Standard join operation, over-approximating union.

val fixpoint_step : loop_id:loop_id -> state -> state -> state * bool

fixpoint_step ~loop_id previous next detects whether fixpoint computation is over (then it returns true and the final abstract state), or it tries to extrapolates (widen) from the evolution from previous to next (returning false and an widened state).

val transfer : transition -> state -> state option

Standard transfer function. The transition returns None if the state is bottom

val pp : Format.formatter -> state -> unit

Pretty printer used for debugging.

val enter_loop : state -> state * loop_id

Enter loop, providing a new identifier for the loop.

val leave_loop : state -> state

Leave loop; useful e.g. for induction variable analysis, that introduces variable counting the number of loop iterations.