MemVal (soteria-rust.Soteria_rust_lib.State.Tree_state.Tree

module TB = Soteria.Sym_states.Tree_block

module S_bool = Soteria_rust_lib.Typed.Bool

module S_bounded_int : sig ... end

type qty =

| Totally
| Partially

val pp_qty : 
  Ppx_deriving_runtime.Format.formatter ->
  qty ->
  Ppx_deriving_runtime.unit

val show_qty : qty -> Ppx_deriving_runtime.string

type !'a value_raw =

| Init of 'a
| Zeros
| Uninit of qty
| Any
| Lazy

type value = rust_val value_raw

type value_syn = Sptr.syn Rust_val.syn value_raw

type t = value * Tree_borrow.tb_state

type syn = value_syn

val ins_outs : 
  (Soteria_rust_lib.Typed.Expr.t, Soteria_rust_lib.Typed.Expr.t, Sptr.syn)
    Rust_val.raw
    value_raw ->
  'a list * Soteria_rust_lib.Typed.Expr.t list

val value_to_syn : 
  (Soteria_rust_lib.Typed.T.sint Typed.t,
    'a Soteria__Bv_values__Typed.t,
    Sptr.t)
    Rust_val.raw
    value_raw ->
  (Soteria_rust_lib.Typed.Expr.t, Soteria_rust_lib.Typed.Expr.t, Sptr.syn)
    Rust_val.raw
    value_raw
    Soteria.Soteria_std.Seq.t
    option

val to_syn : t -> syn Soteria.Soteria_std.Seq.t option

val pp_value_raw : 
  (Stdlib.Format.formatter -> 'a -> Ppx_deriving_runtime.unit) ->
  Stdlib.Format.formatter ->
  'a value_raw ->
  Ppx_deriving_runtime.unit

val pp_value : 
  Stdlib.Format.formatter ->
  (Soteria_rust_lib.Typed.T.sint Typed.t,
    Soteria_rust_lib.Typed.T.sfloat Typed.t,
    Sptr.t)
    Rust_val.raw
    value_raw ->
  Ppx_deriving_runtime.unit

val pp : 
  Stdlib.Format.formatter ->
  ((Soteria_rust_lib.Typed.T.sint Typed.t,
     Soteria_rust_lib.Typed.T.sfloat Typed.t,
     Sptr.t)
     Rust_val.raw
     value_raw
   * 'a) ->
  Ppx_deriving_runtime.unit

val pp_value_syn : 
  Stdlib.Format.formatter ->
  (Soteria_rust_lib.Typed.Expr.t, Soteria_rust_lib.Typed.Expr.t, Sptr.syn)
    Rust_val.raw
    value_raw ->
  Ppx_deriving_runtime.unit

val pp_syn : 
  Stdlib.Format.formatter ->
  (Soteria_rust_lib.Typed.Expr.t, Soteria_rust_lib.Typed.Expr.t, Sptr.syn)
    Rust_val.raw
    value_raw ->
  Ppx_deriving_runtime.unit

val merge : 
  left:('a value_raw * Tree_borrow.tb_state) ->
  right:('b value_raw * Tree_borrow.tb_state) ->
  'c value_raw * Tree_borrow.tb_state

val split_rval : 
  rust_val ->
  [< Soteria__Bv_values__Typed.T.any NonZero Zero ] Typed.t ->
  Soteria_rust_lib__Sptr.DecayMap.t ->
  ((([> Soteria__Bv_values__Typed.T.sint ] Soteria__Bv_values__Typed.t, 'a, 'b)
      Rust_val.raw
    * ([> Soteria__Bv_values__Typed.T.sint ] Soteria__Bv_values__Typed.t,
        'c,
        'd)
        Rust_val.raw)
   * Soteria_rust_lib__Sptr.DecayMap.t)
    Rustsymex.t

val split : 
  at:Soteria_rust_lib.Typed.T.sint Typed.t ->
  (rust_val value_raw * 'a) ->
  ((([> Soteria__Bv_values__Typed.T.sint ] Soteria__Bv_values__Typed.t, 'b, 'c)
      Rust_val.raw
      value_raw
    * 'a,
     'd)
     TB.Split_tree.t
   * (([> Soteria__Bv_values__Typed.T.sint ] Soteria__Bv_values__Typed.t,
        'e,
        'f)
        Rust_val.raw
        value_raw
      * 'a,
       'g)
       TB.Split_tree.t)
    Sptr.DecayMapMonad.t

val mk_fix_typed : 
  Charon.Types.ty ->
  unit ->
  Soteria_rust_lib__Sptr.DecayMap.t ->
  ((Soteria_rust_lib.Typed.Expr.t, Soteria_rust_lib.Typed.Expr.t, Sptr.syn)
     Rust_val.raw
     value_raw
     list
   * Soteria_rust_lib__Sptr.DecayMap.t)
    Rustsymex.t

val mk_fix_any : unit -> 'a value_raw list

type tree = (t, Soteria_rust_lib.Typed.T.sint Typed.t) TB.tree

val not_owned : tree -> tree

val owned : tree -> value -> tree

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

val produce : syn -> tree -> tree Sptr.DecayMapMonad.Producer.t

val assert_exclusively_owned : 'a -> (unit, 'b, 'c) Sptr.DecayMapMonad.Result.t