Module Cgil_lib.SHeapTree

type missingResourceType =
  1. | Unfixable
  2. | Fixable of {
    1. is_store : bool;
    2. low : Gillian.Gil_syntax.Expr.t;
    3. chunk : Chunk.t;
    }
type err =
  1. | UseAfterFree
  2. | BufferOverrun
  3. | InsufficientPermission of {
    1. required : Perm.t;
    2. actual : Perm.t;
    }
  4. | InvalidAlignment of {
    1. alignment : int;
    2. offset : Gillian.Gil_syntax.Expr.t;
    }
  5. | MissingResource of missingResourceType
  6. | Unhandled of string
  7. | RemovingNotOwned
  8. | WrongMemVal
  9. | MemoryNotFreed
val err_to_yojson : err -> Yojson.Safe.t
val err_of_yojson : Yojson.Safe.t -> err Ppx_deriving_yojson_runtime.error_or
val pp_err : err Fmt.t
type 'a or_error = ('a, err) Result.t
type 'a d_or_error = ('a, err) Monadic.Delayed_result.t
module Range : sig ... end
type t
val to_yojson : t -> Yojson.Safe.t
val of_yojson : Yojson.Safe.t -> t Ppx_deriving_yojson_runtime.error_or
val pp : t Fmt.t
val pp_full : t Fmt.t
val empty : t
val freed : t
val is_empty : t -> bool
val is_empty_or_freed : t -> bool
val lvars : t -> Utils.Containers.SS.t
val alocs : t -> Utils.Containers.SS.t
val cons_bounds : t -> (Range.t option * t) or_error
val prod_bounds : t -> Range.t option -> t or_error
val cons_single : t -> Gillian.Gil_syntax.Expr.t -> Chunk.t -> (SVal.t * Perm.t option * t) d_or_error
val prod_single : t -> Gillian.Gil_syntax.Expr.t -> Chunk.t -> SVal.t -> Perm.t -> t d_or_error
val get_perm_at : t -> Gillian.Gil_syntax.Expr.t -> Perm.t option d_or_error
val weak_valid_pointer : t -> Gillian.Gil_syntax.Expr.t -> bool d_or_error
val is_freed : t -> bool
val allocated_function : t

An allocated function always has the exact same tree

move dst_tree dst_ofs src_tree src_ofs size moves size bytes from src_tree at src_ofs into dst_tree at dst_ofs and returns the new dst_tree after modification

val assertions : loc:string -> t -> Gillian.Gil_syntax.Asrt.t
val substitution : le_subst:(Gillian.Gil_syntax.Expr.t -> Gillian.Gil_syntax.Expr.t) -> sval_subst:(SVal.t -> SVal.t) -> svarr_subst:(MonadicSVal.SVArray.t -> MonadicSVal.SVArray.t) -> t -> t
val merge : old_tree:t -> new_tree:t -> t d_or_error
module Lift : sig ... end