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

vstd_extra/external/
mod.rs
