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 manually_drop;
8pub mod nonnull;
9pub mod smart_ptr;
10
11pub use deref::*;
12pub use ilog2::*;
13pub use manually_drop::*;
14pub use nonnull::*;
15pub use smart_ptr::*;
16
17use vstd::prelude::*;
18
19verus! {
20
21pub assume_specification[ core::hint::spin_loop ]()
22    opens_invariants none
23    no_unwind
24;
25
26} // verus!

vstd_extra/external/mod.rs

vstd_extra/external/
mod.rs