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/Equality/Action/index.html

Module Equality.ActionSource

Parameters

module B : sig ... end

Signature

type bitvector = B.bitvector
type integer = B.integer
type boolean = B.boolean
type enum = B.enum
Sourcetype ('a, 'b) relation = ('a, 'b) t

One-to-one correspodance between value types and term types

Sourcetype 'term wrapper =
  1. | Wrap : ('value * ('value, 'term) mapping) -> 'term wrapper

Existential wrapper for mappings

Sourceval apply_relation : 'value_parent -> ('term_child, 'term_parent) relation -> ('value_parent, 'term_parent) mapping -> 'term_child wrapper

apply_relation vp rel proof is the value vc obtained by applying relation rel to value vp. This is a simple forward transfer function.

The proof terms are there to ensure correspondance between the types of values (B.bitvector, B.boolean, B.integer, B.enum) and of terms (TC.bitvector, TC.boolean, TC.integer, TC.enum)

Sourceval refine_relation : 'value_parent -> 'value_child -> ('term_child, 'term_parent) relation -> ('value_parent, 'term_parent) mapping -> ('value_child, 'term_child) mapping -> 'value_parent option

refine_relation ~size vp vc rel proof_p proof_c refines the value vp into, using knowledge that applying rel to vp must be in vc. This is a simple backward transfer function. None is returned when no new information can be deduced.

Note: this returns the newly learned value. It should be intersected with vp for best precision.

The proof terms are there to ensure correspondance between the types of values (B.bitvector, B.boolean, B.integer, B.enum) and of terms (TC.bitvector, TC.boolean, TC.integer, TC.enum)