fix: Count proof obligations of loop headers (dafny-lang#3244)

This PR changes the verifier to increment the assertion count when it
encounters a loop with non-free invariants. This increment was
previously missing, which caused certain "loop invariant on entry"
checks to be omitted (see dafny-lang#3243).

Fixes dafny-lang#3243


<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>

Source/DafnyCore/Verifier/BoogieStmtListBuilder.cs

@@ -1,3 +1,4 @@
+using System.Linq;
 using Microsoft.Boogie;
 
 namespace Microsoft.Dafny {
@@ -26,7 +27,14 @@ public void Add(Cmd cmd) {
  }
  }
  }
- public void Add(StructuredCmd scmd) { builder.Add(scmd); }
+
+ public void Add(StructuredCmd scmd) {
+ builder.Add(scmd);
+ if (scmd is Boogie.WhileCmd whyle && whyle.Invariants.Any(inv => inv is Boogie.AssertCmd)) {
+ tran.assertionCount++;
+ }
+ }
+
  public void Add(TransferCmd tcmd) { builder.Add(tcmd); }
  public void AddLabelCmd(string label) { builder.AddLabelCmd(label); }
  public void AddLocalVariable(string name) { builder.AddLocalVariable(name); }

Test/git-issues/git-issue-3243.dfy

@@ -0,0 +1,22 @@
+// RUN: %exits-with 4 %dafny /compile:0 "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+
+method LoopWithBody(x: int)
+ decreases *
+{
+ var i := 0;
+ while i < x
+ // The following loop-invariant-on-entry check was once omitted when it was the only proof obligation.
+ invariant i <= x // error: loop invariant does not hold on entry
+ decreases *
+ {
+ }
+}
+
+method BodylessLoop(x: int)
+{
+ var i := 0;
+ while i < x
+ // The following loop-invariant-on-entry check was once omitted when it was the only proof obligation.
+ invariant i <= x // error: loop invariant does not hold on entry
+}

Test/git-issues/git-issue-3243.dfy.expect

@@ -0,0 +1,7 @@
+git-issue-3243.dfy(19,2): Warning: note, this loop has no body (loop frame: i)
+git-issue-3243.dfy(10,16): Error: This loop invariant might not hold on entry.
+git-issue-3243.dfy(10,16): Related message: loop invariant violation
+git-issue-3243.dfy(21,16): Error: This loop invariant might not hold on entry.
+git-issue-3243.dfy(21,16): Related message: loop invariant violation
+
+Dafny program verifier finished with 0 verified, 2 errors

docs/dev/news/3244.fix

@@ -0,0 +1 @@
+Check loop invariants on entry, even when such are the only proof obligations in a method.