Module Ctree_block.Node

type qty =
  1. | Partially
  2. | Totally
val pp_qty : Stdlib.Format.formatter -> qty -> unit
val merge_qty : qty -> qty -> qty
type t
val pp : Stdlib.Format.formatter -> MemVal.t Soteria__Sym_states__Tree_block.node -> unit
val is_empty : 'a Soteria__Sym_states__Tree_block.node -> bool
val is_fully_owned : 'a Soteria__Sym_states__Tree_block.node -> bool
val assert_exclusively_owned : MemVal.t Soteria__Sym_states__Tree_block.node -> Cerb_location.t -> ((unit, 'a, MemVal.syn list) Soteria.Symex.Compo_res.t * Cerb_location.t) Soteria__Symex.Make(Soteria.Bv_values.Bv_solver.Z3_solver).t
val merge : left:MemVal.t Soteria__Sym_states__Tree_block.node -> right:MemVal.t Soteria__Sym_states__Tree_block.node -> MemVal.t Soteria__Sym_states__Tree_block.node * bool
val split : at:MemVal.S_bounded_int.t Soteria.Bv_values.Bv_solver.Z3_solver.Value.t -> MemVal.t Soteria__Sym_states__Tree_block.node -> Cerb_location.t -> (((MemVal.t Soteria__Sym_states__Tree_block.node, MemVal.S_bounded_int.t Soteria.Bv_values.Bv_solver.Z3_solver.Value.t) Split_tree.t * (MemVal.t Soteria__Sym_states__Tree_block.node, MemVal.S_bounded_int.t Soteria.Bv_values.Bv_solver.Z3_solver.Value.t) Split_tree.t) * Cerb_location.t) Soteria__Symex.Make(Soteria.Bv_values.Bv_solver.Z3_solver).t