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.whilelib/Whilelib/Analysis_sva/State/BaseMap/index.html

Module State.BaseMapSource

Sourcetype _ key = key
Sourcetype (!'a, 'b) value = ('a, 'b value) PatriciaTree.snd
Sourcetype 'a t = 'a t
Sourceval empty : 'map t
Sourceval leaf : 'key key -> ('key, 'map) value -> 'map t
Sourceval branch : prefix:int -> branching_bit:int -> tree0:'map t -> tree1:'map t -> 'map t
Sourcetype !'map view = private
  1. | Empty : 'map0 view
  2. | Branch : {
    1. prefix : int;
    2. branching_bit : int;
    3. tree0 : 'map1 t;
    4. tree1 : 'map1 t;
    } -> 'map1 view
  3. | Leaf : {
    1. key : 'key key;
    2. value : ('key, 'map2) value;
    } -> 'map2 view
Sourceval is_empty : 'map t -> bool
Sourceval view : 'a t -> 'a view
Sourceval find : 'key key -> 'map t -> ('key, 'map) value
Sourceval find_opt : 'key key -> 'map t -> ('key, 'map) value option
Sourcetype !'map key_value_pair =
  1. | KeyValue : 'a key * ('a, 'map0) value -> 'map0 key_value_pair
Sourceval unsigned_min_binding : 'a t -> 'a key_value_pair
Sourceval unsigned_max_binding : 'a t -> 'a key_value_pair
Sourceval singleton : 'a key -> ('a, 'b) value -> 'b t
Sourceval cardinal : 'a t -> int
Sourceval is_singleton : 'a t -> 'a key_value_pair option
Sourceval mem : 'key key -> 'map t -> bool
Sourceval remove : 'key key -> 'map t -> 'map t
Sourceval pop_unsigned_minimum : 'map t -> ('map key_value_pair * 'map t) option
Sourceval pop_unsigned_maximum : 'map t -> ('map key_value_pair * 'map t) option
Sourceval insert : 'a key -> (('a, 'map) value option -> ('a, 'map) value) -> 'map t -> 'map t
Sourceval update : 'a key -> (('a, 'map) value option -> ('a, 'map) value option) -> 'map t -> 'map t
Sourceval add : 'key key -> ('key, 'map) value -> 'map t -> 'map t
Sourceval split : 'key key -> 'map t -> 'map t * ('key, 'map) value option * 'map t
Sourcetype (!'map, !'res) polyfold = {
  1. f : 'a. 'a key -> ('a, 'map) value -> 'res;
}
Sourceval iter : ('map, unit) polyfold -> 'map t -> unit
Sourceval fold : ('map, 'acc -> 'acc) polyfold -> 'map t -> 'acc -> 'acc
Sourcetype (!'acc, !'map1, !'map2) polyfold2_inter = {
  1. f : 'a. 'a key -> ('a, 'map1) value -> ('a, 'map2) value -> 'acc -> 'acc;
}
Sourceval fold_on_nonequal_inter : ('acc, 'map1, 'map2) polyfold2_inter -> 'map1 t -> 'map2 t -> 'acc -> 'acc
Sourceval fold_on_inter : ('acc, 'map1, 'map2) polyfold2_inter -> 'map1 t -> 'map2 t -> 'acc -> 'acc
Sourcetype (!'map1, !'map2, !'res) polyfold2 = {
  1. f : 'a. 'a key -> ('a, 'map1) value option -> ('a, 'map2) value option -> 'res;
}
Sourceval fold_on_nonequal_union : ('map1, 'map2, 'acc -> 'acc) polyfold2 -> 'map1 t -> 'map2 t -> 'acc -> 'acc
Sourceval fold_on_union : ('map1, 'map2, 'acc -> 'acc) polyfold2 -> 'map1 t -> 'map2 t -> 'acc -> 'acc
Sourcetype !'map polypredicate = {
  1. f : 'a. 'a key -> ('a, 'map) value -> bool;
}
Sourceval filter : 'map polypredicate -> 'map t -> 'map t
Sourceval for_all : 'map polypredicate -> 'map t -> bool
Sourcetype (!'map1, !'map2) polymap = {
  1. f : 'a. ('a, 'map1) value -> ('a, 'map2) value;
}
Sourceval map : ('map, 'map) polymap -> 'map t -> 'map t
Sourceval map_no_share : ('map1, 'map2) polymap -> 'map1 t -> 'map2 t
Sourcetype (!'map1, !'map2) polymapi = {
  1. f : 'a. 'a key -> ('a, 'map1) value -> ('a, 'map2) value;
}
Sourceval mapi : ('map, 'map) polymapi -> 'map t -> 'map t
Sourceval mapi_no_share : ('map1, 'map2) polymapi -> 'map1 t -> 'map2 t
Sourcetype (!'map1, !'map2) polyfilter_map = {
  1. f : 'a. 'a key -> ('a, 'map1) value -> ('a, 'map2) value option;
}
Sourceval filter_map : ('map, 'map) polyfilter_map -> 'map t -> 'map t
Sourceval filter_map_no_share : ('map1, 'map2) polyfilter_map -> 'map1 t -> 'map2 t
Sourcetype !'map polypretty = {
  1. f : 'a. Format.formatter -> 'a key -> ('a, 'map) value -> unit;
}
Sourceval pretty : ?pp_sep:??? -> 'map polypretty -> Format.formatter -> 'map t -> unit
Sourcetype (!'map1, !'map2) polysame_domain_for_all2 = {
  1. f : 'a. 'a key -> ('a, 'map1) value -> ('a, 'map2) value -> bool;
}
Sourceval reflexive_same_domain_for_all2 : ('map, 'map) polysame_domain_for_all2 -> 'map t -> 'map t -> bool
Sourceval nonreflexive_same_domain_for_all2 : ('map1, 'map2) polysame_domain_for_all2 -> 'map1 t -> 'map2 t -> bool
Sourceval reflexive_subset_domain_for_all2 : ('map, 'map) polysame_domain_for_all2 -> 'map t -> 'map t -> bool
Sourceval nonreflexive_subset_domain_for_all2 : ('map1, 'map2) polysame_domain_for_all2 -> 'map1 t -> 'map2 t -> bool
Sourcetype (!'map1, !'map2) polyfor_all2 = {
  1. f : 'a. 'a key -> ('a, 'map1) value option -> ('a, 'map2) value option -> bool;
}
Sourceval reflexive_any_domain_for_all2 : ('map1, 'map2) polyfor_all2 -> 'map1 t -> 'map2 t -> bool
Sourceval nonreflexive_any_domain_for_all2 : ('map1, 'map2) polyfor_all2 -> 'map1 t -> 'map2 t -> bool
Sourcetype !'map polycompare = {
  1. f : 'a. 'a key -> ('a, 'map) value -> ('a, 'map) value -> int;
}
Sourceval reflexive_compare : 'a polycompare -> 'a t -> 'a t -> int
Sourceval disjoint : 'a t -> 'a t -> bool
Sourcetype (!'map1, !'map2, !'map3) polyunion = {
  1. f : 'a. 'a key -> ('a, 'map1) value -> ('a, 'map2) value -> ('a, 'map3) value;
}
Sourceval idempotent_union : ('a, 'a, 'a) polyunion -> 'a t -> 'a t -> 'a t
Sourceval nonidempotent_union : ('a, 'a, 'a) polyunion -> 'a t -> 'a t -> 'a t
Sourcetype (!'map1, !'map2, !'map3) polyinter = {
  1. f : 'a. 'a key -> ('a, 'map1) value -> ('a, 'map2) value -> ('a, 'map3) value;
}
Sourceval idempotent_inter : ('a, 'a, 'a) polyinter -> 'a t -> 'a t -> 'a t
Sourceval nonidempotent_inter_no_share : ('a, 'b, 'c) polyinter -> 'a t -> 'b t -> 'c t
Sourcetype (!'map1, !'map2, !'map3) polyinterfilter = {
  1. f : 'a. 'a key -> ('a, 'map1) value -> ('a, 'map2) value -> ('a, 'map3) value option;
}
Sourceval idempotent_inter_filter : ('a, 'a, 'a) polyinterfilter -> 'a t -> 'a t -> 'a t
Sourceval nonidempotent_inter_filter_no_share : ('a, 'b, 'c) polyinterfilter -> 'a t -> 'b t -> 'c t
Sourcetype (!'map1, !'map2, !'map3) polymerge = {
  1. f : 'a. 'a key -> ('a, 'map1) value option -> ('a, 'map2) value option -> ('a, 'map3) value option;
}
Sourceval slow_merge : ('map1, 'map2, 'map3) polymerge -> 'map1 t -> 'map2 t -> 'map3 t
Sourcetype (!'a, !'b) polydifference = ('a, 'b, 'a) polyinterfilter
Sourceval symmetric_difference : ('a, 'a) polydifference -> 'a t -> 'a t -> 'a t
Sourceval difference : ('a, 'a) polydifference -> 'a t -> 'a t -> 'a t
Sourcetype (!'a, !'b) key_value_value =
  1. | KeyValueValue : 'k key * ('k, 'a0) value * ('k, 'b0) value -> ('a0, 'b0) key_value_value
Sourceval min_binding_inter : 'a t -> 'b t -> ('a, 'b) key_value_value option
Sourceval max_binding_inter : 'a t -> 'b t -> ('a, 'b) key_value_value option
Sourceval to_seq : 'a t -> 'a key_value_pair Seq.t
Sourceval to_rev_seq : 'a t -> 'a key_value_pair Seq.t
Sourceval add_seq : 'a key_value_pair Seq.t -> 'a t -> 'a t
Sourceval of_seq : 'a key_value_pair Seq.t -> 'a t
Sourceval of_list : 'a key_value_pair list -> 'a t
Sourceval to_list : 'a t -> 'a key_value_pair list
Sourcemodule WithForeign (Map2 : sig ... end) : sig ... end