Tree (soteria-c.Soteria_c_lib.Csymex.Tree

type t = (MemVal.t, sint) tree

val pp : Stdlib.Format.formatter -> (MemVal.t, 'a CSYMEX.Value.t) tree -> unit

val make : 
  node:'a Soteria__Sym_states__Tree_block.node ->
  range:('b * 'b) ->
  ?children:
    (('a, 'b) Soteria__Sym_states__Tree_block.tree
     * ('a, 'b) Soteria__Sym_states__Tree_block.tree) ->
  unit ->
  ('a, 'b) Soteria__Sym_states__Tree_block.tree

val is_empty : ('a, 'b) tree -> bool

val not_owned : ('a * 'a) -> ('b, 'a) Soteria__Sym_states__Tree_block.tree

val map_leaves : 
  ('a, 'b) tree ->
  (('a, 'b) tree -> (('a, 'b) tree, 'c, 'd) CSYMEX.Result.t) ->
  (('a, 'b) tree, 'c, 'd) CSYMEX.Result.t

val iter_leaves_rev : ('a, 'b) tree -> (('a, 'b) tree -> unit) -> unit

val of_children_s : 
  left:(MemVal.t, 'a) tree ->
  right:(MemVal.t, 'a) tree ->
  (MemVal.t, 'a) tree CSYMEX.t

val of_children : 
  'a ->
  left:(MemVal.t, 'b) tree ->
  right:(MemVal.t, 'b) tree ->
  (MemVal.t, 'b) tree CSYMEX.t

val with_children : 
  ('a, 'b) tree ->
  left:('a, 'b) Soteria__Sym_states__Tree_block.tree ->
  right:('a, 'b) Soteria__Sym_states__Tree_block.tree ->
  ('a, 'b) tree CSYMEX.t

val offset : 
  by:MemVal.S_bounded_int.t CSYMEX.Value.t ->
  ('a, MemVal.S_bounded_int.t CSYMEX.Value.t) tree ->
  ('a, MemVal.S_bounded_int.t CSYMEX.Value.t)
    Soteria__Sym_states__Tree_block.tree

val of_split_tree : 
  (MemVal.S_bounded_int.t CSYMEX.Value.t
   * MemVal.S_bounded_int.t CSYMEX.Value.t) ->
  (MemVal.t Soteria__Sym_states__Tree_block.node,
    MemVal.S_bounded_int.t CSYMEX.Value.t)
    Split_tree.t ->
  (MemVal.t, MemVal.S_bounded_int.t CSYMEX.Value.t) tree CSYMEX.t

val to_split_tree : 
  (MemVal.t, MemVal.S_bounded_int.t CSYMEX.Value.t) tree ->
  (Node.t, sint) Split_tree.t

val split : range:Range.t -> (MemVal.t, sint) tree -> (Node.t * t * t) CSYMEX.t

val extract : t -> Range.t -> (t * t option) CSYMEX.t

val extend_if_needed : 
  ('a, MemVal.S_bounded_int.t CSYMEX.Value.t) tree ->
  (MemVal.S_bounded_int.t CSYMEX.Value.t
   * MemVal.S_bounded_int.t CSYMEX.Value.t) ->
  ('a, MemVal.S_bounded_int.t CSYMEX.Value.t) tree CSYMEX.t

val add_to_the_right : 
  (MemVal.t, sint) tree ->
  (MemVal.t, sint) tree ->
  t CSYMEX.t

val add_to_the_left : 
  (MemVal.t, sint) tree ->
  (MemVal.t, sint) tree ->
  t CSYMEX.t

module Frame_range (M : sig ... end) : sig ... end

val (let*) : 
  ('a, 'b, 'c) Soteria.Symex.Compo_res.t CSYMEX.t ->
  ('a -> ('d, 'b, 'c) Soteria.Symex.Compo_res.t CSYMEX.t) ->
  ('d, 'b, 'c) Soteria.Symex.Compo_res.t CSYMEX.t

val (let+) : 
  ('a, 'b, 'c) Soteria.Symex.Compo_res.t CSYMEX.t ->
  ('a -> 'd) ->
  ('d, 'b, 'c) Soteria.Symex.Compo_res.t CSYMEX.t

val (let*^) : 
  'a CSYMEX.t ->
  ('a -> ('b, 'c, 'd) Soteria.Symex.Compo_res.t CSYMEX.t) ->
  ('b, 'c, 'd) Soteria.Symex.Compo_res.t CSYMEX.t

val (let+^) : 
  'a CSYMEX.t ->
  ('a -> 'b) ->
  ('b, 'c, 'd) Soteria.Symex.Compo_res.t CSYMEX.t

val frame_range : 
  t ->
  replace_node:(t -> (t, 'b, 'c) Soteria.Symex.Compo_res.t CSYMEX.t) ->
  rebuild_parent:
    ((MemVal.t, sint) tree ->
      left:t ->
      right:t ->
      (MemVal.t, sint) tree CSYMEX.t) ->
  Range.t ->
  (t * t, 'b, 'c) Soteria.Symex.Compo_res.t CSYMEX.t

val get_raw : 
  MemVal.S_bounded_int.t CSYMEX.Value.t ->
  MemVal.S_bounded_int.t CSYMEX.Value.t ->
  t ->
  (t * t, 'a, 'b) Soteria.Symex.Compo_res.t CSYMEX.t

val put_raw : t -> t -> (unit * t, 'a, 'b) CSYMEX.Result.t

module Consumer_frame_range : sig ... end

val consume : 
  MemVal.syn ->
  Range.t ->
  t ->
  (t, MemVal.syn list) CSYMEX.Consumer.t

module Producer_frame_range : sig ... end

val produce : MemVal.syn -> Range.t -> t -> t CSYMEX.Producer.t