vstd_extra/external/
mod.rs

1//! Specifications for functions from Rust standard library but not specified in `vstd`.
2//!
3//! These specifications are determined with careful inspection of the std library source code and documentation, and trusted as TCB.
4//! They are subject to change if `vstd` covers more cases in the future.
5pub mod deref;
6pub mod ilog2;
7pub mod nonnull;
8pub mod smart_ptr;
9
10#[deprecated(
11    note = "If you can, do not use this module as it adds assumptions about the core of Rust's deref semantics."
12)]
13pub use deref::*;
14pub use ilog2::*;
15pub use nonnull::*;
16pub use smart_ptr::*;
17
18use vstd::prelude::*;
19
20verus! {
21
22pub assume_specification[ core::hint::spin_loop ]()
23    opens_invariants none
24    no_unwind
25;
26
27} // verus!
vstd_extra/external/mod.rs

vstd_extra/external/
mod.rs
