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.fixpoint/Fixpoint/Wto_iteration/WTOFixpoint/CLMap/BaseMap/WithForeign/index.html

Module BaseMap.WithForeignSource

Operation with maps/set of different types. Map2 must use the same KEY.to_int function.

Parameters

module Map2 : PatriciaTree.NODE_WITH_FIND with type 'a key = 'a key

Signature

Sourcetype ('map1, 'map2) polyinter_foreign = {
  1. f : 'a. 'a key -> ('a, 'map1) value -> ('a, 'map2) Map2.value -> ('a, 'map1) value;
}
Sourceval nonidempotent_inter : ('a, 'b) polyinter_foreign -> 'a t -> 'b Map2.t -> 'a t

Like BASE_MAP.idempotent_inter. Tries to preserve physical equality on the first argument when possible.

Sourcetype ('map2, 'map1) polyfilter_map = {
  1. f : 'a. 'a key -> ('a, 'map2) Map2.value -> ('a, 'map1) value option;
}
Sourceval filter_map_no_share : ('map2, 'map1) polyfilter_map -> 'map2 Map2.t -> 'map1 t

Like BASE_MAP.filter_map_no_share, but allows to transform a foreigh map into the current one.

Sourcetype ('map1, 'map2) polyupdate_multiple = {
  1. f : 'a. 'a key -> ('a, 'map1) value option -> ('a, 'map2) Map2.value -> ('a, 'map1) value option;
}
Sourceval update_multiple_from_foreign : 'b Map2.t -> ('a, 'b) polyupdate_multiple -> 'a t -> 'a t

This is equivalent to multiple calls to update, but more efficient. update_multiple_from_foreign m_from f m_to is the same as calling update k {f=fun v_to -> f.f k v_to v_from} m_to on all bindings (k, v_from) of m_from, i.e. update_multiple_from_foreign m_from f m_to calls f.f on every key of m_from, says if the corresponding value also exists in m_to, and adds or remove the element in m_to depending on the value of f.f. f.f is called in the unsigned order of KEY.to_int. O(size(m_from) + size(m_to)) complexity.

Sourcetype ('map1, 'map2, 'map3) polyupdate_multiple_inter = {
  1. f : 'a. 'a key -> ('a, 'map1) value -> ('a, 'map2) Map2.value -> ('a, 'map3) value option;
}
Sourceval update_multiple_from_inter_with_foreign : 'b Map2.t -> ('a, 'b, 'a) polyupdate_multiple_inter -> 'a t -> 'a t

update_multiple_from_inter_with_foreign m_from f m_to is the same as update_multiple_from_foreign, except that instead of updating for all keys in m_from, it only updates for keys that are both in m_from and m_to.

Sourcetype ('map1, 'map2) polydifference = ('map1, 'map2, 'map1) polyupdate_multiple_inter
Sourceval difference : ('a, 'b) polydifference -> 'a t -> 'b Map2.t -> 'a t

difference f map1 map2 returns the map containing the bindings of map1 that aren't in map2. For keys present in both maps but with different values, f.f is called. If it returns Some v, then binding k,v is kept, else k is dropped.

f.f is called in the unsigned order of KEY.to_int.

This is the same as BASE_MAP.difference but allows the second map to be of a different type.

  • since v0.11.0
Sourcetype ('a, 'b) key_value_value =
  1. | KeyValueValue : 'k key * ('k, 'a) value * ('k, 'b) Map2.value -> ('a, 'b) key_value_value

Existential wrapper for a key with two values

  • since v0.11.0
Sourceval min_binding_inter : 'a t -> 'b Map2.t -> ('a, 'b) key_value_value option

min_binding_inter m1 m2 is the minimal binding of the intersection. I.E. the KeyValueValue(k,v1,v2) such that (k,v1) is in m1, (k,v2) is in m2, and k is minimal using the unsigned order on keys.

Returns None if and only if the intersection is empty.

It is rougthly equivalent to calling unsigned_min_binding on nonindempotent_inter f m1 m2, but can be faster.

  • since v0.11.0
Sourceval max_binding_inter : 'a t -> 'b Map2.t -> ('a, 'b) key_value_value option

max_binding_inter m1 m2 is the same as min_binding_inter, but returns the maximum key instead of the minimum.

  • since v0.11.0