Fix expect files

dafny-lang · Aug 12, 2024 · 51b4ff0 · 51b4ff0
1 parent bb8e2e3
commit 51b4ff0
Show file tree

Hide file tree

Showing 7 changed files with 11 additions and 11 deletions.
diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/ast/reveal/revealFunctions.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/ast/reveal/revealFunctions.dfy.expect
@@ -2,4 +2,4 @@ revealFunctions.dfy(15,12): Error: assertion might not hold
 revealFunctions.dfy(22,12): Error: assertion might not hold
 revealFunctions.dfy(49,21): Error: assertion might not hold
 
-Dafny program verifier finished with 25 verified, 3 errors
+Dafny program verifier finished with 27 verified, 3 errors
diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/ast/subsetTypes/errorReporting.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/ast/subsetTypes/errorReporting.dfy.expect
@@ -1,3 +1,3 @@
-ensuresReporting.dfy(5,2): Error: the given witness expression might not satisfy constraint
+errorReporting.dfy(5,2): Error: the given witness expression might not satisfy constraint
 
-Dafny program verifier finished with 0 verified, 1 errors
+Dafny program verifier finished with 0 verified, 1 error
diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/comp/rust/bymethod.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/comp/rust/bymethod.dfy.expect
@@ -1,3 +1,3 @@
 
-Dafny program verifier finished with 9 verified, 0 errors
+Dafny program verifier finished with 8 verified, 0 errors
 Everything ok
diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/ByMethod.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/ByMethod.dfy.expect
@@ -2,17 +2,17 @@ ByMethod.dfy(38,18): Error: this invariant could not be proved to be maintained
  Related message: loop invariant violation
 ByMethod.dfy(42,4): Error: a postcondition could not be proved on this return path
 ByMethod.dfy(35,4): Related location: this is the postcondition that could not be proved
-ByMethod.dfy(47,11): Error: a postcondition could not be proved on this return path
+ByMethod.dfy(50,4): Error: a postcondition could not be proved on this return path
 ByMethod.dfy(48,12): Related location: this is the postcondition that could not be proved
-ByMethod.dfy(55,11): Error: a postcondition could not be proved on this return path
+ByMethod.dfy(58,4): Error: a postcondition could not be proved on this return path
 ByMethod.dfy(56,12): Related location: this is the postcondition that could not be proved
 ByMethod.dfy(60,4): Error: a postcondition could not be proved on this return path
 ByMethod.dfy(59,4): Related location: this is the postcondition that could not be proved
-ByMethod.dfy(63,12): Error: a postcondition could not be proved on this return path
+ByMethod.dfy(66,12): Error: a postcondition could not be proved on this return path
 ByMethod.dfy(64,27): Related location: this is the postcondition that could not be proved
 ByMethod.dfy(68,4): Error: a postcondition could not be proved on this return path
 ByMethod.dfy(67,4): Related location: this is the postcondition that could not be proved
-ByMethod.dfy(71,12): Error: a postcondition could not be proved on this return path
+ByMethod.dfy(74,12): Error: a postcondition could not be proved on this return path
 ByMethod.dfy(72,27): Related location: this is the postcondition that could not be proved
 ByMethod.dfy(93,11): Error: decreases clause might not decrease
 ByMethod.dfy(102,11): Error: decreases clause might not decrease

diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/Include.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/Include.dfy.expect
@@ -1,5 +1,5 @@
 Include.dfy(32,7): Warning: the ... refinement feature in statements is deprecated
-Include.dfy(20,11): Error: a postcondition could not be proved on this return path
+Include.dfy(22,6): Error: a postcondition could not be proved on this return path
 Includee.dfy(17,19): Related location: this is the postcondition that could not be proved
 Includee.dfy[Concrete](22,15): Error: assertion might not hold
 Include.dfy(28,6): Error: a postcondition could not be proved on this return path
@@ -13,7 +13,7 @@ Includee.dfy(7,0): Error: out-parameter 'y', which is subject to definite-assign
 Includee.dfy(21,2): Error: a postcondition could not be proved on this return path
 Includee.dfy(20,14): Related location: this is the postcondition that could not be proved
 Includee.dfy(24,17): Error: assertion might not hold
-Include.dfy(20,11): Error: a postcondition could not be proved on this return path
+Include.dfy(22,6): Error: a postcondition could not be proved on this return path
 Includee.dfy(17,19): Related location: this is the postcondition that could not be proved
 Includee.dfy[Concrete](22,15): Error: assertion might not hold
 Include.dfy(28,6): Error: a postcondition could not be proved on this return path

diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/NonZeroInitialization.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/NonZeroInitialization.dfy.expect
@@ -7,7 +7,7 @@ NonZeroInitialization.dfy(17,61): Error: result of operation might violate newty
 NonZeroInitialization.dfy(18,46): Error: result of operation might violate newtype constraint for 'NewSix'
 NonZeroInitialization.dfy(19,8): Error: trying witness 0: result of operation might violate newtype constraint for 'NewSix'
 NonZeroInitialization.dfy(37,5): Error: cannot find witness that shows type is inhabited; try giving a hint through a 'witness' or 'ghost witness' clause, or use 'witness *' to treat as a possibly empty type
-NonZeroInitialization.dfy(38,70): Error: result of operation might violate subset type constraint for 'ListTwo'
+NonZeroInitialization.dfy(38,66): Error: result of operation might violate subset type constraint for 'ListTwo'
 NonZeroInitialization.dfy(39,5): Error: cannot find witness that shows type is inhabited; try giving a hint through a 'witness' or 'ghost witness' clause, or use 'witness *' to treat as a possibly empty type
 NonZeroInitialization.dfy(53,0): Error: out-parameter 'g', which is subject to definite-assignment rules, might be uninitialized at this return point
 NonZeroInitialization.dfy(58,7): Error: unless an initializer is provided for the array elements, a new array of 'Yt<GW>' must have empty size

diff --git a/...ce/IntegrationTests/TestFiles/LitTests/LitTest/traits/NonReferenceTraitsVerify.dfy.expect b/...ce/IntegrationTests/TestFiles/LitTests/LitTest/traits/NonReferenceTraitsVerify.dfy.expect