Skip to content

Commit

Permalink
Fix gutter icons fields (#4549)
Browse files Browse the repository at this point in the history
Fixes #4540

### Changes

Do not create verification trees for non-constant fields that can never
trigger verification

### Testing

Added an XUnit test

<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>
  • Loading branch information
keyboardDrummer committed Sep 26, 2023
1 parent a5ecb15 commit e2213ad
Show file tree
Hide file tree
Showing 2 changed files with 19 additions and 1 deletion.
Original file line number Diff line number Diff line change
Expand Up @@ -14,6 +14,24 @@ public class SimpleLinearVerificationGutterStatusTester : LinearVerificationGutt
// the test will fail and give the correct output that can be use for the test
// Add '//Replace<n>:' to edit a line multiple times

[Fact]
public async Task Fields() {
var markedSource = @"
| :method Test() {
| : assert true;
| :}
| :
| :class A {
| : ghost var B: seq<int>
| : var C: array<int>
| :
| : method Test() {
| : assert true;
| : }
| :}";
await VerifyTrace(markedSource, false, intermediates: false);
}

[Fact]
public async Task GitIssue4287GutterHighlightingBroken() {
await VerifyTrace(@"
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -95,7 +95,7 @@ void AddAndPossiblyMigrateVerificationTree(VerificationTree verificationTree) {
continue;
}

if (member is Field) {
if (member is ConstantField) {
var constantHasNoBody = member.RangeToken.EndToken.line == 0;
if (constantHasNoBody) {
continue; // Nothing to verify
Expand Down

0 comments on commit e2213ad

Please sign in to comment.