You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
…-lang#3305)
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`.
Resolvesrust-lang#3228
The following crashes:
This is because the autoderef code is not being used if the call occurs in a monomorphized context. My trans refactoring should fix this.
The text was updated successfully, but these errors were encountered: