Use Module Name in identifying a let-such-that expression #4718
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
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.
WIP Fixes #4717
Description
Let-such-that expressions are currently assigned an id during translation to Boogie which is unique within the Dafny module being translated. However, this id is not unique in the entire translated Dafny program, since a Dafny program with multiple modules is translated to multiple Boogie files. This means that several Boogie files might contain
#canCallfunctions that are identically named but express different functionality. This PR proposes to extend the unique id with the module name to make disambiguating between such functions easier.To be clear, the existing implementation does not lead to any issues during verification. However, it makes it much more difficult to manipulate Boogie code produced from Dafny and, in particular, leads to a bug in test generation when several Boogie files are merged together into one. The proposed change maintains the properties that ids have right now (unique per module and consistent when translating the same file multiple times) while also making it easier to interpret and modify the resulting Boogie code.
How has this been tested?
By submitting this pull request, I confirm that my contribution is made under the terms of the MIT license.