Skip to content

Commit

Permalink
Update tests that use --progress, so they are stable (dafny-lang#5300)
Browse files Browse the repository at this point in the history 
### Description
Update tests that use --progress, so they no longer depend on an
unstable order

### How has this been tested?
Tests were changed

<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
keyboardDrummer authored Apr 5, 2024
1 parent 56a1652 commit beab582
Show file tree
Hide file tree
Showing 6 changed files with 30 additions and 22 deletions.
3 changes: 1 addition & 2 deletions Source/IntegrationTests/TestFiles/LitTests/LitTest/hofs/ArrowTypeOptimizations.dfy
View file
Original file line number Diff line number Diff line change
@@ -1,5 1,4 @@
// RUN: %exits-with 4 %verify --cores 1 --progress "%s" > "%t".raw
// RUN: %sed 's/taking \d*ms/redacted/g' %t.raw > %t
// RUN: %exits-with 4 %verify --isolate-assertions --cores 1 "%s" > "%t"
// RUN: %diff "%s.expect" "%t"

// These tests make sure that the built-in arrow types are taken into account when
Expand Down
22 changes: 4 additions & 18 deletions Source/IntegrationTests/TestFiles/LitTests/LitTest/hofs/ArrowTypeOptimizations.dfy.expect
View file
Original file line number Diff line number Diff line change
@@ -1,19 1,5 @@
Verified 0/7 symbols. Waiting for CheckReads to verify.
Verification part 1/1 of CheckReads, on line 8, could not prove all assertions, redacted and consuming 1.1E 004 resources
ArrowTypeOptimizations.dfy(11,2): Error: function precondition could not be proved
ArrowTypeOptimizations.dfy(11,2): Error: insufficient reads clause to invoke function
Verified 1/7 symbols. Waiting for CheckPre to verify.
Verification part 1/1 of CheckPre, on line 14, could not prove all assertions, redacted and consuming 1.0E 004 resources
ArrowTypeOptimizations.dfy(17,2): Error: function precondition could not be proved
Verified 2/7 symbols. Waiting for CheckReadsTot to verify.
Verification part 1/1 of CheckReadsTot, on line 20, verified successfully, redacted and consuming 1.0E 004 resources
Verified 3/7 symbols. Waiting for CheckReadsParens to verify.
Verification part 1/1 of CheckReadsParens, on line 26, verified successfully, redacted and consuming 1.0E 004 resources
Verified 4/7 symbols. Waiting for CheckReadsLambdaGeneral to verify.
Verification part 1/1 of CheckReadsLambdaGeneral, on line 32, verified successfully, redacted and consuming 1.9E 004 resources
Verified 5/7 symbols. Waiting for CheckReadsLambdaPartial to verify.
Verification part 1/1 of CheckReadsLambdaPartial, on line 38, verified successfully, redacted and consuming 1.7E 004 resources
Verified 6/7 symbols. Waiting for CheckReadsLambdaTotal to verify.
Verification part 1/1 of CheckReadsLambdaTotal, on line 44, verified successfully, redacted and consuming 1.5E 004 resources
ArrowTypeOptimizations.dfy(10,2): Error: function precondition could not be proved
ArrowTypeOptimizations.dfy(10,2): Error: insufficient reads clause to invoke function
ArrowTypeOptimizations.dfy(16,2): Error: function precondition could not be proved

Dafny program verifier finished with 5 verified, 3 errors
Dafny program verifier finished with 17 verified, 3 errors
5 changes: 5 additions & 0 deletions ...tegrationTests/TestFiles/LitTests/LitTest/verification/Inputs/progressFirstSequence.check
View file
Original file line number Diff line number Diff line change
@@ -0,0 1,5 @@
// CHECK-L:Verified 0/5 symbols. Waiting for Foo to verify.
// CHECK-L:Verified 1/5 symbols. Waiting for Faz to verify.
// CHECK-L:Verified 2/5 symbols. Waiting for Fopple to verify.
// CHECK-L:Verified 3/5 symbols. Waiting for Burp to verify.
// CHECK-L:Verified 4/5 symbols. Waiting for Blanc to verify.
12 changes: 12 additions & 0 deletions ...egrationTests/TestFiles/LitTests/LitTest/verification/Inputs/progressSecondSequence.check
View file
Original file line number Diff line number Diff line change
@@ -0,0 1,12 @@
// CHECK-L:Verification part 1/3 of Foo, on line 6, verified successfully, redacted and consuming 8.7E 002 resources
// CHECK-L:Verification part 2/3 of Foo, on line 8, verified successfully, redacted and consuming 3.1E 003 resources
// CHECK-L:Verification part 3/3 of Foo, on line 9, verified successfully, redacted and consuming 2.8E 003 resources
// CHECK-L:Verification part 1/2 of Faz, on line 12, verified successfully, redacted and consuming 8.7E 002 resources
// CHECK-L:Verification part 2/2 of Faz, on line 12, verified successfully, redacted and consuming 3.1E 003 resources
// CHECK-L:Verification part 1/2 of Fopple, on line 14, verified successfully, redacted and consuming 8.7E 002 resources
// CHECK-L:Verification part 2/2 of Fopple, on line 14, verified successfully, redacted and consuming 3.1E 003 resources
// CHECK-L:Verification part 1/3 of Burp, on line 16, verified successfully, redacted and consuming 8.7E 002 resources
// CHECK-L:Verification part 2/3 of Burp, on line 18, verified successfully, redacted and consuming 3.1E 003 resources
// CHECK-L:Verification part 3/3 of Burp, on line 19, verified successfully, redacted and consuming 2.8E 003 resources
// CHECK-L:Verification part 1/2 of Blanc, on line 22, verified successfully, redacted and consuming 8.7E 002 resources
// CHECK-L:Verification part 2/2 of Blanc, on line 22, verified successfully, redacted and consuming 3.1E 003 resources
7 changes: 6 additions & 1 deletion Source/IntegrationTests/TestFiles/LitTests/LitTest/verification/isolate-assertions.dfy
View file
Original file line number Diff line number Diff line change
@@ -1,6 1,11 @@
// RUN: %verify --progress --cores=1 %s &> %t.raw
// RUN: %sed 's/taking \d*ms/redacted/g' %t.raw > %t
// RUN: %diff "%s.expect" "%t"
// RUN: %OutputCheck --file-to-check "%t" "%s"
// CHECK-L:Verification part 1/3 of Foo, on line 10, verified successfully, redacted and consuming 8.7E 002 resources
// CHECK-L:Verification part 2/3 of Foo, on line 11, verified successfully, redacted and consuming 3.1E 003 resources
// CHECK-L:Verification part 3/3 of Foo, on line 12, verified successfully, redacted and consuming 2.8E 003 resources
// CHECK-L:Verified 1/2 symbols. Waiting for Bar to verify.
// CHECK-L:Verification part 1/1 of Bar, on line 15, verified successfully, redacted and consuming 3.1E 003 resources

method {:isolate_assertions} Foo() {
assert true;
Expand Down
3 changes: 2 additions & 1 deletion Source/IntegrationTests/TestFiles/LitTests/LitTest/verification/progress.dfy
View file
Original file line number Diff line number Diff line change
@@ -1,6 1,7 @@
// RUN: %verify --progress --isolate-assertions --cores=1 %s > %t.raw
// RUN: %sed 's/taking \d*ms/redacted/g' %t.raw > %t
// RUN: %diff "%s.expect" "%t"
// RUN: %OutputCheck --file-to-check %t "%S/Inputs/progressFirstSequence.check"
// RUN: %OutputCheck --file-to-check %t "%S/Inputs/progressSecondSequence.check"

method Foo()
{
Expand Down

0 comments on commit beab582

Please sign in to comment.