Module non_volatile 

SMT lowering for the NonVolatile safety property.

This module handles the NonVolatile property which ensures that memory accessed through a pointer is not volatile (memory-mapped I/O).

NonVolatile is a hardware-level property — SMT cannot model whether memory is volatile. However, inside the standard library:

• references (&T, &mut T) and derived pointers are always non-volatile;
• heap-allocated memory is never volatile;
• volatile access is only performed through the explicit read_volatile / write_volatile family, which carry no NonVolatile contract.

Therefore every pointer flowing into a NonVolatile-guarded callsite inside the standard library is, by construction, non-volatile, and we conservatively prove it here.

Functions

check 🔒