package soteria

  1. Overview
  2. Docs
package soteria
Legend:
Page
Library
Module
Module type
Parameter
Class
Class type
Source

Module Make.Tree

type t = (MemVal.t, sint) tree
val pp : t Fmt.t
val node_merge : MemVal.t node -> MemVal.t node -> MemVal.t node
val make : node:'a -> range:('b * 'b) -> ?children:??? -> unit -> ('a, 'b) Soteria.Data.Range_tree.t
val is_empty : ('a node, 'b) Soteria.Data.Range_tree.t -> bool
val not_owned : ('a * 'a) -> ('b node, 'a) Soteria.Data.Range_tree.t
val iter_leaves_rev : ('a, 'b) Soteria.Data.Range_tree.t -> (('a, 'b) Soteria.Data.Range_tree.t -> unit) -> unit
val map_leaves : ('a -> ('a, 'b, 'c) Symex.Result.t) -> ('a, 'd) Soteria.Data.Range_tree.t -> (('a, 'd) Soteria.Data.Range_tree.t, 'b, 'c) Symex.Result.t
val with_children : ('a, 'b) Soteria.Data.Range_tree.t -> left:('a, 'b) Soteria.Data.Range_tree.t -> right:('a, 'b) Soteria.Data.Range_tree.t -> ('a, 'b) Soteria.Data.Range_tree.t Symex.t

Like of_children, but doesn't attempt merging the children, i.e. assumes that the intermediary node that is in t is still correct for the new children. This is faster than of_children but is only sound if the children's content did not change.

Converts a Split_tree of Nodes (ie. a tree with no base) into a Tree, reconstructing each node's range and constructing intermediary nodes.

Converts the given Tree into a Split_tree, ignoring intermediary nodes and erasing offset information.

split ~range t isolates range from t. Precondition: range is a strict subrange of t.range (neither empty nor equal to t.range). Returns (node, left, right) where:

  • node is the node covering exactly range
  • left and right can be safely set as t's children, and range lies within either left or right.

If range touches the left or right edge of t, a single split suffices. Otherwise, we first split at fst range to peel off the left part, then carve range out of the resulting right part. This makes the procedure right-biased (it prefers introducing structure on the right)

val extract : t -> Range.t -> (t * t option) Symex.t
module Frame_range (M : sig ... end) : sig ... end
include sig ... end
val (let+) : ('a, 'b, 'c) Soteria.Soteria_std.Compo_res.t Symex.t -> ('a -> 'd) -> ('d, 'b, 'c) Soteria.Soteria_std.Compo_res.t Symex.t
val (let*^) : 'a Symex.t -> ('a -> ('b, 'c, 'd) Soteria.Soteria_std.Compo_res.t Symex.t) -> ('b, 'c, 'd) Soteria.Soteria_std.Compo_res.t Symex.t
val (let+^) : 'a Symex.t -> ('a -> 'b) -> ('b, 'c, 'd) Soteria.Soteria_std.Compo_res.t Symex.t
val put_raw : t -> t -> (unit * t, 'a, 'b) Symex.Result.t

Cons/prod

module Consumer_frame_range : sig ... end
val consume : MemVal.syn -> Range.t -> t -> (t, MemVal.syn list) Symex.Consumer.t
module Producer_frame_range : sig ... end
val produce : MemVal.syn -> Range.t -> t -> t Symex.Producer.t