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

vstd_extra/external/
mod.rs
