package codex

  1. Overview
  2. Docs
The Codex library for building static analysers based on abstract interpretation

Install

dune-project
 Dependency

Authors

Maintainers

Sources

1.0-rc4.tar.gz
md5=bc7266a140c6886add673ede90e335d3
sha512=8da42c0ff2c1098c5f9cb2b5b43b306faf7ac93b8f5ae00c176918cee761f249ff45b29309f31a05bbcf6312304f86a0d5a000eb3f1094d3d3c2b9b4c7f5c386

doc/codex.fixpoint/Fixpoint/Fixpoint_wto/Make/argument-1-G/ControlLocation/index.html

Module G.ControlLocation

type t

The type of keys.

It is recommended to use immutable keys. If keys are mutable, any mutations to keys must preserve to_int. Failing to do so will break the patricia trees' invariants.

val to_int : t -> int

A unique identifier for values of the type. Usually, we use a fresh counter that is increased to give a unique id to each object. Correctness of the operations requires that different values in a tree correspond to different integers.

Must be injective, and ideally fast. hash-consing keys is a good way to generate such unique identifiers.

Note that since Patricia Trees use unsigned order, negative keys are seen as bigger than positive keys. Be wary of this when using negative keys combined with functions like unsigned_max_binding and pop_unsigned_maximum.