Soteria_lib (soteria-rust.Soteria_rust_lib.Builtins.Eval.M.Soteria

val parse_string : StateM.full_ptr -> (string option, 'a) StateM.t

val assert_ : 
  (Soteria_rust_lib.Typed.T.sint Typed.t, 'a, StateM.Sptr.t) Rust_val.raw list ->
  (('b, 'c, 'd) Rust_val.raw, 'e) StateM.t

val assume : 
  ([< Soteria_rust_lib.Typed.T.any ] Typed.t, 'a, 'b) Rust_val.raw list ->
  (('c, 'd, 'e) Rust_val.raw, 'f) StateM.t

val nondet_bytes : Charon.Types.fun_sig -> 'a -> (StateM.rust_val, 'b) StateM.t

val panic : 
  ?msg:string ->
  (Soteria_rust_lib.Typed.T.sint Typed.t, 'a, StateM.Sptr.t) Rust_val.raw list ->
  ('b, 'c) StateM.t