Module BlockTree.M

type err_t = err
val pp_err_t : Ppx_deriving_runtime.Format.formatter -> err_t -> Ppx_deriving_runtime.unit
val show_err_t : err_t -> Ppx_deriving_runtime.string
val err_t_to_yojson : err_t -> Yojson.Safe.t
val err_t_of_yojson : Yojson.Safe.t -> err_t Ppx_deriving_yojson_runtime.error_or
type t = {
  1. bounds : Range.t option;
  2. root : Tree.t option;
}
val show : t -> Ppx_deriving_runtime.string
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
type action = LActions.ac
type pred = LActions.ga
val action_to_str : LActions.ac -> string
val action_from_str : string -> LActions.ac option
val pred_to_str : LActions.ga -> string
val pred_from_str : string -> LActions.ga option
val list_actions : 'a -> (LActions.ac * string list * string list) list
val list_preds : 'a -> (LActions.ga * string list * string list) list
val pp : Stdlib.Format.formatter -> t -> unit
val empty : unit -> t
val is_empty : t -> bool
val is_concrete : t -> bool
val lvars : t -> SS.t
val alocs : t -> SS.t
val get_perm_at : t -> Gillian.Gil_syntax.Expr.t -> (Perm.t option, err) Result.t Gillian.Monadic.Delayed.t
val weak_valid_pointer : t -> Gillian.Gil_syntax.Expr.t -> (bool, err_t) DR.t
val cons_bounds : t -> (Range.t option * t, 'a) Stdlib.result
val prod_bounds : t -> Range.t option -> (t, 'a) Stdlib.result
val with_root_opt : t -> Tree.t option -> (t, 'a) Stdlib.result
val with_root : t -> Tree.t -> (t, 'a) Stdlib.result
val cons_single : t -> Gillian.Gil_syntax.Expr.t -> Chunk.t -> (SVal.t * Perm.t option * t, err) Result.t Gillian.Monadic.Delayed.t
val prod_single : t -> Gillian.Gil_syntax.Expr.t -> Chunk.t -> SVal.t -> Perm.t -> (t, err) Result.t Monadic.Delayed.t
val cons_simple_mem_val : expected_mem_val:Node.mem_val -> t -> Gillian.Gil_syntax.Expr.t -> Gillian.Gil_syntax.Expr.t -> (t * Perm.t option, err) Result.t Gillian.Monadic.Delayed.t
val prod_simple_mem_val : mem_val:Node.mem_val -> t -> Gillian.Gil_syntax.Expr.t -> Gillian.Gil_syntax.Expr.t -> Perm.t -> (t, err) Result.t Monadic.Delayed.t
val _check_valid_alignment : Chunk.t -> Gillian.Gil_syntax.Expr.t -> (unit, err) Stdlib.result Gillian.Monadic.Delayed.t
val assertions : t -> (LActions.ga * Gillian.Gil_syntax.Expr.t list * Gillian.Gil_syntax.Expr.t list) list
val assertions_others : t -> Gillian.Gil_syntax.Asrt.atom list
val merge : old_tree:t -> new_tree:t -> (t, err) Result.t Monadic.Delayed.t
val substitution : le_subst:(Gillian.Gil_syntax.Expr.t -> Gillian.Gil_syntax.Expr.t) -> sval_subst:(SVal.t -> SVal.t) -> svarr_subst:(SVArr.t -> SVArr.t) -> t -> t
val execute_action : LActions.ac -> t -> Gillian.Gil_syntax.Expr.t list -> (t * Gillian.Gil_syntax.Expr.t list, err_t) Result.t Monadic.Delayed.t
val compose : t -> t -> t Monadic__Delayed.t
val is_exclusively_owned : t -> Gillian.Gil_syntax.Expr.t list -> bool Gillian.Monadic.Delayed.t
val substitution_in_place : Subst.t -> t -> t Monadic.Delayed.t
val get_recovery_tactic : 'a -> 'b Gillian.General.Recovery_tactic.t
val instantiate : Gillian.Gil_syntax.Expr.t list -> t * 'a list
val can_fix : err -> bool
val get_fixes : err -> LActions.ga MyAsrt.t list list
val allocated_function : t