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

vstd_extra/external/
mod.rs
