Fix: Better reporting if 'this' used in a subset type - and no crash #2994
Conversation
| @@ -14875,7 +14874,11 @@ public ResolutionContext(ICodeContext codeContext, bool isTwoState) | |||
| if (currentClass is ClassDecl cd && cd.IsDefaultClass) { | |||
There was a problem hiding this comment.
It looks like this case would also hit a crash, just later on in the pipeline?
There was a problem hiding this comment.
How would you reproduce it?
There was a problem hiding this comment.
I didn't have any luck, and it looks like the error immediately above should always be triggered, which seems to prevent any further problems.
Test/git-issues/git-issue-2068.dfy
Outdated
| // RUN: %dafny_0 /compile:0 "%s" > "%t" | ||
| // RUN: %diff "%s.expect" "%t" | ||
|
|
||
| type St = s:St_ | (forall o | o in s :: o.i(this)) |
There was a problem hiding this comment.
As per my other comment, it would be great to show this fix working correctly in a few other illegal contexts as well, just for deeper testing coverage.
There was a problem hiding this comment.
I added two other illegal context, the witness clause and a static const RHS. The static const RHS was also crashing Boogie. I was able to ensure the fixes use the same convention as for the existing code.
Of the top-level contexts, there is no other case to my knowledge where "this" should be disallowed.
This PR fixes #2068
I added the corresponding test. The case of a "this" inside a subset type is not allowed, but there was no error mechanism to detect it. This PR solves that problem.
By submitting this pull request, I confirm that my contribution is made under the terms of the MIT license.