model-checking
Fix contract handling of promoted constants and constant static
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.
seems like filling up undefined bytes with
falsein Allocation initialisers may be underapproximating.
Reading undefined bytes is UB. Any analysis that read uninitialized bytes is unsound, hence the value doesn't matter.