Add :reproducible_resource_limit attribute
#796
Merged
Conversation
This file contains 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
This doesn't multiply by 1000. The corresponding CLI flag is /reproducibleResourceLimit.
| ps.GetUnsignedNumericArgument(x => ResourceLimit = Util.BoundedMultiply(x, 1000), null); | ||
| return true; | ||
|
|
||
| case "reproducibleResourceLimit": |
There was a problem hiding this comment.
Can we use a word that captures "reproducible resource that correlates with time", like tick or cycle ?
| @@ -1978,7 +1982,10 @@ similar effects. | |||
| Limit the number of seconds spent trying to verify | |||
| each procedure | |||
| /rlimit:<num> | |||
There was a problem hiding this comment.
Please update the documentation to say that this option is deprecated and will be removed. I would even prefer already removing it by returning an error when it is used.
|
I simplified things by removing the backward-compatibility layer. We'll want one in Dafny, but it's not necessarily needed in Boogie, given the very few users of the feature. |
keyboardDrummer
previously approved these changes
Oct 17, 2023
keyboardDrummer
approved these changes
Oct 18, 2023
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.
This doesn't multiply by 1000, unlike
:rlimit. The corresponding CLI flag is/reproducibleResourceLimit.I'm a little unsure about the name. It's a bit of a mouthful. Maybe leaving out "reproducible" would be better.
Fixes #795.