Module external 

Specifications for functions from Rust standard library but not specified in vstd.

These specifications are determined with careful inspection of the std library source code and documentation, and trusted as TCB. They are subject to change if vstd covers more cases in the future.

Re-exports

pub use ilog2::*;

pub use nonnull::*;

pub use ptr::*;

pub use range::*;

pub use slice::*;

pub use smart_ptr::*;

Modules

derefDeprecated

ilog2

nonnull

nonzero

Specifications for core::num::NonZero<usize> using a wrapper type NonZeroUsize.

ptr

range

slice

smart_ptr

Functions

_verus_external_fn_specification_17_core_32__58__58__32_hint_32__58__58__32_spin__loop^⚠