-
Notifications
You must be signed in to change notification settings - Fork 250
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
[CONTRACTS] Allow loop contracts annotated to goto statement #8281
base: develop
Are you sure you want to change the base?
Conversation
8462c9f
to
7de1747
Compare
warning().source_location = code.find_source_location(); | ||
warning() << "Loop invariants is not side-effect-free." << eom; |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Nobody reads warnings. Can you describe the scenario where side effects would be ok?
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
According to the offline discussion. I will move all the checks and throw to contracts component. They should not be in the converter.
Codecov ReportAttention: Patch coverage is
Additional details and impacted files@@ Coverage Diff @@
## develop #8281 +/- ##
===========================================
- Coverage 77.55% 77.49% -0.07%
===========================================
Files 1721 1721
Lines 190128 190281 +153
Branches 18438 18371 -67
===========================================
+ Hits 147448 147450 +2
- Misses 42680 42831 +151 ☔ View full report in Codecov by Sentry. |
This PR enable loop contracts annotated to goto statement, which is we we do in Kani generated GOTO program.