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 nonzero;
9pub mod ptr;
10pub mod range;
11pub mod slice;
12pub mod smart_ptr;
13
14pub use ilog2::*;
15pub use nonnull::*;
16pub use ptr::*;
17pub use range::*;
18pub use slice::*;
19pub use smart_ptr::*;
20
21use vstd::prelude::*;
22
23verus! {
24
25pub assume_specification[ core::hint::spin_loop ]()
26    opens_invariants none
27    no_unwind
28;
29
30} // verus!
vstd_extra/external/mod.rs

vstd_extra/external/
mod.rs
