Open celinval opened 1 month ago
[modifies(dst)]
Does this mean that 1) the function modifies the contents of the location pointed to by
dst
or 2) the contents ofdst
?
Assuming 1), this should be translated to __CPROVER_assigns(*dst)
and CBMC will check that *dst is a valid location of size 0. Which may not be the case depending on how pointers to ZSTs are initialised in Rust.
In Rust, a 0 sized access is valid for any pointer, and the address of a ZST variable can be anything. https://github.com/model-checking/kani/pull/3134 changed Kani to implement that.
I believe CBMC still expects the pointer to point to a valid allocation, which is likely the reason why this is failing. If that's the case, we need to omit the assigns clause.
I tried this code:
using the following command line invocation:
with Kani version: 0.51.0-dev (https://github.com/model-checking/kani/pull/3107)
I expected to see this happen: verification succeeds
Instead, this happened: Verification failed with the following failure: