Tree_state (soteria-rust.Soteria_rust_lib.State.Tree

module T = Soteria_rust_lib.Typed.T

module DecayMap = Sptr.DecayMap

module DecayMapMonad = Sptr.DecayMapMonad

module Sptr = Sptr.ArithPtr

module Encoder : sig ... end

module StateKey : sig ... end

module Freeable (I : sig ... end) : sig ... end

module Bi (B : Soteria.Sym_states.Base.M(DecayMapMonad).S) : sig ... end

module Tree_block : sig ... end

module Meta : sig ... end

type global =

| String of string
| Global of Charon.Types.global_decl_id

module GlobMap : sig ... end

module FunBiMap : sig ... end

module Block : sig ... end

module Freeable_block : sig ... end

module Freeable_block_with_meta : sig ... end

module Heap : sig ... end

type syn =

| Heap of Heap.syn

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

val show_syn : syn -> Ppx_deriving_runtime.string

type t = {

heap : Heap.t option;
functions : FunBiMap.t;
globals : Sptr.t Rust_val.full_ptr GlobMap.t;
errors : Error.with_trace list;
pointers : DecayMap.t;
thread_destructor : unit -> t option -> ((unit, Error.with_trace, syn list) Soteria.Symex.Compo_res.t * t option) Rustsymex.t;
const_generics : Sptr.t Rust_val.rust_val Charon.Types.ConstGenericVarId.Map.t;

}

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

val show : t -> Ppx_deriving_runtime.string

module SM : sig ... end

val pp_pretty : ignore_freed:bool -> Stdlib.Format.formatter -> t -> unit

val empty_state : t

val empty : t option

val of_opt : t option -> t

val log : string -> Sptr.t -> unit SM.t

val with_loc_err : 
  ?trace:string ->
  unit ->
  (unit -> ('a, Error.t, 'f) SM.Result.t) ->
  ('a, Error.with_trace, 'f) SM.Result.t

val with_heap_symex : 'a Heap.SM.t -> 'a SM.t

val with_heap : 
  ('a, 'b, Heap.syn list) Heap.SM.Result.t ->
  ('a, 'b, syn list) SM.Result.t

val apply_parser : 
  ?ignore_borrow:bool ->
  Sptr.t ->
  (offset:T.sint Typed.t -> 'a Heap.Decoder.ParserMonad.t) ->
  ('a, Error.t, syn list) SM.Result.t

val with_decay_map : 'a DecayMapMonad.t -> 'a SM.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 uninit : 
  (Sptr.t * 'a) ->
  Charon.Types.ty ->
  (unit, Error.with_trace, syn list) SM.Result.t

val tb_load_untyped : 
  Sptr.t ->
  [ `NonZero | `Zero ] Typed.t ->
  (unit,
    [> `AccessedFnPointer
    | `AliasingError
    | `NullDereference
    | `OutOfBounds
    | `UBDanglingPointer
    | `UseAfterFree ],
    syn list)
    SM.Result.t

Performs a load at the tree borrow level, by updating the borrow state, without attempting to validate the values or checking uninitialised memory accesses; all of these are ignored.

val tb_load : 
  (Sptr.t * 'a) ->
  Charon.Types.ty ->
  (unit, Error.with_trace, syn list) SM.Result.t

Performs a load at the tree borrow level, by updating the borrow state, without attempting to validate the values or checking uninitialised memory accesses; all of these are ignored.

val store : 
  (Sptr.t * Sptr.t Rust_val.meta) ->
  Charon.Types.ty ->
  Encoder.rust_val ->
  (unit, Error.with_trace, syn list) SM.Result.t

val size_and_align_of_val : 
  Charon.Types.ty ->
  (Soteria_rust_lib.Typed.T.sint Typed.t, Sptr.t) Rust_val.meta_raw ->
  (Soteria_rust_lib.Typed.T.sint Typed.t
   * Soteria_rust_lib.Typed.T.nonzero Typed.t,
    Error.with_trace,
    syn list)
    SM.Result.t

val check_ptr_align : 
  Sptr.t Rust_val.full_ptr ->
  Charon.Types.ty ->
  (unit, Error.with_trace, syn list) SM.Result.t

val load : 
  ?ignore_borrow:bool ->
  (Sptr.t * (Soteria_rust_lib.Typed.T.sint Typed.t, Sptr.t) Rust_val.meta_raw) ->
  Charon.Types.ty_kind ->
  (Sptr.t Rust_val.rust_val, Error.with_trace, syn list) SM.Result.t

val load_discriminant : 
  (Sptr.t * Sptr.t Rust_val.meta) ->
  Charon.Types.ty ->
  (Charon.Types.variant_id, Error.with_trace, syn list) SM.Result.t

val check_non_dangling : 
  (Sptr.t * (Soteria_rust_lib.Typed.T.sint Typed.t, Sptr.t) Rust_val.meta_raw) ->
  Charon.Types.ty ->
  (unit, Error.with_trace, syn list) SM.Result.t

val fake_read : 
  (Sptr.t * (Soteria_rust_lib.Typed.T.sint Typed.t, Sptr.t) Rust_val.meta_raw) ->
  Charon.Types.ty ->
  (unit, Error.with_trace, syn list) SM.Result.t

val copy_nonoverlapping : 
  src:(Sptr.t * 'a) ->
  dst:(Sptr.t * 'b) ->
  size:Tree_block.MemVal.S_bounded_int.t Sptr.DecayMapMonad.Value.t ->
  (unit, Error.with_trace, syn list) SM.Result.t

val alloc : 
  ?kind:Common.Alloc_kind.t ->
  ?span:Charon.Meta.span_data ->
  ?zeroed:bool ->
  Tree_block.sint ->
  Soteria_rust_lib.Typed.T.nonzero Typed.t ->
  (Sptr.t * ('a, 'b) Rust_val.meta_raw, 'c, syn list) SM.Result.t

val alloc_untyped : 
  ?kind:Common.Alloc_kind.t ->
  ?span:Charon.Meta.span_data ->
  zeroed:bool ->
  size:Tree_block.sint ->
  align:Soteria_rust_lib.Typed.T.nonzero Typed.t ->
  (Sptr.t * ('a, 'b) Rust_val.meta_raw, 'c, syn list) SM.Result.t

val alloc_ty : 
  ?kind:Common.Alloc_kind.t ->
  ?span:Charon.Meta.span_data ->
  Charon.Types.ty ->
  (Sptr.t * ('a, 'b) Rust_val.meta_raw, Error.with_trace, syn list) SM.Result.t

val alloc_tys : 
  ?kind:Common.Alloc_kind.t ->
  ?span:Charon.Meta.span_data ->
  Charon.Types.ty list ->
  ((Sptr.t * ('a, 'b) Rust_val.meta_raw) list, Error.with_trace, syn list)
    SM.Result.t

val free : (Sptr.t * 'a) -> (unit, Error.with_trace, syn list) SM.Result.t

val zeros : 
  (Sptr.t * 'a) ->
  [ `NonZero | `Zero ] Typed.t ->
  (unit, Error.with_trace, syn list) SM.Result.t

val with_globals : 
  unit ->
  (Sptr.t Rust_val.full_ptr GlobMap.t ->
    'a * Sptr.t Rust_val.full_ptr GlobMap.t) ->
  ('a, 'b, 'c) Soteria.Symex.Compo_res.t SM.t

val store_str_global : 
  string ->
  Sptr.t Rust_val.full_ptr ->
  (unit, 'a, 'b) Soteria.Symex.Compo_res.t SM.t

val store_global : 
  Charon.Types.global_decl_id ->
  Sptr.t Rust_val.full_ptr ->
  (unit, 'a, 'b) Soteria.Symex.Compo_res.t SM.t

val load_str_global : 
  string ->
  (Sptr.t Rust_val.full_ptr option, 'a, 'b) Soteria.Symex.Compo_res.t SM.t

val load_global : 
  Charon.Types.global_decl_id ->
  (Sptr.t Rust_val.full_ptr option, 'a, 'b) Soteria.Symex.Compo_res.t SM.t

val borrow : 
  ?protect:bool ->
  (Sptr.t * 'a) ->
  Charon.Types.ty ->
  (Sptr.t * 'a, Error.with_trace, syn list) SM.Result.t

val unprotect : 
  (Sptr.t * 'a) ->
  Charon.Types.ty ->
  (unit, Error.with_trace, syn list) SM.Result.t

val with_exposed : 
  [< Soteria__Bv_values__Typed.T.sint ] Typed.t ->
  (Sptr.t * ('a, 'b) Rust_val.meta_raw, Error.with_trace, syn list) SM.Result.t

val leak_check : unit -> (unit, Error.with_trace, syn list) SM.Result.t

val with_errors : 
  unit ->
  (Error.with_trace list -> 'a * Error.with_trace list) ->
  ('a, Error.with_trace, syn list) SM.Result.t

val add_error : 
  Error.with_trace ->
  (unit, Error.with_trace, syn list) SM.Result.t

val pop_error : 
  unit ->
  ('a, Error.with_trace, syn list) Soteria.Symex.Compo_res.t SM.t

val with_functions : (FunBiMap.t -> 'a * FunBiMap.t) -> 'a SM.t

val declare_fn : 
  FunBiMap.M_rev.key ->
  (Sptr.t * ('a, 'b) Rust_val.meta_raw, 'c, syn list) Soteria.Symex.Compo_res.t
    SM.t

val lookup_fn : 
  (Sptr.t * 'a) ->
  (Common.Fun_kind.t, Error.with_trace, 'b) SM.Result.t

val lookup_const_generic : 
  Charon.Types.ConstGenericVarId.Map.key ->
  Charon.Types.ty ->
  (Sptr.t Rust_val.rust_val, Error.with_trace, 'a) SM.Result.t

val register_thread_exit : 
  (unit -> (unit, Error.with_trace, syn list) Soteria.Symex.Compo_res.t SM.t) ->
  (unit, 'a, 'b) Soteria.Symex.Compo_res.t SM.t

val run_thread_exits : 
  unit ->
  t option ->
  ((unit, Error.with_trace, syn list) Soteria.Symex.Compo_res.t * t option)
    Rustsymex.t

val to_syn : t -> syn list

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

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

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