List of all items

Structs

• ArbitraryPointer
• PointerGenerator
• futures::JoinHandle
• futures::RoundRobin
• shadow::ShadowMem

Enums

• AllocationStatus
• futures::SchedulingAssumption

Traits

• Arbitrary
• futures::SchedulingStrategy
• invariant::Invariant

Macros

• arbitrary_tuple
• cover
• generate_arbitrary
• generate_float
• generate_models
• implies
• kani_intrinsics
• kani_lib
• kani_mem
• kani_mem_init
• ptr_generator
• ptr_generator_fn
• slice_generator

Attribute Macros

• contracts::ensures
• contracts::modifies
• contracts::proof_for_contract
• contracts::requires
• contracts::stub_verified
• ensures
• loop_invariant
• modifies
• proof
• proof_for_contract
• recursion
• requires
• should_panic
• solver
• stub
• stub_verified
• unwind

Derive Macros

• Arbitrary
• Invariant

Functions

• any
• any_where
• assert
• assume
• concrete_playback_run
• cover
• float::float_to_int_in_range
• futures::block_on
• futures::block_on_with_spawn
• futures::spawn
• futures::yield_now
• mem::can_dereference
• mem::can_read_unaligned
• mem::can_write
• mem::can_write_unaligned
• mem::checked_align_of_raw
• mem::checked_size_of_raw
• mem::same_allocation
• pointer_generator
• slice::any_slice_of_array
• slice::any_slice_of_array_mut
• vec::any_vec
• vec::exact_vec