Heap (soteria-rust.Soteria_rust_lib.State.Tree

include sig ... end

type t

module SM : sig ... end

type syn = StateKey.syn * Freeable_block_with_meta.syn

val consume : syn -> t option -> (t option, syn list) DecayMapMonad.Consumer.t

val empty : t

val syntactic_bindings : 
  t ->
  (StateKey.t * Freeable_block_with_meta.t) Stdlib.Seq.t

val syntactic_mem : StateKey.t -> t -> bool

val pp' : 
  ?codom:(Stdlib.Format.formatter -> Freeable_block_with_meta.t -> unit) ->
  ?key:(Stdlib.Format.formatter -> StateKey.t -> unit) ->
  ?ignore:((StateKey.t * Freeable_block_with_meta.t) -> bool) ->
  Stdlib.Format.formatter ->
  t ->
  unit

val pp : Stdlib.Format.formatter -> t -> unit

val show : t -> string

val pp_syn : Stdlib.Format.formatter -> syn -> unit

val show_syn : syn -> string

val to_syn : t -> syn list

val of_opt : t option -> t

val to_opt : t -> t option

val ins_outs : 
  syn ->
  DecayMapMonad.Value.Expr.t list * DecayMapMonad.Value.Expr.t list

val alloc : 
  new_codom:Freeable_block_with_meta.t ->
  (StateKey.t, 'err, syn list) SM.Result.t

val allocs : 
  fn:('a -> StateKey.t -> ('k * Freeable_block_with_meta.t) DecayMapMonad.t) ->
  els:'a list ->
  ('k list, 'err, syn list) SM.Result.t

val wrap : 
  StateKey.t ->
  (Freeable_block_with_meta.t option ->
    (('a, 'err, Freeable_block_with_meta.syn list) Soteria.Symex.Compo_res.t
     * Freeable_block_with_meta.t option)
      DecayMapMonad.t) ->
  ('a, 'err, syn list) SM.Result.t

val fold : 
  ('acc -> (StateKey.t * Freeable_block_with_meta.t) -> 'acc DecayMapMonad.t) ->
  'acc ->
  t option ->
  'acc DecayMapMonad.t

val produce : syn -> t option -> t option DecayMapMonad.Producer.t

val with_ptr : 
  Sptr.t ->
  ([ `NonZero | `Zero ] Typed.t ->
    ('a,
      [> `AccessedFnPointer
      | `NullDereference
      | `UBDanglingPointer
      | `UseAfterFree ] as 'b,
      Block.syn list)
      Block.SM.Result.t) ->
  ('a, 'b, syn list) SM.Result.t

val is_freed : StateKey.t -> (bool, 'a, syn list) SM.Result.t

module Decoder : sig ... end