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

vstd_extra/external/
mod.rs
