From 5348cc8f2f959585344c516d50b744f9cbca6d8f Mon Sep 17 00:00:00 2001 From: Remy Willems Date: Wed, 8 Jan 2025 10:27:55 +0100 Subject: [PATCH] Update expect files and run formatter --- .../LitTest/dafny0/Definedness.dfy.expect | 14 +++++----- .../LitTest/dafny0/Fuel.legacy.dfy.expect | Bin 3885 -> 3733 bytes .../dafny0/IteratorResolution.dfy.expect | 6 ++--- .../LitTest/dafny0/OpaqueFunctions.dfy.expect | 10 ++++---- .../dafny0/ResolutionErrors1.dfy.expect | 2 +- .../dafny0/ResolutionErrors6.dfy.expect | 18 ++++++------- .../ResolutionErrors6.dfy.refresh.expect | 18 ++++++------- .../LitTest/dafny0/SmallTests.dfy.expect | 4 +-- .../LitTest/dafny0/SubsetTypes.dfy.expect | 8 +++--- .../LitTest/dafny0/TypeTests.dfy.expect | 16 ++++++------ .../LitTests/LitTest/dafny4/Bug170.dfy.expect | 24 +++++++++--------- .../exceptions/TypecheckErrors.dfy.expect | 6 ++--- .../exports/OpaqueFunctions.dfy.expect | 2 +- .../git-issues/git-issue-1958.dfy.expect | 10 ++++---- .../git-issues/git-issue-3719.dfy.expect | 2 +- .../git-issues/git-issue-551.dfy.expect | 2 +- .../LitTest/hofs/ReadsReads.dfy.expect | 10 ++++---- .../shift-lower-bound.dfy.expect | 2 +- ...ter-precondition-related-errors.dfy.expect | 2 +- Source/Scripts/UpdateTests.cs | 8 +++--- docs/DafnyRef/Statements.8b.expect | 2 +- docs/DafnyRef/Topics.3.expect | 2 +- docs/DafnyRef/Types.20.expect | 2 +- 23 files changed, 85 insertions(+), 85 deletions(-) diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/Definedness.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/Definedness.dfy.expect index 9a6e1e5b3d8..bd28e97ab5e 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/Definedness.dfy.expect +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/Definedness.dfy.expect @@ -14,32 +14,32 @@ Definedness.dfy(60,21): Related location: this is the postcondition that could n Definedness.dfy(68,2): Error: a postcondition could not be proved on this return path Definedness.dfy(67,21): Related location: this is the postcondition that could not be proved Definedness.dfy(88,6): Error: target object might be null -Definedness.dfy(89,4): Error: function precondition could not be proved +Definedness.dfy(89,5): Error: function precondition could not be proved Definedness.dfy(79,15): Related location: this proposition could not be proved Definedness.dfy(89,9): Error: assignment might update an object not in the enclosing context's modifies clause Definedness.dfy(89,9): Error: target object might be null -Definedness.dfy(90,9): Error: function precondition could not be proved +Definedness.dfy(90,10): Error: function precondition could not be proved Definedness.dfy(79,15): Related location: this proposition could not be proved Definedness.dfy(95,13): Error: possible division by zero Definedness.dfy(95,22): Error: possible division by zero Definedness.dfy(96,14): Error: possible division by zero Definedness.dfy(101,11): Error: possible division by zero Definedness.dfy(108,14): Error: possible division by zero -Definedness.dfy(117,22): Error: function precondition could not be proved +Definedness.dfy(117,23): Error: function precondition could not be proved Definedness.dfy(79,15): Related location: this proposition could not be proved -Definedness.dfy(123,16): Error: function precondition could not be proved +Definedness.dfy(123,17): Error: function precondition could not be proved Definedness.dfy(79,15): Related location: this proposition could not be proved -Definedness.dfy(133,16): Error: function precondition could not be proved +Definedness.dfy(133,17): Error: function precondition could not be proved Definedness.dfy(79,15): Related location: this proposition could not be proved Definedness.dfy(133,21): Error: this loop invariant could not be proved on entry Related message: loop invariant violation -Definedness.dfy(134,16): Error: function precondition could not be proved +Definedness.dfy(134,17): Error: function precondition could not be proved Definedness.dfy(79,15): Related location: this proposition could not be proved Definedness.dfy(143,14): Error: possible division by zero Definedness.dfy(162,14): Error: possible division by zero Definedness.dfy(175,27): Error: this loop invariant could not be proved on entry Related message: loop invariant violation -Definedness.dfy(181,16): Error: function precondition could not be proved +Definedness.dfy(181,17): Error: function precondition could not be proved Definedness.dfy(79,15): Related location: this proposition could not be proved Definedness.dfy(196,18): Error: possible division by zero Definedness.dfy(196,22): Error: this loop invariant could not be proved on entry diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/Fuel.legacy.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/Fuel.legacy.dfy.expect index 7f154f3c152845c7348fa001be68fa5146ec7130..b8806cb18c3300849f15de85fd59e1e642ecb6a5 100755 GIT binary patch delta 14 WcmZ20H&u4RjEO!1n;jV6@&W)Wq6L8f delta 164 ZcmbO#yH;+(jCzKF1(G B', which most often is a typo for 'exists x :: A && B'; if you think otherwise, rewrite as 'exists x :: (A ==> B)' or 'exists x :: !A || B' to suppress this warning ResolutionErrors6.dfy(89,13): Warning: the quantifier has the form 'exists x :: A ==> B', which most often is a typo for 'exists x :: A && B'; if you think otherwise, rewrite as 'exists x :: (A ==> B)' or 'exists x :: !A || B' to suppress this warning -ResolutionErrors6.dfy(123,13): Error: a call to a ghost function is allowed only in specification contexts (consider declaring the function without the 'ghost' keyword) -ResolutionErrors6.dfy(124,13): Error: a call to a ghost function is allowed only in specification contexts (consider declaring the function without the 'ghost' keyword) +ResolutionErrors6.dfy(123,14): Error: a call to a ghost function is allowed only in specification contexts (consider declaring the function without the 'ghost' keyword) +ResolutionErrors6.dfy(124,14): Error: a call to a ghost function is allowed only in specification contexts (consider declaring the function without the 'ghost' keyword) ResolutionErrors6.dfy(126,11): Error: ghost variables such as g are allowed only in specification contexts. g was inferred to be ghost based on its declaration or initialization. ResolutionErrors6.dfy(147,4): Error: ghost variables such as g are allowed only in specification contexts. g was inferred to be ghost based on its declaration or initialization. -ResolutionErrors6.dfy(157,15): Error: a call to a ghost function is allowed only in specification contexts (consider declaring the function without the 'ghost' keyword) -ResolutionErrors6.dfy(158,22): Error: a call to a ghost function is allowed only in specification contexts (consider declaring the function without the 'ghost' keyword) -ResolutionErrors6.dfy(164,15): Error: a call to a ghost function is allowed only in specification contexts (consider declaring the function without the 'ghost' keyword) -ResolutionErrors6.dfy(165,22): Error: a call to a ghost function is allowed only in specification contexts (consider declaring the function without the 'ghost' keyword) +ResolutionErrors6.dfy(157,16): Error: a call to a ghost function is allowed only in specification contexts (consider declaring the function without the 'ghost' keyword) +ResolutionErrors6.dfy(158,23): Error: a call to a ghost function is allowed only in specification contexts (consider declaring the function without the 'ghost' keyword) +ResolutionErrors6.dfy(164,16): Error: a call to a ghost function is allowed only in specification contexts (consider declaring the function without the 'ghost' keyword) +ResolutionErrors6.dfy(165,23): Error: a call to a ghost function is allowed only in specification contexts (consider declaring the function without the 'ghost' keyword) ResolutionErrors6.dfy(182,23): Error: type of left argument to * (int) must agree with the result type (bool) ResolutionErrors6.dfy(182,23): Error: type of * must be of a numeric type, bitvector type, or a set-like type (instead got bool) ResolutionErrors6.dfy(181,13): Error: not resolving module 'V' because there were errors in resolving its nested module 'W' @@ -45,7 +45,7 @@ ResolutionErrors6.dfy(343,18): Error: map update requires the value to have the ResolutionErrors6.dfy(368,5): Error: type parameter (F) passed to method Q must support auto-initialization (got Y) (perhaps try declaring type parameter 'Y' on line 363 as 'Y(0)', which says it can only be instantiated with a type that supports auto-initialization) ResolutionErrors6.dfy(371,5): Error: type parameter (F) passed to method Q must support auto-initialization (got Z) (perhaps try declaring type parameter 'Z' on line 363 as 'Z(0)', which says it can only be instantiated with a type that supports auto-initialization) ResolutionErrors6.dfy(372,5): Error: type parameter (G) passed to method P must be nonempty (got Z) (perhaps try declaring type parameter 'Z' on line 363 as 'Z(00)', which says it can only be instantiated with a nonempty type) -ResolutionErrors6.dfy(381,9): Error: type parameter (F) passed to function FQ must support auto-initialization (got Y) (perhaps try declaring type parameter 'Y' on line 376 as 'Y(0)', which says it can only be instantiated with a type that supports auto-initialization) -ResolutionErrors6.dfy(384,9): Error: type parameter (F) passed to function FQ must support auto-initialization (got Z) (perhaps try declaring type parameter 'Z' on line 376 as 'Z(0)', which says it can only be instantiated with a type that supports auto-initialization) -ResolutionErrors6.dfy(385,9): Error: type parameter (G) passed to function FP must be nonempty (got Z) (perhaps try declaring type parameter 'Z' on line 376 as 'Z(00)', which says it can only be instantiated with a nonempty type) +ResolutionErrors6.dfy(381,11): Error: type parameter (F) passed to function FQ must support auto-initialization (got Y) (perhaps try declaring type parameter 'Y' on line 376 as 'Y(0)', which says it can only be instantiated with a type that supports auto-initialization) +ResolutionErrors6.dfy(384,11): Error: type parameter (F) passed to function FQ must support auto-initialization (got Z) (perhaps try declaring type parameter 'Z' on line 376 as 'Z(0)', which says it can only be instantiated with a type that supports auto-initialization) +ResolutionErrors6.dfy(385,11): Error: type parameter (G) passed to function FP must be nonempty (got Z) (perhaps try declaring type parameter 'Z' on line 376 as 'Z(00)', which says it can only be instantiated with a nonempty type) 46 resolution/type errors detected in ResolutionErrors6.dfy diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/ResolutionErrors6.dfy.refresh.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/ResolutionErrors6.dfy.refresh.expect index 09a91ef2e9a..6d46a15c7e2 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/ResolutionErrors6.dfy.refresh.expect +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/ResolutionErrors6.dfy.refresh.expect @@ -4,14 +4,14 @@ ResolutionErrors6.dfy(44,50): Error: the argument of a fresh expression must den ResolutionErrors6.dfy(71,11): Error: name of type (Cache) is used as a variable ResolutionErrors6.dfy(79,13): Warning: the quantifier has the form 'exists x :: A ==> B', which most often is a typo for 'exists x :: A && B'; if you think otherwise, rewrite as 'exists x :: (A ==> B)' or 'exists x :: !A || B' to suppress this warning ResolutionErrors6.dfy(89,13): Warning: the quantifier has the form 'exists x :: A ==> B', which most often is a typo for 'exists x :: A && B'; if you think otherwise, rewrite as 'exists x :: (A ==> B)' or 'exists x :: !A || B' to suppress this warning -ResolutionErrors6.dfy(123,13): Error: a call to a ghost function is allowed only in specification contexts (consider declaring the function without the 'ghost' keyword) -ResolutionErrors6.dfy(124,13): Error: a call to a ghost function is allowed only in specification contexts (consider declaring the function without the 'ghost' keyword) +ResolutionErrors6.dfy(123,14): Error: a call to a ghost function is allowed only in specification contexts (consider declaring the function without the 'ghost' keyword) +ResolutionErrors6.dfy(124,14): Error: a call to a ghost function is allowed only in specification contexts (consider declaring the function without the 'ghost' keyword) ResolutionErrors6.dfy(126,11): Error: ghost variables such as g are allowed only in specification contexts. g was inferred to be ghost based on its declaration or initialization. ResolutionErrors6.dfy(147,4): Error: ghost variables such as g are allowed only in specification contexts. g was inferred to be ghost based on its declaration or initialization. -ResolutionErrors6.dfy(157,15): Error: a call to a ghost function is allowed only in specification contexts (consider declaring the function without the 'ghost' keyword) -ResolutionErrors6.dfy(158,22): Error: a call to a ghost function is allowed only in specification contexts (consider declaring the function without the 'ghost' keyword) -ResolutionErrors6.dfy(164,15): Error: a call to a ghost function is allowed only in specification contexts (consider declaring the function without the 'ghost' keyword) -ResolutionErrors6.dfy(165,22): Error: a call to a ghost function is allowed only in specification contexts (consider declaring the function without the 'ghost' keyword) +ResolutionErrors6.dfy(157,16): Error: a call to a ghost function is allowed only in specification contexts (consider declaring the function without the 'ghost' keyword) +ResolutionErrors6.dfy(158,23): Error: a call to a ghost function is allowed only in specification contexts (consider declaring the function without the 'ghost' keyword) +ResolutionErrors6.dfy(164,16): Error: a call to a ghost function is allowed only in specification contexts (consider declaring the function without the 'ghost' keyword) +ResolutionErrors6.dfy(165,23): Error: a call to a ghost function is allowed only in specification contexts (consider declaring the function without the 'ghost' keyword) ResolutionErrors6.dfy(182,23): Error: type of right argument to * (bool) must agree with the result type (int) ResolutionErrors6.dfy(181,13): Error: not resolving module 'V' because there were errors in resolving its nested module 'W' ResolutionErrors6.dfy(191,21): Error: type of right argument to * (bool) must agree with the result type (int) @@ -43,7 +43,7 @@ ResolutionErrors6.dfy(343,18): Error: map update requires the value to have the ResolutionErrors6.dfy(368,5): Error: type parameter (F) passed to method Q must support auto-initialization (got Y) (perhaps try declaring type parameter 'Y' on line 363 as 'Y(0)', which says it can only be instantiated with a type that supports auto-initialization) ResolutionErrors6.dfy(371,5): Error: type parameter (F) passed to method Q must support auto-initialization (got Z) (perhaps try declaring type parameter 'Z' on line 363 as 'Z(0)', which says it can only be instantiated with a type that supports auto-initialization) ResolutionErrors6.dfy(372,5): Error: type parameter (G) passed to method P must be nonempty (got Z) (perhaps try declaring type parameter 'Z' on line 363 as 'Z(00)', which says it can only be instantiated with a nonempty type) -ResolutionErrors6.dfy(381,9): Error: type parameter (F) passed to function FQ must support auto-initialization (got Y) (perhaps try declaring type parameter 'Y' on line 376 as 'Y(0)', which says it can only be instantiated with a type that supports auto-initialization) -ResolutionErrors6.dfy(384,9): Error: type parameter (F) passed to function FQ must support auto-initialization (got Z) (perhaps try declaring type parameter 'Z' on line 376 as 'Z(0)', which says it can only be instantiated with a type that supports auto-initialization) -ResolutionErrors6.dfy(385,9): Error: type parameter (G) passed to function FP must be nonempty (got Z) (perhaps try declaring type parameter 'Z' on line 376 as 'Z(00)', which says it can only be instantiated with a nonempty type) +ResolutionErrors6.dfy(381,11): Error: type parameter (F) passed to function FQ must support auto-initialization (got Y) (perhaps try declaring type parameter 'Y' on line 376 as 'Y(0)', which says it can only be instantiated with a type that supports auto-initialization) +ResolutionErrors6.dfy(384,11): Error: type parameter (F) passed to function FQ must support auto-initialization (got Z) (perhaps try declaring type parameter 'Z' on line 376 as 'Z(0)', which says it can only be instantiated with a type that supports auto-initialization) +ResolutionErrors6.dfy(385,11): Error: type parameter (G) passed to function FP must be nonempty (got Z) (perhaps try declaring type parameter 'Z' on line 376 as 'Z(00)', which says it can only be instantiated with a nonempty type) 44 resolution/type errors detected in ResolutionErrors6.dfy diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/SmallTests.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/SmallTests.dfy.expect index c48ba2ad2be..352e0f7ec43 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/SmallTests.dfy.expect +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/SmallTests.dfy.expect @@ -37,10 +37,10 @@ SmallTests.dfy(338,2): Error: a postcondition could not be proved on this return SmallTests.dfy(332,10): Related location: this is the postcondition that could not be proved SmallTests.dfy(379,2): Error: assertion might not hold SmallTests.dfy(386,2): Error: assertion might not hold -SmallTests.dfy(396,3): Error: cannot prove termination; try supplying a decreases clause +SmallTests.dfy(396,8): Error: cannot prove termination; try supplying a decreases clause SmallTests.dfy(408,4): Error: assertion might not hold SmallTests.dfy(418,4): Error: assertion might not hold -SmallTests.dfy(428,5): Error: cannot prove termination; try supplying a decreases clause +SmallTests.dfy(428,10): Error: cannot prove termination; try supplying a decreases clause SmallTests.dfy(445,2): Error: a postcondition could not be proved on this return path SmallTests.dfy(443,40): Related location: this is the postcondition that could not be proved SmallTests.dfy(604,2): Error: assertion might not hold diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/SubsetTypes.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/SubsetTypes.dfy.expect index fa895e61eab..d2033aa26ee 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/SubsetTypes.dfy.expect +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/SubsetTypes.dfy.expect @@ -7,7 +7,7 @@ SubsetTypes.dfy(16,6): Error: cannot establish the existence of LHS values that SubsetTypes.dfy(19,11): Error: value does not satisfy the subset constraints of 'nat' SubsetTypes.dfy(21,15): Error: value does not satisfy the subset constraints of 'nat' SubsetTypes.dfy(23,8): Error: value does not satisfy the subset constraints of 'nat' -SubsetTypes.dfy(30,4): Error: value does not satisfy the subset constraints of 'nat' +SubsetTypes.dfy(31,6): Error: value does not satisfy the subset constraints of 'nat' SubsetTypes.dfy(31,7): Error: value does not satisfy the subset constraints of 'nat' SubsetTypes.dfy(42,24): Error: value does not satisfy the subset constraints of 'nat' SubsetTypes.dfy(44,15): Error: value does not satisfy the subset constraints of 'nat' @@ -23,7 +23,7 @@ SubsetTypes.dfy(72,6): Error: cannot establish the existence of LHS values that SubsetTypes.dfy(75,11): Error: value of expression (of type 'set') is not known to be an instance of type 'set' SubsetTypes.dfy(77,15): Error: value of expression (of type 'set') is not known to be an instance of type 'set' SubsetTypes.dfy(79,8): Error: value of expression (of type 'set') is not known to be an instance of type 'set' -SubsetTypes.dfy(86,4): Error: value of expression (of type 'set') is not known to be an instance of type 'set' +SubsetTypes.dfy(87,6): Error: value of expression (of type 'set') is not known to be an instance of type 'set' SubsetTypes.dfy(87,7): Error: value of expression (of type 'set') is not known to be an instance of type 'set' SubsetTypes.dfy(98,24): Error: value of expression (of type 'set') is not known to be an instance of type 'set' SubsetTypes.dfy(100,15): Error: value of expression (of type 'set') is not known to be an instance of type 'set' @@ -91,5 +91,5 @@ SubsetTypes.dfy(459,6): Error: assertion might not hold SubsetTypes.dfy(464,4): Error: assertion might not hold Dafny program verifier finished with 13 verified, 91 errors -Total resources used is 739000 -Max resources used by VC is 75000 +Total resources used is 738500 +Max resources used by VC is 78400 diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/TypeTests.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/TypeTests.dfy.expect index ecc486403b5..169f5d7882f 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/TypeTests.dfy.expect +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/TypeTests.dfy.expect @@ -15,19 +15,19 @@ TypeTests.dfy(92,3): Error: cannot assign to a range of array elements (try the TypeTests.dfy(94,3): Error: cannot assign to a range of array elements (try the 'forall' statement) TypeTests.dfy(95,3): Error: cannot assign to a range of array elements (try the 'forall' statement) TypeTests.dfy(96,3): Error: cannot assign to a range of array elements (try the 'forall' statement) -TypeTests.dfy(9,14): Error: incorrect argument type at index 0 for function parameter 'c' (expected C, found D) -TypeTests.dfy(9,14): Error: incorrect argument type at index 1 for function parameter 'd' (expected D, found C) -TypeTests.dfy(10,14): Error: incorrect argument type at index 0 for function parameter 'c' (expected C, found int) -TypeTests.dfy(10,14): Error: incorrect argument type at index 1 for function parameter 'd' (expected D, found int) -TypeTests.dfy(16,16): Error: incorrect argument type for method in-parameter 'x' (expected int, found bool) +TypeTests.dfy(9,17): Error: incorrect argument type at index 0 for function parameter 'c' (expected C, found D) +TypeTests.dfy(9,20): Error: incorrect argument type at index 1 for function parameter 'd' (expected D, found C) +TypeTests.dfy(10,15): Error: incorrect argument type at index 0 for function parameter 'c' (expected C, found int) +TypeTests.dfy(10,18): Error: incorrect argument type at index 1 for function parameter 'd' (expected D, found int) +TypeTests.dfy(16,17): Error: incorrect argument type for method in-parameter 'x' (expected int, found bool) TypeTests.dfy(16,16): Error: incorrect return type at index 1 for method out-parameter 'c' (expected C, got int) TypeTests.dfy(17,12): Error: incorrect return type at index 1 for method out-parameter 'c' (expected C, got int) TypeTests.dfy(169,7): Error: non-ghost variable cannot be assigned a value that depends on a ghost TypeTests.dfy(179,6): Error: cannot assign to non-ghost variable in a ghost context TypeTests.dfy(180,9): Error: cannot assign to non-ghost variable in a ghost context -TypeTests.dfy(198,10): Error: incorrect argument type for datatype constructor parameter (expected int -> Dt, found int -> int) (covariant type parameter 1 would require int <: Dt) -TypeTests.dfy(204,10): Error: incorrect argument type for datatype constructor parameter (expected ? -> Dt, found Dt -> Dt) (contravariance for type parameter at index 0 expects ? <: Dt) -TypeTests.dfy(211,10): Error: incorrect argument type for function parameter 'x' (expected ?, found set) +TypeTests.dfy(198,15): Error: incorrect argument type for datatype constructor parameter (expected int -> Dt, found int -> int) (covariant type parameter 1 would require int <: Dt) +TypeTests.dfy(204,15): Error: incorrect argument type for datatype constructor parameter (expected ? -> Dt, found Dt -> Dt) (contravariance for type parameter at index 0 expects ? <: Dt) +TypeTests.dfy(211,11): Error: incorrect argument type for function parameter 'x' (expected ?, found set) TypeTests.dfy(222,9): Error: assignment to array element is not allowed in this context, because this is a ghost method TypeTests.dfy(229,20): Error: using the type being defined ('A') here would cause a logical inconsistency by defining a type whose cardinality exceeds itself (like the Continuum Transfunctioner, you might say its power would then be exceeded only by its mystery) TypeTests.dfy(233,7): Error: recursive constraint dependency involving a subset type: Cyc -> Cycle -> Cyc diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny4/Bug170.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny4/Bug170.dfy.expect index 668f5801e02..9fc780dadfb 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny4/Bug170.dfy.expect +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny4/Bug170.dfy.expect @@ -4,14 +4,14 @@ Bug170.dfy(18,14): Info: _k: ORDINAL Bug170.dfy(26,14): Info: _k: ORDINAL Bug170.dfy(19,14): Info: A#[_k] Bug170.dfy(18,14): Info: AA# with focal predicates A, B -Bug170.dfy(21,7): Info: B#[_k - 1] +Bug170.dfy(21,8): Info: B#[_k - 1] Bug170.dfy(22,6): Info: BB#[_k - 1] Bug170.dfy(27,14): Info: B#[_k] Bug170.dfy(26,14): Info: BB# with focal predicates B, A -Bug170.dfy(29,7): Info: A#[_k - 1] +Bug170.dfy(29,8): Info: A#[_k - 1] Bug170.dfy(30,6): Info: AA#[_k - 1] -Bug170.dfy(10,12): Info: B#[_k - 1] -Bug170.dfy(15,12): Info: A#[_k - 1] +Bug170.dfy(10,13): Info: B#[_k - 1] +Bug170.dfy(15,13): Info: A#[_k - 1] Bug170.dfy(18,14): Info: AA# decreases _k, x Bug170.dfy(26,14): Info: BB# decreases _k, x Bug170.dfy(36,21): Info: _k: ORDINAL @@ -21,13 +21,13 @@ Bug170.dfy(53,17): Info: _k: ORDINAL Bug170.dfy(47,13): Info: A#[_k] Bug170.dfy(46,17): Info: AA# with focal predicates A, B Bug170.dfy(49,4): Info: BB#[_k - 1] -Bug170.dfy(50,11): Info: B#[_k - 1] +Bug170.dfy(50,12): Info: B#[_k - 1] Bug170.dfy(54,13): Info: B#[_k] Bug170.dfy(53,17): Info: BB# with focal predicates B, A Bug170.dfy(56,4): Info: AA#[_k - 1] -Bug170.dfy(57,11): Info: A#[_k - 1] -Bug170.dfy(38,4): Info: B#[_k - 1] -Bug170.dfy(43,4): Info: A#[_k - 1] +Bug170.dfy(57,12): Info: A#[_k - 1] +Bug170.dfy(38,5): Info: B#[_k - 1] +Bug170.dfy(43,5): Info: A#[_k - 1] Bug170.dfy(46,17): Info: AA# decreases _k, x Bug170.dfy(53,17): Info: BB# decreases _k, x Bug170.dfy(46,17): Info: AA# {:induction _k, x} @@ -38,11 +38,11 @@ Bug170.dfy(64,18): Info: _k: ORDINAL Bug170.dfy(69,14): Info: _k: ORDINAL Bug170.dfy(70,14): Info: A#[_k] Bug170.dfy(69,14): Info: AA# with focal predicate A -Bug170.dfy(72,7): Info: A#[_k - 1] +Bug170.dfy(72,8): Info: A#[_k - 1] Bug170.dfy(73,6): Info: AA#[_k - 1] -Bug170.dfy(66,12): Info: A#[_k - 1] +Bug170.dfy(66,13): Info: A#[_k - 1] Bug170.dfy(69,14): Info: AA# decreases _k, x -Bug170.dfy(50,11): Info: Some instances of this call are not inlined. -Bug170.dfy(57,11): Info: Some instances of this call are not inlined. +Bug170.dfy(50,12): Info: Some instances of this call are not inlined. +Bug170.dfy(57,12): Info: Some instances of this call are not inlined. Dafny program verifier finished with 5 verified, 0 errors diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/exceptions/TypecheckErrors.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/exceptions/TypecheckErrors.dfy.expect index 62e9e41df03..13d5abc7d42 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/exceptions/TypecheckErrors.dfy.expect +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/exceptions/TypecheckErrors.dfy.expect @@ -1,10 +1,10 @@ -TypecheckErrors.dfy(7,28): Error: incorrect argument type for method in-parameter 'n' (expected nat, found string) -TypecheckErrors.dfy(8,28): Error: incorrect argument type for method in-parameter 'n' (expected nat, found string) +TypecheckErrors.dfy(7,29): Error: incorrect argument type for method in-parameter 'n' (expected nat, found string) +TypecheckErrors.dfy(8,29): Error: incorrect argument type for method in-parameter 'n' (expected nat, found string) TypecheckErrors.dfy(39,10): Error: member IsFailure does not exist in BadOutcome1?, in :- statement TypecheckErrors.dfy(43,10): Error: member 'PropagateFailure' does not exist in trait 'BadOutcome2' TypecheckErrors.dfy(43,10): Error: The right-hand side of ':-', which is of type 'BadOutcome2?', must have functions 'IsFailure()', 'PropagateFailure()', and 'Extract()' TypecheckErrors.dfy(47,10): Error: number of lhs (1) must be one less than number of rhs (1) for a rhs type (BadOutcome3?) without member Extract -TypecheckErrors.dfy(51,22): Error: incorrect argument type for method in-parameter 'msg' (expected string, found int) +TypecheckErrors.dfy(51,23): Error: incorrect argument type for method in-parameter 'msg' (expected string, found int) TypecheckErrors.dfy(71,4): Error: member IsFailure does not exist in BadVoidOutcome1?, in :- statement TypecheckErrors.dfy(75,4): Error: member 'PropagateFailure' does not exist in trait 'BadVoidOutcome2' TypecheckErrors.dfy(75,4): Error: The right-hand side of ':-', which is of type 'BadVoidOutcome2?', must have functions 'IsFailure()' and 'PropagateFailure()', but not 'Extract()' diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/exports/OpaqueFunctions.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/exports/OpaqueFunctions.dfy.expect index 8c7c7f11ac5..ecac718e52d 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/exports/OpaqueFunctions.dfy.expect +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/exports/OpaqueFunctions.dfy.expect @@ -1,4 +1,4 @@ -OpaqueFunctions.dfy(18,4): Error: a postcondition could not be proved on this return path +OpaqueFunctions.dfy(18,5): Error: a postcondition could not be proved on this return path OpaqueFunctions.dfy(17,14): Related location: this is the postcondition that could not be proved OpaqueFunctions.dfy(58,2): Error: a postcondition could not be proved on this return path OpaqueFunctions.dfy(57,16): Related location: this is the postcondition that could not be proved diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-1958.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-1958.dfy.expect index 7b3eb340bf6..071dcbfdc85 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-1958.dfy.expect +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-1958.dfy.expect @@ -2,17 +2,17 @@ git-issue-1958.dfy(13,16): Error: value does not satisfy the subset constraints git-issue-1958.dfy(18,16): Error: value does not satisfy the subset constraints of 'R' git-issue-1958.dfy(32,4): Error: value does not satisfy the subset constraints of 'R' git-issue-1958.dfy(36,4): Error: value does not satisfy the subset constraints of 'R' -git-issue-1958.dfy(56,16): Error: function precondition could not be proved +git-issue-1958.dfy(56,20): Error: function precondition could not be proved git-issue-1958.dfy(49,13): Related location: this proposition could not be proved -git-issue-1958.dfy(61,4): Error: function precondition could not be proved +git-issue-1958.dfy(61,8): Error: function precondition could not be proved git-issue-1958.dfy(49,13): Related location: this proposition could not be proved -git-issue-1958.dfy(65,4): Error: function precondition could not be proved +git-issue-1958.dfy(65,8): Error: function precondition could not be proved git-issue-1958.dfy(49,13): Related location: this proposition could not be proved -git-issue-1958.dfy(70,9): Error: function precondition could not be proved +git-issue-1958.dfy(70,13): Error: function precondition could not be proved git-issue-1958.dfy(49,13): Related location: this proposition could not be proved git-issue-1958.dfy(77,13): Error: cannot establish the existence of LHS values that satisfy the such-that predicate git-issue-1958.dfy(81,4): Error: cannot establish the existence of LHS values that satisfy the such-that predicate -git-issue-1958.dfy(104,16): Error: function precondition could not be proved +git-issue-1958.dfy(104,20): Error: function precondition could not be proved git-issue-1958.dfy(97,13): Related location: this proposition could not be proved git-issue-1958.dfy(167,7): Error: index out of range diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-3719.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-3719.dfy.expect index 33250c5106b..bbceecbdce7 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-3719.dfy.expect +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-3719.dfy.expect @@ -1,4 +1,4 @@ -git-issue-3719.dfy(12,9): Error: assertion might not hold +git-issue-3719.dfy(12,18): Error: assertion might not hold git-issue-3719.dfy(7,37): Related location: this proposition could not be proved Dafny program verifier finished with 3 verified, 1 error diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-551.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-551.dfy.expect index a21f3686e77..6e9fc4bc7f0 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-551.dfy.expect +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-551.dfy.expect @@ -1,2 +1,2 @@ -git-issue-551.dfy(27,15): Error: a call to a ghost predicate is allowed only in specification contexts (consider declaring the predicate without the 'ghost' keyword) +git-issue-551.dfy(27,26): Error: a call to a ghost predicate is allowed only in specification contexts (consider declaring the predicate without the 'ghost' keyword) 1 resolution/type errors detected in git-issue-551.dfy diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/hofs/ReadsReads.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/hofs/ReadsReads.dfy.expect index 4ce74cb012e..7f67349bb47 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/hofs/ReadsReads.dfy.expect +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/hofs/ReadsReads.dfy.expect @@ -1,10 +1,10 @@ -ReadsReads.dfy(35,6): Error: function precondition could not be proved -ReadsReads.dfy(35,6): Error: insufficient reads clause to invoke function +ReadsReads.dfy(35,11): Error: function precondition could not be proved +ReadsReads.dfy(35,11): Error: insufficient reads clause to invoke function ReadsReads.dfy(40,4): Error: function precondition could not be proved ReadsReads.dfy(40,4): Error: insufficient reads clause to invoke function -ReadsReads.dfy(52,11): Error: function precondition could not be proved -ReadsReads.dfy(52,11): Error: insufficient reads clause to invoke function -ReadsReads.dfy(64,6): Error: insufficient reads clause to invoke function +ReadsReads.dfy(52,16): Error: function precondition could not be proved +ReadsReads.dfy(52,16): Error: insufficient reads clause to invoke function +ReadsReads.dfy(64,14): Error: insufficient reads clause to invoke function ReadsReads.dfy(93,18): Error: assertion might not hold ReadsReads.dfy(95,18): Error: assertion might not hold ReadsReads.dfy(105,18): Error: assertion might not hold diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/proof-obligation-desc/shift-lower-bound.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/proof-obligation-desc/shift-lower-bound.dfy.expect index b59657a0906..cfdac31f3f7 100755 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/proof-obligation-desc/shift-lower-bound.dfy.expect +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/proof-obligation-desc/shift-lower-bound.dfy.expect @@ -1,4 +1,4 @@ -shift-lower-bound.dfy(5,6): Error: rotate amount must be non-negative +shift-lower-bound.dfy(5,16): Error: rotate amount must be non-negative Asserted expression: 0 <= -1 Dafny program verifier finished with 0 verified, 1 error diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/triggers/splitting-triggers-yields-better-precondition-related-errors.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/triggers/splitting-triggers-yields-better-precondition-related-errors.dfy.expect index 98bb2797b8d..af17b521378 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/triggers/splitting-triggers-yields-better-precondition-related-errors.dfy.expect +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/triggers/splitting-triggers-yields-better-precondition-related-errors.dfy.expect @@ -2,7 +2,7 @@ splitting-triggers-yields-better-precondition-related-errors.dfy(7,11): Warning: splitting-triggers-yields-better-precondition-related-errors.dfy(15,11): Warning: Could not find a trigger for this quantifier. Without a trigger, the quantifier may cause brittle verification. To silence this warning, add an explicit trigger using the {:trigger} attribute. For more information, see the section quantifier instantiation rules in the reference manual. splitting-triggers-yields-better-precondition-related-errors.dfy(11,3): Error: a precondition for this call could not be proved splitting-triggers-yields-better-precondition-related-errors.dfy(7,11): Related location: this is the precondition that could not be proved -splitting-triggers-yields-better-precondition-related-errors.dfy(20,2): Error: function precondition could not be proved +splitting-triggers-yields-better-precondition-related-errors.dfy(20,4): Error: function precondition could not be proved splitting-triggers-yields-better-precondition-related-errors.dfy(15,11): Related location: this proposition could not be proved Dafny program verifier finished with 0 verified, 2 errors diff --git a/Source/Scripts/UpdateTests.cs b/Source/Scripts/UpdateTests.cs index 0f676543580..3e8a23a2bf1 100644 --- a/Source/Scripts/UpdateTests.cs +++ b/Source/Scripts/UpdateTests.cs @@ -4,10 +4,10 @@ namespace IntegrationTests; public class UpdateTests { - + public static async Task Main(string[] args) { Environment.SetEnvironmentVariable("DAFNY_INTEGRATION_TESTS_UPDATE_EXPECT_FILE", "true"); - + var files = Directory.GetFiles(args[0]); var key = "integration-tests"; var integrationFiles = files.Where(f => { @@ -37,11 +37,11 @@ public static async Task Main(string[] args) { } Console.WriteLine($"Tests to update:\n{string.Join("\n", failedTestNames)}\n"); - + var needsBuilds = true; for (var index = 0; index < failedTestNames.Count; index++) { var failedTestName = failedTestNames[index]; - Console.WriteLine($"Updating test {index+1}/{failedTestNames.Count} '{failedTestName}'"); + Console.WriteLine($"Updating test {index + 1}/{failedTestNames.Count} '{failedTestName}'"); var integrationTestsDir = $"{repoRoot}/Source/IntegrationTests"; var arguments = new List { "test", integrationTestsDir, $"--filter=DisplayName~{failedTestName}" }; if (!needsBuilds) { diff --git a/docs/DafnyRef/Statements.8b.expect b/docs/DafnyRef/Statements.8b.expect index 7e599dfb192..0732822b503 100644 --- a/docs/DafnyRef/Statements.8b.expect +++ b/docs/DafnyRef/Statements.8b.expect @@ -1,4 +1,4 @@ -text.dfy(6,12): Error: function precondition could not be proved +text.dfy(6,13): Error: function precondition could not be proved text.dfy(3,30): Related location: this proposition could not be proved Dafny program verifier finished with 8 verified, 1 error diff --git a/docs/DafnyRef/Topics.3.expect b/docs/DafnyRef/Topics.3.expect index a5f9b7e52ef..66c482d6870 100644 --- a/docs/DafnyRef/Topics.3.expect +++ b/docs/DafnyRef/Topics.3.expect @@ -1,3 +1,3 @@ text.dfy(6,10): Error: the type of this variable is underspecified -text.dfy(6,15): Error: type parameter 'T' (inferred to be '?') in the function call to 'EmptySet' could not be determined +text.dfy(6,23): Error: type parameter 'T' (inferred to be '?') in the function call to 'EmptySet' could not be determined 2 resolution/type errors detected in text.dfy diff --git a/docs/DafnyRef/Types.20.expect b/docs/DafnyRef/Types.20.expect index b80b729c5fc..df1d037df0b 100644 --- a/docs/DafnyRef/Types.20.expect +++ b/docs/DafnyRef/Types.20.expect @@ -1,5 +1,5 @@ text.dfy(26,0): Error: a postcondition could not be proved on this return path -text.dfy(25,10): Related location: this is the postcondition that could not be proved +text.dfy(25,15): Related location: this is the postcondition that could not be proved text.dfy(10,9): Related location: this proposition could not be proved Dafny program verifier finished with 1 verified, 1 error