Module C_states.BlockTree

module Subst = Gillian.Symbolic.Subst
module CoreP = Constr.Core
module MyAsrt = States.MyAsrt
module CConstants = Cgil_lib.CConstants
module Perm = Cgil_lib.Perm
module ValueTranslation = Cgil_lib.ValueTranslation
module Chunk = Cgil_lib.Chunk
module NSVal = Cgil_lib.SVal
module SVal = Cgil_lib.MonadicSVal
module SVArr = SVal.SVArray
val log_string : string -> unit
type missingResourceType =
  1. | Unfixable
  2. | Fixable of {
    1. is_store : bool;
    2. low : Gillian.Gil_syntax.Expr.t;
    3. chunk : Chunk.t;
    }
val pp_missingResourceType : Ppx_deriving_runtime.Format.formatter -> missingResourceType -> Ppx_deriving_runtime.unit
val show_missingResourceType : missingResourceType -> Ppx_deriving_runtime.string
val missingResourceType_to_yojson : missingResourceType -> Yojson.Safe.t
val missingResourceType_of_yojson : Yojson.Safe.t -> missingResourceType Ppx_deriving_yojson_runtime.error_or
type err =
  1. | BufferOverrun
  2. | InsufficientPermission of {
    1. required : Perm.t;
    2. actual : Perm.t;
    }
  3. | InvalidAlignment of {
    1. alignment : int;
    2. offset : Gillian.Gil_syntax.Expr.t;
    }
  4. | MissingResource of missingResourceType
  5. | Unhandled of string
  6. | WrongMemVal
val pp_err : Ppx_deriving_runtime.Format.formatter -> err -> Ppx_deriving_runtime.unit
val show_err : err -> Ppx_deriving_runtime.string
val err_to_yojson : err -> Yojson.Safe.t
val err_of_yojson : Yojson.Safe.t -> err Ppx_deriving_yojson_runtime.error_or
val _ : Yojson.Safe.t -> err Ppx_deriving_yojson_runtime.error_or
exception FatalErr of err
val sval_is_concrete : SVal.t -> bool
val svarr_is_concrete : SVArr.t -> bool
module Range : sig ... end
module Node : sig ... end
module Tree : sig ... end
module M : sig ... end