Tree (soteria-c.Soteria_c_lib.Ctree

type t = (MemVal.t, sint) tree

val pp : 
  Stdlib.Format.formatter ->
  (MemVal.t, 'a Soteria.Bv_values.Bv_solver.Z3_solver.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 ->
    Cerb_location.t ->
    ((('a, 'b) tree, 'c, 'd) Soteria.Symex.Compo_res.t * Cerb_location.t)
      Soteria__Symex.Make(Soteria.Bv_values.Bv_solver.Z3_solver).t) ->
  Cerb_location.t ->
  ((('a, 'b) tree, 'c, 'd) Soteria.Symex.Compo_res.t * Cerb_location.t)
    Soteria__Symex.Make(Soteria.Bv_values.Bv_solver.Z3_solver).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 ->
  Cerb_location.t ->
  ((MemVal.t, 'a) tree * Cerb_location.t)
    Soteria__Symex.Make(Soteria.Bv_values.Bv_solver.Z3_solver).t

val of_children : 
  'a ->
  left:(MemVal.t, 'b) tree ->
  right:(MemVal.t, 'b) tree ->
  Cerb_location.t ->
  ((MemVal.t, 'b) tree * Cerb_location.t)
    Soteria__Symex.Make(Soteria.Bv_values.Bv_solver.Z3_solver).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 ->
  Cerb_location.t ->
  (('a, 'b) tree * Cerb_location.t)
    Soteria__Symex.Make(Soteria.Bv_values.Bv_solver.Z3_solver).t

val offset : 
  by:MemVal.S_bounded_int.t Soteria.Bv_values.Bv_solver.Z3_solver.Value.t ->
  ('a, MemVal.S_bounded_int.t Soteria.Bv_values.Bv_solver.Z3_solver.Value.t)
    tree ->
  ('a, MemVal.S_bounded_int.t Soteria.Bv_values.Bv_solver.Z3_solver.Value.t)
    Soteria__Sym_states__Tree_block.tree

val of_split_tree : 
  (MemVal.S_bounded_int.t Soteria.Bv_values.Bv_solver.Z3_solver.Value.t
   * MemVal.S_bounded_int.t Soteria.Bv_values.Bv_solver.Z3_solver.Value.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 ->
  ((MemVal.t,
     MemVal.S_bounded_int.t Soteria.Bv_values.Bv_solver.Z3_solver.Value.t)
     tree
   * Cerb_location.t)
    Soteria__Symex.Make(Soteria.Bv_values.Bv_solver.Z3_solver).t

val to_split_tree : 
  (MemVal.t,
    MemVal.S_bounded_int.t Soteria.Bv_values.Bv_solver.Z3_solver.Value.t)
    tree ->
  (Node.t, sint) Split_tree.t

val split : 
  range:Range.t ->
  (MemVal.t, sint) tree ->
  Cerb_location.t ->
  ((Node.t * t * t) * Cerb_location.t)
    Soteria__Symex.Make(Soteria.Bv_values.Bv_solver.Z3_solver).t

val extract : 
  t ->
  Range.t ->
  Cerb_location.t ->
  ((t * t option) * Cerb_location.t)
    Soteria__Symex.Make(Soteria.Bv_values.Bv_solver.Z3_solver).t

val extend_if_needed : 
  ('a, MemVal.S_bounded_int.t Soteria.Bv_values.Bv_solver.Z3_solver.Value.t)
    tree ->
  (MemVal.S_bounded_int.t Soteria.Bv_values.Bv_solver.Z3_solver.Value.t
   * MemVal.S_bounded_int.t Soteria.Bv_values.Bv_solver.Z3_solver.Value.t) ->
  Cerb_location.t ->
  (('a, MemVal.S_bounded_int.t Soteria.Bv_values.Bv_solver.Z3_solver.Value.t)
     tree
   * Cerb_location.t)
    Soteria__Symex.Make(Soteria.Bv_values.Bv_solver.Z3_solver).t

val add_to_the_right : 
  (MemVal.t, sint) tree ->
  (MemVal.t, sint) tree ->
  Cerb_location.t ->
  (t * Cerb_location.t)
    Soteria__Symex.Make(Soteria.Bv_values.Bv_solver.Z3_solver).t

val add_to_the_left : 
  (MemVal.t, sint) tree ->
  (MemVal.t, sint) tree ->
  Cerb_location.t ->
  (t * Cerb_location.t)
    Soteria__Symex.Make(Soteria.Bv_values.Bv_solver.Z3_solver).t

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

val (let*) : 
  (Cerb_location.t ->
    (('a, 'b, 'c) Soteria.Symex.Compo_res.t * Cerb_location.t)
      Soteria__Symex.Make(Soteria.Bv_values.Bv_solver.Z3_solver).t) ->
  ('a ->
    Cerb_location.t ->
    (('d, 'b, 'c) Soteria.Symex.Compo_res.t * Cerb_location.t)
      Soteria__Symex.Make(Soteria.Bv_values.Bv_solver.Z3_solver).t) ->
  Cerb_location.t ->
  (('d, 'b, 'c) Soteria.Symex.Compo_res.t * Cerb_location.t)
    Soteria__Symex.Make(Soteria.Bv_values.Bv_solver.Z3_solver).t

val (let+) : 
  (Cerb_location.t ->
    (('a, 'b, 'c) Soteria.Symex.Compo_res.t * Cerb_location.t)
      Soteria__Symex.Make(Soteria.Bv_values.Bv_solver.Z3_solver).t) ->
  ('a -> 'd) ->
  Cerb_location.t ->
  (('d, 'b, 'c) Soteria.Symex.Compo_res.t * Cerb_location.t)
    Soteria__Symex.Make(Soteria.Bv_values.Bv_solver.Z3_solver).t

val (let*^) : 
  (Cerb_location.t ->
    ('a * Cerb_location.t)
      Soteria__Symex.Make(Soteria.Bv_values.Bv_solver.Z3_solver).t) ->
  ('a ->
    Cerb_location.t ->
    (('b, 'c, 'd) Soteria.Symex.Compo_res.t * Cerb_location.t)
      Soteria__Symex.Make(Soteria.Bv_values.Bv_solver.Z3_solver).t) ->
  Cerb_location.t ->
  (('b, 'c, 'd) Soteria.Symex.Compo_res.t * Cerb_location.t)
    Soteria__Symex.Make(Soteria.Bv_values.Bv_solver.Z3_solver).t

val (let+^) : 
  (Cerb_location.t ->
    ('a * Cerb_location.t)
      Soteria__Symex.Make(Soteria.Bv_values.Bv_solver.Z3_solver).t) ->
  ('a -> 'b) ->
  Cerb_location.t ->
  (('b, 'c, 'd) Soteria.Symex.Compo_res.t * Cerb_location.t)
    Soteria__Symex.Make(Soteria.Bv_values.Bv_solver.Z3_solver).t

val frame_range : 
  t ->
  replace_node:
    (t ->
      Cerb_location.t ->
      ((t, 'b, 'c) Soteria.Symex.Compo_res.t * Cerb_location.t)
        Soteria__Symex.Make(Soteria.Bv_values.Bv_solver.Z3_solver).t) ->
  rebuild_parent:
    ((MemVal.t, sint) tree ->
      left:t ->
      right:t ->
      Cerb_location.t ->
      ((MemVal.t, sint) tree * Cerb_location.t)
        Soteria__Symex.Make(Soteria.Bv_values.Bv_solver.Z3_solver).t) ->
  Range.t ->
  Cerb_location.t ->
  ((t * t, 'b, 'c) Soteria.Symex.Compo_res.t * Cerb_location.t)
    Soteria__Symex.Make(Soteria.Bv_values.Bv_solver.Z3_solver).t

val get_raw : 
  MemVal.S_bounded_int.t Soteria.Bv_values.Bv_solver.Z3_solver.Value.t ->
  MemVal.S_bounded_int.t Soteria.Bv_values.Bv_solver.Z3_solver.Value.t ->
  t ->
  Cerb_location.t ->
  ((t * t, 'a, 'b) Soteria.Symex.Compo_res.t * Cerb_location.t)
    Soteria__Symex.Make(Soteria.Bv_values.Bv_solver.Z3_solver).t

val put_raw : 
  t ->
  t ->
  Cerb_location.t ->
  ((unit * t, 'a, 'b) Soteria.Symex.Compo_res.t * Cerb_location.t)
    Soteria__Symex.Make(Soteria.Bv_values.Bv_solver.Z3_solver).t

module Consumer_frame_range : sig ... end

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

module Producer_frame_range : sig ... end

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