Module BlockTree.Node

type qty =
  1. | Totally
  2. | Partially
val qty_to_yojson : qty -> Yojson.Safe.t
val qty_of_yojson : Yojson.Safe.t -> qty Ppx_deriving_yojson_runtime.error_or
val str_qty : qty -> string
type mem_val =
  1. | Zeros
  2. | Undef of qty
  3. | Single of {
    1. chunk : Chunk.t;
    2. value : SVal.t;
    }
  4. | Array of {
    1. chunk : Chunk.t;
    2. values : SVArr.t;
    }
val mem_val_to_yojson : mem_val -> Yojson.Safe.t
val mem_val_of_yojson : Yojson.Safe.t -> mem_val Ppx_deriving_yojson_runtime.error_or
val eq_mem_val : mem_val -> mem_val -> bool
type t =
  1. | NotOwned of qty
  2. | MemVal of {
    1. min_perm : Perm.t;
    2. exact_perm : Perm.t option;
    3. mem_val : mem_val;
    }
val to_yojson : t -> Yojson.Safe.t
val of_yojson : Yojson.Safe.t -> t Ppx_deriving_yojson_runtime.error_or
val _ : Yojson.Safe.t -> t Ppx_deriving_yojson_runtime.error_or
val is_concrete : t -> bool
val make_owned : mem_val:mem_val -> perm:Perm.t -> t
val drop_perm_exn : perm:Perm.t -> t -> t
val update_parent_perm : t -> left:t -> right:t -> t
val undefined : perm:Perm.t -> t
val pp : Stdlib.Format.formatter -> t -> unit
val check_perm : Compcert.Memtype.permission option -> t -> (unit, err) Stdlib.result
val exact_perm : t -> [> `KeepLooking | `StopLooking of (Perm.t, err) Stdlib.result ]
val decode_bytes_to_unsigned_int : chunk:Cgil_lib.Chunk.t -> SVArr.t -> int -> SVal.t Monadic__Delayed.t
val decode : low:Gillian.Gil_syntax.Expr.t -> chunk:Chunk.t -> t -> (SVal.t * Perm.t option, err) Stdlib.result Monadic.Delayed.t
val decode_arr : low:'a -> size:Gillian.Gil_syntax.Expr.t -> chunk:Chunk.t -> t -> (SVArr.t * Perm.t option, err) Stdlib.result Monadic.Delayed.t
val encode : perm:Perm.t -> chunk:Chunk.t -> SVal.t -> t
val encode_arr : perm:Perm.t -> chunk:Chunk.t -> SVArr.t -> t
val lvars : t -> Utils.Containers.SS.t
val alocs : t -> Utils.Containers.SS.t
val substitution : sval_subst:(SVal.t -> SVal.t) -> svarr_subst:(SVArr.t -> SVArr.t) -> t -> t