From 4dde430f4fbb55d1a14b31ace773f401b2bb2314 Mon Sep 17 00:00:00 2001 From: Remy Willems Date: Tue, 22 Oct 2024 16:51:46 +0200 Subject: [PATCH] Ran formatter and update expect files --- .../Statements/BoogieGenerator.TrStatement.cs | 3 +- Source/DafnyDriver/CliCompilation.cs | 3 +- .../LitTest/cli/measure-complexity.dfy | 2 +- .../LitTest/cli/measure-complexity.dfy.expect | 52 +++++++++---------- .../dafny0/CoinductiveProofs.dfy.expect | 4 +- .../LitTest/dafny0/SubsetTypes.dfy.expect | 2 +- .../LitTest/dafny1/ListReverse.dfy.expect | 2 +- .../LitTest/dafny1/SchorrWaite.dfy.expect | 4 +- .../definite-assignment.dfy.expect | 4 +- .../Inputs/progressSecondSequence.check | 14 ++--- .../proofDivision/isolateAllAssertions.dfy | 6 +-- .../proofDivision/isolatePaths.dfy | 4 +- 12 files changed, 49 insertions(+), 51 deletions(-) diff --git a/Source/DafnyCore/Verifier/Statements/BoogieGenerator.TrStatement.cs b/Source/DafnyCore/Verifier/Statements/BoogieGenerator.TrStatement.cs index ff27ec52f7..926e680c90 100644 --- 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 index 98089bb513..ae38fdeb96 100644 --- 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 index 62e786470c..4ba89c4c79 100644 --- 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+#): #g' %t.raw > %t.raw2 +// RUN: %sed 's#\(\d+,\d+\): \d+##g' %t.raw > %t.raw2 // RUN: %sed 's#are \d+#are #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 index 8050a00fdc..427b48d3a5 100644 --- 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 The most demanding 100 verification tasks consumed these resources: -measure-complexity.dfy(9,18): -measure-complexity.dfy(8,18): -measure-complexity.dfy(9,15): -measure-complexity.dfy(7,18): -measure-complexity.dfy(19,4): -measure-complexity.dfy(6,18): -measure-complexity.dfy(7,15): -measure-complexity.dfy(7,13): -measure-complexity.dfy(19,15): -measure-complexity.dfy(17,4): -measure-complexity.dfy(19,24): -measure-complexity.dfy(17,15): -measure-complexity.dfy(17,10): -measure-complexity.dfy(19,10): -measure-complexity.dfy(15,6): -measure-complexity.dfy(19,4): -measure-complexity.dfy(19,4): -measure-complexity.dfy(9,13): -measure-complexity.dfy(17,4): -measure-complexity.dfy(8,15): -measure-complexity.dfy(19,15): -measure-complexity.dfy(6,13): -measure-complexity.dfy(8,13): -measure-complexity.dfy(17,4): -measure-complexity.dfy(6,15): -measure-complexity.dfy(19,15): +measure-complexity.dfy +measure-complexity.dfy +measure-complexity.dfy +measure-complexity.dfy +measure-complexity.dfy +measure-complexity.dfy +measure-complexity.dfy +measure-complexity.dfy +measure-complexity.dfy +measure-complexity.dfy +measure-complexity.dfy +measure-complexity.dfy +measure-complexity.dfy +measure-complexity.dfy +measure-complexity.dfy +measure-complexity.dfy +measure-complexity.dfy +measure-complexity.dfy +measure-complexity.dfy +measure-complexity.dfy +measure-complexity.dfy +measure-complexity.dfy +measure-complexity.dfy +measure-complexity.dfy +measure-complexity.dfy +measure-complexity.dfy diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/CoinductiveProofs.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/CoinductiveProofs.dfy.expect index d56b584921..b944b27405 100644 --- 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 index f1a6f5942d..6bcabe0f59 100644 --- 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 index ebe2328e07..823a60a105 100644 --- 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 index a51243d461..699d7ad4e9 100644 --- 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/Source/IntegrationTests/TestFiles/LitTests/LitTest/proof-obligation-desc/definite-assignment.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/proof-obligation-desc/definite-assignment.dfy.expect index 7654cd2021..ceda23307b 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/proof-obligation-desc/definite-assignment.dfy.expect +++ b/Source/IntegrationTests/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/Source/IntegrationTests/TestFiles/LitTests/LitTest/verification/Inputs/progressSecondSequence.check b/Source/IntegrationTests/TestFiles/LitTests/LitTest/verification/Inputs/progressSecondSequence.check index d0b202595a..81630ec8e6 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/verification/Inputs/progressSecondSequence.check +++ b/Source/IntegrationTests/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/Source/IntegrationTests/TestFiles/LitTests/LitTest/verification/proofDivision/isolateAllAssertions.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/verification/proofDivision/isolateAllAssertions.dfy index 45d489f1cf..e117138815 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/verification/proofDivision/isolateAllAssertions.dfy +++ b/Source/IntegrationTests/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/Source/IntegrationTests/TestFiles/LitTests/LitTest/verification/proofDivision/isolatePaths.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/verification/proofDivision/isolatePaths.dfy index f02ea5653f..541e6ff272 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/verification/proofDivision/isolatePaths.dfy +++ b/Source/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