Skip to content

Commit

Permalink
Fix: Green gutter icons over constants without RHS (#5842)
Browse files Browse the repository at this point in the history
Fixes #5841
Tests have been added

<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
MikaelMayer authored Oct 18, 2024
1 parent 64f5715 commit 2db26d2
Show file tree
Hide file tree
Showing 3 changed files with 17 additions and 3 deletions.
Original file line number Diff line number Diff line change
Expand Up @@ -37,6 +37,20 @@ await VerifyTrace(@"
? :}", false, intermediates: false);
}

[Fact]
public async Task ConstantWithoutRhsMarkedAsVerified() {
await VerifyTrace(@"
| :class Test {
| : const x: int
| :
| : method Testing()
| : requires x > 0
| : ensures x != 0
| : {
| : }
| :}", false, intermediates: false);
}

[Fact]
public async Task Fields() {
var markedSource = @"
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -80,9 +80,8 @@ void AddAndPossiblyMigrateVerificationTree(VerificationTree verificationTree) {
continue;
}

if (member is ConstantField) {
var constantHasNoBody = member.RangeToken.EndToken.line == 0;
if (constantHasNoBody) {
if (member is ConstantField constantField) {
if (constantField.Rhs == null) {
continue; // Nothing to verify
}

Expand Down
1 change: 1 addition & 0 deletions docs/dev/news/5841.fix
Original file line number Diff line number Diff line change
@@ -0,0 +1 @@
Green gutter icons cover constants without RHS

0 comments on commit 2db26d2

Please sign in to comment.