Spurious dereference failure for ptr::read_volatile on a zero-sized type #5072

ptr::read_volatile on a valid, aligned pointer to a zero-sized type reports four dereference failures, while the same read through ptr::read verifies.

Reproduction (standalone crate, cargo kani)

#[cfg(kani)]
mod proofs {
    #[kani::proof]
    fn read_volatile_zst() {
        let x = ();
        unsafe { core::ptr::read_volatile(&x) };
    }

    #[kani::proof]
    fn read_zst() {
        let x = ();
        unsafe { core::ptr::read(&x) };
    }
}

Output (cargo kani --output-format=terse):

Checking harness proofs::read_zst...
VERIFICATION:- SUCCESSFUL
Checking harness proofs::read_volatile_zst...
Failed Checks: dereference failure: pointer NULL
Failed Checks: dereference failure: pointer invalid
Failed Checks: dereference failure: pointer outside object bounds
Failed Checks: dereference failure: invalid integer address
VERIFICATION:- FAILED
Complete - 1 successfully verified harnesses, 1 failures, 2 total.

The failed checks carry no source location.

Expected

Both harnesses verify. Per the read_volatile documentation, for a zero-sized type the pointer only has to be non-null and properly aligned, which &x is, so the call is defined behavior. It looks like a zero-size volatile_load is modeled as an actual memory access (possibly related to #1163).

Versions where it reproduces

• kani-verifier latest release via cargo install --locked kani-verifier: Kani 0.68.0, CBMC 6.11.0;
• Kani built from commit 9461e07af7ec929f050aa4192f29363c9be07779: Kani 0.68.0, CBMC 6.11.0.

Both on GitHub-hosted ubuntu-latest. We first saw it in kani verify-std mode in model-checking/verify-rust-std, where a comparator that reads its arguments with read_volatile fails for T = () only because of this; the standalone crate above confirms it outside the standard library.

Disclosure: this report was drafted with the help of an AI assistant (Claude). The reproduction above was run on GitHub Actions with both Kani versions listed, and the output shown is from those runs.