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 int_specs::*;

pub use nonnull::*;

pub use ptr::*;

pub use range::*;

pub use slice::*;

pub use smart_ptr::*;

Modules

convert

derefDeprecated

ilog2

int_specs

Specs for stdlib methods on integer types that aren’t covered by vstd.

nonnull

nonzero

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

ptr

range

slice

smart_ptr

Functions

_verus_external_fn_specification_27_core_32__58__58__32_hint_32__58__58__32_spin__loop^⚠