Adds support for range annotation in assigns clauses #5972
Closed
Conversation
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
We now support ranges on code contracts when specifiying which portions of an array should or should not change. We update the parser and type checking to support this new annotations within assigns clauses. Signed-off-by: Felipe R. Monteiro <[email protected]>
We expand assigns clause's support to also handle array ranges (e.g. `myArr[5 .. lastIdx]`) similarly to ACSL. Signed-off-by: Felipe R. Monteiro <[email protected]>
Code contracts properly supports assigns clause with array ranges. So, we added regression tests to validate this capability. Signed-off-by: Felipe R. Monteiro <[email protected]>
feliperodri
added
do not review
aws
Codecov Report
@@ Coverage Diff @@
## develop #5972 +/- ##
===========================================
+ Coverage 75.01% 75.04% +0.02%
===========================================
Files 1431 1431
Lines 155609 155715 +106
===========================================
+ Hits 116732 116855 +123
+ Misses 38877 38860 -17
Continue to review full report at Codecov.
|
|
We decided to not move forward with this range annotation. |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
We proposed an initial support for array ranges based on the ACSL language at #5538. As discussed at #5966, this might not be the correct approach to handle arrays in assigns clause. I'll keep this PR open until we agree on a proper design for assigns clauses moving forward.