-
Notifications
You must be signed in to change notification settings - Fork 13k
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
typeof() in the type language #3228
Comments
Nominating for backwards compatible milestone. |
reserving the keyword at least is required for this to be backwards-compatible; actual feature is later |
accepted for backwards-compatible milestone |
This would be very nice. |
This is the kind of thing we really need to go through the new formal RFC process. There's never going to be enough discussion here. It's no longer a backwards compatibility issue because |
…-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`. Resolves rust-lang#3228
I'm not sure if this would be useful in every-day code, but I just wrote some code where it would've been nice to say:
instead of
The text was updated successfully, but these errors were encountered: