Def assignment update #3311
Merged
Def assignment update #3311
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
…ess --enforce-determinism is used.
davidcok
requested changes
Jan 3, 2023
| var x:G, y:G, z:G := a, *, a; | ||
| if h < 10 { | ||
| k := x; // fine | ||
| } else if h < 20 { | ||
| k := y; // error: y has not yet been assigned | ||
| k := y; | ||
| } else { | ||
| z := *; | ||
| return z; // this is fine, since z was assigned before the havoc |
There was a problem hiding this comment.
Why does 'z was assigned before the havoc' matter? It doesn't for 'y', right?
There was a problem hiding this comment.
I think this comment can go
davidcok
approved these changes
Jan 3, 2023
(I'm assuming you meant "possibly empty", not "non-empty".) Since we allow |
I see :-) |
|
Don't you effectively define In fact: given you have |
This was referenced Feb 27, 2023
keyboardDrummer
added a commit
that referenced
this pull request
Feb 27, 2023
Fixes #3640 This PR fixes some issues with definite assignment and determinacy. Recently, we changed the default rules for definite assignment in Dafny (PR #3052). The main change was to insist that all local variables and out-parameters be definitely assigned before they are used. This was followed up by PR #3311, which started considering `:= *` assignments as fulfilling definite-assignment requirements. PR #3311 also fixed a point where #3052 had gone too far; with PR #3311, it is now again possible to allocate an array of an auto-init type without having to explicitly assign the array elements. There was one more point where PR #3052 had gone too far (reported in #3640), and the present PR fixes that point. The issue regards fields of a class. The present PR once again allows fields to be auto-initialized (provided their types allow that). This PR also makes `/definiteAssignment:4` available in the legacy CLI. (Previously, it had been added internally, but not exposed in the legacy CLI.) Finally, this PR reports an error in the `--enforce-determinism` mode for any class without a `constructor`. This was a latent omission in the previous checking. Together with once again allowing auto-initialization of fields, this change puts ``` dafny class Cell { // constructor-less class not allowed with --enforce-determinism var data: int } method NondeterministicReturn() returns (r: int) { var c := new Cell; return c.data; } ``` on the same footing as ``` dafny class Cell { var data: int constructor () { // with --enforce-determinism, this constructor must initialize .data } } method NondeterministicReturn() returns (r: int) { var c := new Cell(); return c.data; } ``` I argue this PR fixes the new definite-assignment mode in an important way and therefore should be included in Dafny 4.0. The documentation (see, e.g., #3584) may need to be updated. <small>By submitting this pull request, I confirm that my contribution is made under the terms of the [MIT license](https://github.com/dafny-lang/dafny/blob/master/LICENSE.txt).</small> --------- Co-authored-by: Remy Willems <rwillems@amazon.com>
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.
Changes
@RustanLeino should havocing a variable of a non-empty type even be allowed?
Testing
--enforce-determinism, don't need to initialise their values or be empty.By submitting this pull request, I confirm that my contribution is made under the terms of the MIT license.