Allow outer function outputs in outline preconditions (Fix issue #1029)#1031
Draft
jcp19 wants to merge 3 commits into
Draft
Allow outer function outputs in outline preconditions (Fix issue #1029)#1031jcp19 wants to merge 3 commits into
jcp19 wants to merge 3 commits into
Conversation
When checking preconditions, we used to reject every reference to an output parameter, regardless of which function-like construct introduced it. This was too strict: output parameters of the surrounding function already have a meaningful value by the time an outline statement or a nested closure literal is entered, so referencing them in the precondition of those constructs is legitimate. The check now only rejects references to output parameters declared by the spec's own owner (function, method, closure literal, interface method, or method implementation proof). For outline statements - which do not declare their own outputs - no output parameter reference is rejected. Fixes #1029.
jcp19
commented
May 13, 2026
Comment on lines
+6
to
+8
| // Output parameters of the surrounding function may be referenced in the | ||
| // precondition of an outline statement, because they have a meaningful value | ||
| // at the entry of the outline block. (Issue #1029) |
Contributor
Author
There was a problem hiding this comment.
Suggested change
| // Output parameters of the surrounding function may be referenced in the | |
| // precondition of an outline statement, because they have a meaningful value | |
| // at the entry of the outline block. (Issue #1029) | |
| // Output parameters of the surrounding function may be referenced in the | |
| // precondition of an outline statement and closres. |
| // precondition of an outline statement, because they have a meaningful value | ||
| // at the entry of the outline block. (Issue #1029) | ||
|
|
||
| ensures acc(r) && *r == 42 |
Contributor
Author
There was a problem hiding this comment.
add explicit return statements in all examples
Comment on lines
+37
to
+45
| func bad() { | ||
| //:: ExpectedOutput(type_error) | ||
| c := requires s == 0 | ||
| ensures s == 1 | ||
| func nested() (s int) { | ||
| return 1 | ||
| } | ||
| _ = c | ||
| } |
Contributor
Author
There was a problem hiding this comment.
introduce another example where a closure's precondition mentions the return parameter of the outer scope. that should be accepted by the type checker as well.
Comment on lines
+47
to
+60
| // An outline block in a function without named output parameters keeps | ||
| // type-checking. | ||
| func unnamedOut() *int { | ||
| i@ := 0 | ||
| p := &i | ||
|
|
||
| requires acc(p) | ||
| ensures acc(p) && *p == 42 | ||
| outline ( | ||
| *p = 42 | ||
| ) | ||
|
|
||
| return p | ||
| } |
Contributor
Author
There was a problem hiding this comment.
Suggested change
| // An outline block in a function without named output parameters keeps | |
| // type-checking. | |
| func unnamedOut() *int { | |
| i@ := 0 | |
| p := &i | |
| requires acc(p) | |
| ensures acc(p) && *p == 42 | |
| outline ( | |
| *p = 42 | |
| ) | |
| return p | |
| } |
jcp19
changed the title
- Reword the header comment to refer to outlines and closures. - Add explicit return statements in the positive examples. - Add a positive test case where a nested closure literal's precondition references the outer function's named output parameter. - Drop the redundant outline-with-unnamed-output example.
jcp19
commented
May 13, 2026
Co-authored-by: João Pereira <joaopereira.19@gmail.com>
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
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
2 participants
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.
PR #1018 introduced a regression where occurrences of a return parameter are no longer allowed in pres of outline blocks and closures declared inside the body. This fixes that and introduces new tests