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/Relations/LinearTwoVarEquality/index.html

Module Relations.LinearTwoVarEqualitySource

Sourcetype (_, _) t = private
  1. | Identity : ('a, 'a) t
  2. | Linear_Equality : {
    1. size : Units.In_bits.t;
    2. f1 : Z.t;
    3. f2 : Z.t;
    4. offset : Z.t;
    } -> (Operator.Function_symbol.bitvector, Operator.Function_symbol.bitvector) t
    (*

    Linear_Equality{f1; f2; offset} represents the relation f1*x + f2*y = offset. For instance {f1=1; f2=-2; offset=8} represents x - 2y = 8 or x = 2y+8 Both f1 and f2 should be non-zero. The upside of storing it this way instead of x = q*y + r is that it avoids having to use rational numbers.

    Invariants:

    • f1 > 0
    • gcd f1 f2 offset = 1
    • We never have f1 = -f2 and offset = 0. That case is represented by Identity.
    *)

Smart constructor, normalizes terms to respect invariants

Destructors for easy access

Sourceval f1 : ('a, 'b) t -> Z.t
Sourceval f2 : ('a, 'b) t -> Z.t
Sourceval offset : ('a, 'b) t -> Z.t
include Union_Find.Parameters.GENERIC_GROUP with type ('a, 'b) t := ('a, 'b) t
include Union_Find.Parameters.GENERIC_MONOID with type ('a, 'b) t := ('a, 'b) t
Sourceval equal : ('a, 'b) t -> ('a, 'b) t -> bool

Equality of relations

Sourceval pretty : Format.formatter -> ('a, 'b) t -> unit

Pretty printer for relations

Sourceval pretty_with_terms : (Format.formatter -> 'tl -> unit) -> 'tl -> (Format.formatter -> 'tr -> unit) -> 'tr -> Format.formatter -> ('a, 'b) t -> unit

pretty_with_terms pp_x x pp_y y rel pretty-prints the relation rel between terms x and y (respectively printed with pp_x and pp_y).

For placeholder variables, use pretty

Sourceval identity : ('a, 'a) t

The identity relation

Sourceval compose : ('b, 'c) t -> ('a, 'b) t -> ('a, 'c) t

Monoid composition, written using the functional convention compose f g is f \circ g. Should be associative, and compatible with identity:

  • For all x, G.compose x G.identity = G.compose G.identity x = x
  • For all x y z, G.compose x (G.compose y z) = G.compose (G.compose x y) z
Sourceval inverse : ('a, 'b) t -> ('b, 'a) t

Group inversion, should verify for all x: G.compose x (G.inverse x) = G.compose (G.inverse x) x = G.identity

Sourcemodule Action (B : Single_value_abstraction.Sig.NUMERIC_ENUM) : GROUP_ACTION with type bitvector = B.bitvector and type integer = B.integer and type boolean = B.boolean and type enum = B.enum and type ('a, 'b) relation = ('a, 'b) t