Parameter Tree_block.MemVal

type t
val pp : Stdlib.Format.formatter -> t -> unit
val merge : left:t -> right:t -> t

Merges two children node into a single node; returns the merged node. Note children of the node are always preserved too, for further accesses.

val split : at:sint -> t -> ((t, sint) Soteria__Sym_states__Tree_block.Split_tree.t * (t, sint) Soteria__Sym_states__Tree_block.Split_tree.t) CSYMEX.t

split ~at node Splits node at at, which is the relative offset within the node. Returns the left and right split trees, which themselves may contain further splits.

at is guaranteed to be in the range [1, size(node)), i.e. strictly within the node.

type syn
val ins_outs : syn -> CSYMEX.Value.Expr.t list * CSYMEX.Value.Expr.t list
val pp_syn : Stdlib.Format.formatter -> syn -> unit
val to_syn : t -> syn Stdlib.Seq.t option

Serialize this memory value; either returns Some syn, or None to signal the children must instead be serialized instead.

val consume : syn -> (t, sint) Soteria__Sym_states__Tree_block.tree -> ((t, sint) Soteria__Sym_states__Tree_block.tree, syn list) CSYMEX.Consumer.t

Extract the given syn predicate from the tree; this may result in an empty (NotOwned Totally) tree, or may only modify part of the tree if the predicate only represents part of this tree's state. A Missing may be raised if part of the state is missing for the consumption to succeed.

The input tree corresponds to the subtree relevant to the predicate's offset and length, meaning t.node is the node covering the whole predicate's range.

val produce : syn -> (t, sint) Soteria__Sym_states__Tree_block.tree -> (t, sint) Soteria__Sym_states__Tree_block.tree CSYMEX.Producer.t

Add the given syn predicate onto the given tree; the input tree is not necessarily empty (NotOwned Totally), and if the predicate overlaps the production may vanish.

The input tree corresponds to the subtree relevant to the predicate's offset and length, meaning t.node is the node covering the whole predicate's range.

val assert_exclusively_owned : t -> (unit, 'err, syn list) CSYMEX.Result.t

Returns ok if this memory value is exclusively owned, ie no additional state can be composed with it; in other words, calling produce on a tree with this node must always vanish. Otherwise this should raise a miss with the fixes needed for this to become exclusively owned.