Block (soteria-rust.Soteria_rust_lib.State.Tree

type t = Tree_block.t option * Tree_borrow.t

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

val show : t -> Ppx_deriving_runtime.string

type syn = Tree_block.syn

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

val show_syn : syn -> Ppx_deriving_runtime.string

val to_syn : (Tree_block.t option * 'a) -> Tree_block.syn list

val ins_outs : 
  Tree_block.syn ->
  Tree_block.Expr.t list * Tree_block.Expr.t list

val of_opt : ('a option * Tree_borrow.t) option -> 'a option * Tree_borrow.t

val to_opt : t -> t option

module SM : sig ... end

val with_tree_block : 
  ('a, 'err, 'fix) Tree_block.SM.Result.t ->
  ('a, 'err, 'fix) SM.Result.t

val with_tree_block_read_tb : 
  (Tree_borrow.t -> ('a, 'err, 'fix) Tree_block.SM.Result.t) ->
  ('a, 'err, 'fix) SM.Result.t

val borrow : 
  ?protect:bool ->
  (Sptr.t * 'a) ->
  Charon.Types.ty ->
  Soteria_rust_lib.Typed.T.sint Typed.t ->
  ((Soteria_rust_lib.Typed.T.sptr Typed.t,
     Soteria_rust_lib.Typed.T.nonzero Typed.t,
     Soteria_rust_lib.Typed.T.sint Typed.t)
     Soteria_rust_lib__Sptr.arithptr
   * 'a,
    [> `AliasingError | `InvalidLayout of Charon.Types.ty | `OutOfBounds ],
    Tree_block.syn list)
    Soteria.Symex.Compo_res.t
    SM.t

Borrows a given pointer. ty is the type of the pointer/reference/box being reborrowed.

val unprotect : 
  Soteria_rust_lib.Typed.T.sint Typed.t ->
  Tree_borrow.tag ->
  Soteria_rust_lib.Typed.T.sint Typed.t ->
  (unit, [> `OutOfBounds ], Tree_block.syn list) Soteria.Symex.Compo_res.t SM.t

val assert_exclusively_owned : 
  (Tree_block.t option * Tree_borrow.t) option ->
  (unit, 'a, Tree_block.syn list) Sptr.DecayMapMonad.Result.t

val produce : 'a -> 'b -> 'c

val consume : 'a -> 'b -> 'c