fix: Verify that all compilable expressions are compilable #2641
Conversation
| @@ -2,9 +2,9 @@ ArrayElementInitResolution.dfy(16,26): Error: array-allocation initialization ex | |||
| ArrayElementInitResolution.dfy(23,23): Error: array-allocation initialization expression expected to have type 'nat ~> D' (instead got 'D') (perhaps write '_ =>' in front of the expression you gave in order to make it an arrow type) | |||
| ArrayElementInitResolution.dfy(38,33): Error: array-allocation initialization expression expected to have type '(nat, nat, nat) ~> char' (instead got 'int -> char') | |||
| ArrayElementInitResolution.dfy(55,31): Error: array-allocation initialization expression expected to have type '(nat, nat, nat, nat, nat) ~> D' (instead got 'D') (perhaps write '(_, _, _, _, _) =>' in front of the expression you gave in order to make it an arrow type) | |||
| ArrayElementInitResolution.dfy(64,21): Error: ghost fields are allowed only in specification contexts | |||
| ArrayElementInitResolution.dfy(64,21): Error: a ghost function is allowed only in specification contexts | |||
There was a problem hiding this comment.
Nice improvement of error reporting :-)
| /* | ||
| module Types { | ||
| datatype XY = | ||
| | {:hello} D0(x: int) |
There was a problem hiding this comment.
What is the purpose of these annotations?
| module Types { | ||
| datatype XY = | ||
| | {:hello} D0(x: int) | ||
| | ghost {:bye} G0(y: bool) |
There was a problem hiding this comment.
Oh wow I did not know you could have ghost variants.
There was a problem hiding this comment.
We don't. Yet. Sorry, my cherry picking must have included these by accident. I didn't intend to include this file in this PR.
| s := 3; | ||
| } | ||
|
|
||
| if xy1.D1? { // error: xy1 might be of a ghost variant |
| } | ||
|
|
||
| method Bad() returns (r: int) { | ||
| if C? { // error: cannot ask about C? since ghost variant A? is a possibility |
There was a problem hiding this comment.
I'm not sure of this one. How come ghost variant A? is a possibility if we are in compiled code?
| @@ -0,0 +1,252 @@ | |||
| // RUN: %dafny_0 /compile:0 "%s" > "%t" | |||
| // RUN: %diff "%s.expect" "%t" | |||
| /* | |||
There was a problem hiding this comment.
What is the purpose of commenting the entire test? Any plans to remove the comments?
| } | ||
| } | ||
|
|
||
| // TODO: resolve and verify update expressions |
Source/Dafny/Util.cs
Outdated
| return false; | ||
| } | ||
|
|
||
| } else if (expr is MemberSelectExpr selectExpr) { | ||
| if (selectExpr.Member != null && selectExpr.Member.IsGhost) { | ||
| reporter?.Error(MessageSource.Resolver, selectExpr, "ghost fields are allowed only in specification contexts"); | ||
| string what; | ||
| switch (selectExpr.Member) { |
There was a problem hiding this comment.
Could you please create a new field for all members, named like WhatKindWithExplicitGhostness or something similar and preferably shorter, that will return what you compute in the variable "what"?
I bet this will be useful for reporting other errors, so it might be worth it moving it there..
Co-authored-by: Mikaël Mayer <[email protected]>
Co-authored-by: Mikaël Mayer <[email protected]>
# Conflicts: # RELEASE_NOTES.md
This PR updates resolution bookkeeping information that tells the verifier to check certain expressions to be compilable. This information was previously missing, except in the case of assignment statements.
Fixes #2640
By submitting this pull request, I confirm that my contribution is made under the terms of the MIT license.