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

vstd_extra/external/
mod.rs
