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

vstd_extra/external/
mod.rs
