search

model-checking / kani

Kani Rust Verifier
https://model-checking.github.io/kani
Apache License 2.0
2.03k stars 85 forks source link

Fix contract handling of promoted constants and constant static #3305

Open celinval opened 2 days ago

celinval commented 2 days ago

When verifying contracts, CBMC initializes all static variables to non-deterministic values, except for those with constant types or with types / values annotated with ID_C_no_nondet_initialization.

Kani compiler never set these flags, which caused spurious failures when verification depended on promoted constants or constant static variables. This fix changes that.

First, I did a bit of refactoring since we may need to set this Symbol property at a later time for static variables. I also got rid of the initialization function, since the allocation initialization can be done directly from an expression.

Then, I added the new property to the Symbol type. In CBMC, this is a property of the type or expression. However, I decided to add it to Symbol to avoid having to add this attribute to all variants of Type and Expr.

Resolves #3228

By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses.

celinval commented 2 days ago

@remi-delmas-3000 do you mind taking a look?