package codex

You can search for identifiers within the package.

in-package search v0.2.0

The Codex library for building static analysers based on abstract interpretation

Install

dune-project

Dependency

codex.top Edit opam file Versions (1)

Authors

Maintainers

M

Matthieu Lemerre <matthieu.lemerre@cea.fr>

Sources

1.0-rc4.tar.gz

md5=bc7266a140c6886add673ede90e335d3

sha512=8da42c0ff2c1098c5f9cb2b5b43b306faf7ac93b8f5ae00c176918cee761f249ff45b29309f31a05bbcf6312304f86a0d5a000eb3f1094d3d3c2b9b4c7f5c386

doc/codex.domains/Domains/Term_based/Nonrelational/index.html

Module `Term_based.Nonrelational`

module Make
  (Terms : 
    Terms.Sig.TERMS
      with type ('a, 'b) Relation.t = ('a, 'b) Terms.Relations.Equality.t)
  (SVA : Single_value_abstraction.Sig.NUMERIC_ENUM) : 
  Term_based_sig.Domain_S
    with module Query.Boolean_Lattice = SVA.Boolean_Lattice
     and module Query.Integer_Lattice = SVA.Integer_Lattice
     and module Terms = Terms

Simple non-relational abstraction, maps terms to the numeric abstraction provided in SVA. This is for the case where there are no relations between the terms (besides equality).

module MakeUF
  (T : Terms.Sig.TERMS)
  (SVA : Single_value_abstraction.Sig.NUMERIC_ENUM)
  (_ : 
    Terms.Relations.GROUP_ACTION
      with type bitvector = SVA.bitvector
       and type integer = SVA.integer
       and type boolean = SVA.boolean
       and type enum = SVA.enum
       and type ('a, 'b) relation = ('a, 'b) T.Relation.t) : 
  Term_based_sig.DOMAIN_WITH_UNION
    with module Query.Boolean_Lattice = SVA.Boolean_Lattice
     and module Query.Integer_Lattice = SVA.Integer_Lattice
     and module Terms = T

Make the reduced product of a non-relational domain and a labeled union-find. This should then be passed to one of the functions in Union_find, as these are the ones that create relation