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.terms/Terms/Condition/ConditionDom/index.html

Module Condition.ConditionDomSource

This uses the structure of the dominator tree as conditions. It observes the fact that we never perform intersection on arbitrary conditions, as conditions represent set of paths, we either assume a new condition or join existing ones.

This works together with skiplist.ml (fast implementation of useful algorithms like online nearest_common_ancestor) and treemap.ml (mapping from tree relations to lattices).

It is a good candidate for introducing scopes and getting rid of Cudd. Still, when I tested these conditions with Domain_non_relational, it worked for most benchmarks, but the performance gains were not fantastic compared to cudd (sometimes less time, some times more; sometimes a lot less memory, but sometimes more).

Sourcemodule Literal : sig ... end
Sourcemodule Path : sig ... end
Sourcetype t =
  1. | False
  2. | Literal of Literal.t
  3. | Path of Path.t
  4. | Complement of t
Sourceval hash : t -> int
Sourceval pretty : Format.formatter -> t -> unit
Sourceval equal : t -> t -> bool
Sourceval _equal : t -> t -> bool
Sourceval var : unit -> t
Sourceval empty : t
Sourceval all : t
Sourceval one : t
Sourceval complement : t -> t
Sourceval (!~) : t -> t
Sourceval is_included : t -> t -> bool
Sourceval union : t -> t -> t
Sourceval (||~) : t -> t -> t
Sourceval nearest_common_ancestor : t -> t -> t
Sourceval is_prefix : t -> t -> bool
Sourceval inter : t -> t -> t
Sourceval (&&~) : t -> t -> t
Sourceval is_empty : t -> bool
Sourceval disjoint : t -> t -> bool
Sourcemodule Log : sig ... end