Ran formatter and update expect files

dafny-lang · Oct 22, 2024 · 4dde430 · 4dde430
1 parent 30f91b2
commit 4dde430
Show file tree

Hide file tree

Showing 12 changed files with 49 additions and 51 deletions.
diff --git a/Source/DafnyCore/Verifier/Statements/BoogieGenerator.TrStatement.cs b/Source/DafnyCore/Verifier/Statements/BoogieGenerator.TrStatement.cs
@@ -404,8 +404,7 @@ void AddResultCommands(BoogieStmtListBuilder returnBuilder, Expression result) {
     }
   }
 
-  private void TrBreakStmt(BoogieStmtListBuilder builder, ExpressionTranslator etran, BreakStmt breakStmt)
-  {
+  private void TrBreakStmt(BoogieStmtListBuilder builder, ExpressionTranslator etran, BreakStmt breakStmt) {
     AddComment(builder, breakStmt, $"{breakStmt.Kind} statement");
     foreach (var _ in Enumerable.Range(0, builder.Context.ScopeDepth - breakStmt.TargetStmt.ScopeDepth)) {
       builder.Add(new ChangeScope(breakStmt.Tok, ChangeScope.Modes.Pop));

diff --git a/Source/DafnyDriver/CliCompilation.cs b/Source/DafnyDriver/CliCompilation.cs
@@ -279,8 +279,7 @@ await Options.OutputWriter.WriteLineAsync(
     }
   }
 
-  private static string JumpOriginKind(JumpOrigin returnOrigin)
-  {
+  private static string JumpOriginKind(JumpOrigin returnOrigin) {
     return returnOrigin.IsolatedReturn is GotoCmd ? "continue" : "return";
   }
 

diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/cli/measure-complexity.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/cli/measure-complexity.dfy
@@ -1,5 +1,5 @@
 // RUN: %exits-with 4 %baredafny measure-complexity --show-snippets false --use-basename-for-filename --isolate-assertions --worst-amount 100 "%s" > %t.raw
-// RUN: %sed 's#\): \d+#): <redacted>#g' %t.raw > %t.raw2
+// RUN: %sed 's#\(\d+,\d+\): \d+#<redacted>#g' %t.raw > %t.raw2
 // RUN: %sed 's#are \d+#are <redacted>#g' %t.raw2 > %t
 // RUN: %diff "%s.expect" "%t"
 method Foo() {

diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/cli/measure-complexity.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/cli/measure-complexity.dfy.expect
@@ -2,29 +2,29 @@ Starting verification of iteration 1/1 with seed 0
 measure-complexity.dfy(6,18): Error: assertion might not hold
 The total consumed resources are <redacted>
 The most demanding 100 verification tasks consumed these resources:
-measure-complexity.dfy(9,18): <redacted>
-measure-complexity.dfy(8,18): <redacted>
-measure-complexity.dfy(9,15): <redacted>
-measure-complexity.dfy(7,18): <redacted>
-measure-complexity.dfy(19,4): <redacted>
-measure-complexity.dfy(6,18): <redacted>
-measure-complexity.dfy(7,15): <redacted>
-measure-complexity.dfy(7,13): <redacted>
-measure-complexity.dfy(19,15): <redacted>
-measure-complexity.dfy(17,4): <redacted>
-measure-complexity.dfy(19,24): <redacted>
-measure-complexity.dfy(17,15): <redacted>
-measure-complexity.dfy(17,10): <redacted>
-measure-complexity.dfy(19,10): <redacted>
-measure-complexity.dfy(15,6): <redacted>
-measure-complexity.dfy(19,4): <redacted>
-measure-complexity.dfy(19,4): <redacted>
-measure-complexity.dfy(9,13): <redacted>
-measure-complexity.dfy(17,4): <redacted>
-measure-complexity.dfy(8,15): <redacted>
-measure-complexity.dfy(19,15): <redacted>
-measure-complexity.dfy(6,13): <redacted>
-measure-complexity.dfy(8,13): <redacted>
-measure-complexity.dfy(17,4): <redacted>
-measure-complexity.dfy(6,15): <redacted>
-measure-complexity.dfy(19,15): <redacted>
+measure-complexity.dfy<redacted>
+measure-complexity.dfy<redacted>
+measure-complexity.dfy<redacted>
+measure-complexity.dfy<redacted>
+measure-complexity.dfy<redacted>
+measure-complexity.dfy<redacted>
+measure-complexity.dfy<redacted>
+measure-complexity.dfy<redacted>
+measure-complexity.dfy<redacted>
+measure-complexity.dfy<redacted>
+measure-complexity.dfy<redacted>
+measure-complexity.dfy<redacted>
+measure-complexity.dfy<redacted>
+measure-complexity.dfy<redacted>
+measure-complexity.dfy<redacted>
+measure-complexity.dfy<redacted>
+measure-complexity.dfy<redacted>
+measure-complexity.dfy<redacted>
+measure-complexity.dfy<redacted>
+measure-complexity.dfy<redacted>
+measure-complexity.dfy<redacted>
+measure-complexity.dfy<redacted>
+measure-complexity.dfy<redacted>
+measure-complexity.dfy<redacted>
+measure-complexity.dfy<redacted>
+measure-complexity.dfy<redacted>
diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/CoinductiveProofs.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/CoinductiveProofs.dfy.expect
@@ -31,5 +31,5 @@ CoinductiveProofs.dfy(208,21): Related location: this is the postcondition that
 CoinductiveProofs.dfy(4,23): Related location: this proposition could not be proved
 
 Dafny program verifier finished with 23 verified, 12 errors
-Total resources used is 770796
-Max resources used by VC is 60436
+Total resources used is 779029
+Max resources used by VC is 66829
diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/SubsetTypes.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/SubsetTypes.dfy.expect
@@ -91,5 +91,5 @@ SubsetTypes.dfy(459,15): Error: assertion might not hold
 SubsetTypes.dfy(464,13): Error: assertion might not hold
 
 Dafny program verifier finished with 13 verified, 91 errors
-Total resources used is 775000
+Total resources used is 775600
 Max resources used by VC is 101900
diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny1/ListReverse.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny1/ListReverse.dfy.expect
@@ -1,2 +1,2 @@
 
-Dafny program verifier finished with 2 verified, 0 errors
+Dafny program verifier finished with 1 verified, 0 errors
diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny1/SchorrWaite.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny1/SchorrWaite.dfy.expect
@@ -1,4 +1,4 @@
 
 Dafny program verifier finished with 272 verified, 0 errors
-Total resources used is 30906777
-Max resources used by VC is 2048364
+Total resources used is 22649507
+Max resources used by VC is 2020501
diff --git a/...tionTests/TestFiles/LitTests/LitTest/proof-obligation-desc/definite-assignment.dfy.expect b/...tionTests/TestFiles/LitTests/LitTest/proof-obligation-desc/definite-assignment.dfy.expect
@@ -1,7 +1,7 @@
-definite-assignment.dfy(16,4): Error: field 'x', which is subject to definite-assignment rules, might be uninitialized at this point in the constructor body
- Asserted expression: assigned(x)
 definite-assignment.dfy(16,4): Error: field 'y', which is subject to definite-assignment rules, might be uninitialized at this point in the constructor body
  Asserted expression: assigned(y)
+definite-assignment.dfy(16,4): Error: field 'x', which is subject to definite-assignment rules, might be uninitialized at this point in the constructor body
+ Asserted expression: assigned(x)
 definite-assignment.dfy(33,9): Error: variable 'y', which is subject to definite-assignment rules, might be uninitialized here
  Asserted expression: assigned(y)
 definite-assignment.dfy(36,0): Error: out-parameter 'x', which is subject to definite-assignment rules, might be uninitialized at this return point

diff --git a/...egrationTests/TestFiles/LitTests/LitTest/verification/Inputs/progressSecondSequence.check b/...egrationTests/TestFiles/LitTests/LitTest/verification/Inputs/progressSecondSequence.check
@@ -1,7 +1,7 @@
-// CHECK:Verified part #0, 1/2 of Foo, on line 8, verified successfully \(time: .*, resource count: .*\)
-// CHECK:Verified part #1, 2/2 of Foo, on line 9, verified successfully \(time: .*, resource count: .*\)
-// CHECK:Verified part #0, 1/1 of Faz, on line 12, verified successfully \(time: .*, resource count: .*\)
-// CHECK:Verified part #0, 1/1 of Fopple, on line 14, verified successfully \(time: .*, resource count: .*\)
-// CHECK:Verified part #0, 1/2 of Burp, on line 18, verified successfully \(time: .*, resource count: .*\)
-// CHECK:Verified part #1, 2/2 of Burp, on line 19, verified successfully \(time: .*, resource count: .*\)
-// CHECK:Verified part #0, 1/1 of Blanc, on line 22, verified successfully \(time: .*, resource count: .*\)
+// CHECK:Verified 1/2 of Foo: assertion at line 8, verified successfully \(time: .*, resource count: .*\)
+// CHECK:Verified 2/2 of Foo: assertion at line 9, verified successfully \(time: .*, resource count: .*\)
+// CHECK:Verified 1/1 of Faz: assertion at line 12, verified successfully \(time: .*, resource count: .*\)
+// CHECK:Verified 1/1 of Fopple: assertion at line 14, verified successfully \(time: .*, resource count: .*\)
+// CHECK:Verified 1/2 of Burp: assertion at line 18, verified successfully \(time: .*, resource count: .*\)
+// CHECK:Verified 2/2 of Burp: assertion at line 19, verified successfully \(time: .*, resource count: .*\)
+// CHECK:Verified 1/1 of Blanc: assertion at line 22, verified successfully \(time: .*, resource count: .*\)
diff --git a/...ationTests/TestFiles/LitTests/LitTest/verification/proofDivision/isolateAllAssertions.dfy b/...ationTests/TestFiles/LitTests/LitTest/verification/proofDivision/isolateAllAssertions.dfy
@@ -1,9 +1,9 @@
 // RUN: %verify --progress VerificationJobs --cores=1 %s &> %t
 // RUN: %OutputCheck --file-to-check "%t" "%s"
-// CHECK:Verified part #0, 1/2 of Foo, on line 9, verified successfully \(time: .*, resource count: .*\)
-// CHECK:Verified part #1, 2/2 of Foo, on line 10, verified successfully \(time: .*, resource count: .*\)
+// CHECK:Verified 1/2 of Foo: assertion at line 9, verified successfully \(time: .*, resource count: .*\)
+// CHECK:Verified 2/2 of Foo: assertion at line 10, verified successfully \(time: .*, resource count: .*\)
 // CHECK:Verified 1/2 symbols. Waiting for Bar to verify.
-// CHECK:Verified part #0, 1/1 of Bar, on line 13, verified successfully \(time: .*, resource count: .*\)
+// CHECK:Verified 1/1 of Bar: body, verified successfully \(time: .*, resource count: .*\)
 
 method {:isolate_assertions} Foo() {
   assert true;

diff --git a/...e/IntegrationTests/TestFiles/LitTests/LitTest/verification/proofDivision/isolatePaths.dfy b/...e/IntegrationTests/TestFiles/LitTests/LitTest/verification/proofDivision/isolatePaths.dfy
@@ -1,10 +1,10 @@
-// RUN: ! %verify --progress --cores=1 %s &> %t
+// RUN: ! %verify --progress VerificationJobs --cores=1 %s &> %t
 // RUN: %OutputCheck --file-to-check "%t" "%s"
 // CHECK:Verified 1/4 of Assertion: assertion at line 28, through \[15,23\], could not prove all assertions
 // CHECK:Verified 2/4 of Assertion: assertion at line 28, through \[15,25\], verified successfully
 // CHECK:Verified 3/4 of Assertion: assertion at line 28, through \[18,23\], verified successfully
 // CHECK:Verified 4/4 of Assertion: assertion at line 28, through \[18,25\], verified successfully
-// CHECK:Verified 1/3 of Return: remaining body, could not prove all assertions
+// CHECK:Verified 1/3 of Return: body, could not prove all assertions
 // CHECK:Verified 2/3 of Return: return at line 45, through \[37\], could not prove all assertions
 // CHECK:Verified 3/3 of Return: return at line 45, through \[40\], verified successfully