Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Let the center of a predicate statement be the keyword #6010

Merged
merged 11 commits into from
Dec 30, 2024
Merged

Let the center of a predicate statement be the keyword #6010

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
11 commits
Select commit Hold shift + click to select a range
0f25030
Let the center of a predicate statement be the keyword ('assert/'assu…
keyboardDrummer Dec 27, 2024
1fe6da5
Update expect files
keyboardDrummer Dec 27, 2024
a524371
Update doc expect file
keyboardDrummer Dec 27, 2024
60ae4fa
Update expect files
keyboardDrummer Dec 27, 2024
6898a25
Update expect files
keyboardDrummer Dec 27, 2024
dec2f40
Update expect file
keyboardDrummer Dec 27, 2024
28fb731
Update doc expect files
keyboardDrummer Dec 27, 2024
94fbe8c
Merge branch 'master' into predicateOrigin
keyboardDrummer Dec 27, 2024
39f1977
Update docs
keyboardDrummer Dec 28, 2024
9574455
Merge branch 'predicateOrigin' of github.com:keyboardDrummer/dafny in…
keyboardDrummer Dec 28, 2024
71c9cc9
Update doc expect files
keyboardDrummer Dec 30, 2024
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
13 changes: 1 addition & 12 deletions Source/DafnyCore/Verifier/Statements/BoogieGenerator.TrPredicateStatement.cs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -149,19 +149,8 @@ private bool TrAssertCondition(PredicateStmt stmt,
var (errorMessage, successMessage) = CustomErrorMessage(stmt.Attributes);
var splits = TrSplitExpr(proofBuilder.Context, stmt.Expr, etran, true, out var splitHappened);
if (!splitHappened) {
IOrigin origin;
if (stmt.Origin is NestedOrigin) {
// The OverrideCenter should move the center from the start of the assertion to the center of the expr.
// For assert ... statements, we don't want to use the override center
// Because that's the location of what was filled in for the ...
// This logic won't be needed anymore once we stop using OverrideCenter.
origin = stmt.Origin;
} else {
origin = new OverrideCenter(stmt.Origin, GetToken(stmt.Expr).Center);
}

var desc = new AssertStatementDescription(stmt, errorMessage, successMessage);
proofBuilder.Add(Assert(origin, etran.TrExpr(stmt.Expr), desc, stmt.Tok, proofBuilder.Context,
proofBuilder.Add(Assert(stmt.Origin, etran.TrExpr(stmt.Expr), desc, stmt.Tok, proofBuilder.Context,
etran.TrAttributes(stmt.Attributes, null)));
} else {
foreach (var split in splits) {
Expand Down
4 changes: 2 additions & 2 deletions ...les/LitTests/LitTest/HigherOrderIntrinsicSpecification/ReadPreconditionBypass3.dfy.expect
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,4 +1,4 @@
ReadPreconditionBypass3.dfy(26,16): Error: assertion might not hold
ReadPreconditionBypass3.dfy(31,16): Error: assertion might not hold
ReadPreconditionBypass3.dfy(26,2): Error: assertion might not hold
ReadPreconditionBypass3.dfy(31,2): Error: assertion might not hold

Dafny program verifier finished with 1 verified, 2 errors
4 changes: 2 additions & 2 deletions ...les/LitTests/LitTest/HigherOrderIntrinsicSpecification/ReadPreconditionBypass4.dfy.expect
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,4 +1,4 @@
ReadPreconditionBypass4.dfy(27,16): Error: assertion might not hold
ReadPreconditionBypass4.dfy(41,16): Error: assertion might not hold
ReadPreconditionBypass4.dfy(27,2): Error: assertion might not hold
ReadPreconditionBypass4.dfy(41,2): Error: assertion might not hold

Dafny program verifier finished with 1 verified, 2 errors
2 changes: 1 addition & 1 deletion Source/IntegrationTests/TestFiles/LitTests/LitTest/ast/reveal/revealConstants.dfy.expect
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,3 +1,3 @@
revealConstants.dfy(10,19): Error: assertion might not hold
revealConstants.dfy(10,2): Error: assertion might not hold

Dafny program verifier finished with 3 verified, 1 error
38 changes: 19 additions & 19 deletions Source/IntegrationTests/TestFiles/LitTests/LitTest/ast/reveal/revealFunctions.dfy.expect
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,25 +1,25 @@
revealFunctions.dfy(90,19): Info: auto-accumulator tail recursive
revealFunctions.dfy(90,19): Info: decreases x
revealFunctions.dfy(15,12): Info: hidden functions: P
revealFunctions.dfy(22,12): Info: hidden functions: P
revealFunctions.dfy(49,21): Info: hidden functions: OpaqueFunc
revealFunctions.dfy(57,11): Info: hidden functions: Natty
revealFunctions.dfy(60,11): Info: hidden functions: Natty
revealFunctions.dfy(15,4): Info: hidden functions: P
revealFunctions.dfy(22,4): Info: hidden functions: P
revealFunctions.dfy(49,4): Info: hidden functions: OpaqueFunc
revealFunctions.dfy(57,2): Info: hidden functions: Natty
revealFunctions.dfy(60,2): Info: hidden functions: Natty
revealFunctions.dfy(79,4): Info: hidden functions: Obj
revealFunctions.dfy(81,18): Info: hidden functions: Obj
revealFunctions.dfy(117,14): Info: hidden functions: Outer
revealFunctions.dfy(118,14): Info: hidden functions: Inner
revealFunctions.dfy(121,14): Info: hidden functions: Outer
revealFunctions.dfy(81,4): Info: hidden functions: Obj
revealFunctions.dfy(117,2): Info: hidden functions: Outer
revealFunctions.dfy(118,2): Info: hidden functions: Inner
revealFunctions.dfy(121,2): Info: hidden functions: Outer
revealFunctions.dfy(131,10): Info: hidden functions: HideInFunction
revealFunctions.dfy(134,10): Info: hidden functions: P
revealFunctions.dfy(138,10): Info: hidden functions: P
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
revealFunctions.dfy(117,14): Error: assertion might not hold
revealFunctions.dfy(118,14): Error: assertion might not hold
revealFunctions.dfy(121,14): Error: assertion might not hold
revealFunctions.dfy(134,10): Error: assertion might not hold
revealFunctions.dfy(138,10): Error: assertion might not hold
revealFunctions.dfy(134,2): Info: hidden functions: P
revealFunctions.dfy(138,2): Info: hidden functions: P
revealFunctions.dfy(15,4): Error: assertion might not hold
revealFunctions.dfy(22,4): Error: assertion might not hold
revealFunctions.dfy(49,4): Error: assertion might not hold
revealFunctions.dfy(117,2): Error: assertion might not hold
revealFunctions.dfy(118,2): Error: assertion might not hold
revealFunctions.dfy(121,2): Error: assertion might not hold
revealFunctions.dfy(134,2): Error: assertion might not hold
revealFunctions.dfy(138,2): Error: assertion might not hold

Dafny program verifier finished with 25 verified, 8 errors
20 changes: 10 additions & 10 deletions Source/IntegrationTests/TestFiles/LitTests/LitTest/ast/reveal/revealInBlock.dfy.expect
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,12 +1,12 @@
revealInBlock.dfy(20,10): Error: assertion might not hold
revealInBlock.dfy(30,14): Error: assertion might not hold
revealInBlock.dfy(33,10): Error: assertion might not hold
revealInBlock.dfy(43,10): Error: assertion might not hold
revealInBlock.dfy(56,10): Error: assertion might not hold
revealInBlock.dfy(67,10): Error: assertion might not hold
revealInBlock.dfy(78,14): Error: assertion might not hold
revealInBlock.dfy(81,10): Error: assertion might not hold
revealInBlock.dfy(91,14): Error: assertion might not hold
revealInBlock.dfy(94,10): Error: assertion might not hold
revealInBlock.dfy(20,2): Error: assertion might not hold
revealInBlock.dfy(30,6): Error: assertion might not hold
revealInBlock.dfy(33,2): Error: assertion might not hold
revealInBlock.dfy(43,2): Error: assertion might not hold
revealInBlock.dfy(56,2): Error: assertion might not hold
revealInBlock.dfy(67,2): Error: assertion might not hold
revealInBlock.dfy(78,6): Error: assertion might not hold
revealInBlock.dfy(81,2): Error: assertion might not hold
revealInBlock.dfy(91,6): Error: assertion might not hold
revealInBlock.dfy(94,2): Error: assertion might not hold

Dafny program verifier finished with 20 verified, 10 errors
2 changes: 1 addition & 1 deletion Source/IntegrationTests/TestFiles/LitTests/LitTest/ast/reveal/revealInExpression.dfy.expect
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,3 +1,3 @@
revealInExpression.dfy(34,14): Error: assertion might not hold
revealInExpression.dfy(34,6): Error: assertion might not hold

Dafny program verifier finished with 15 verified, 1 error
6 changes: 3 additions & 3 deletions Source/IntegrationTests/TestFiles/LitTests/LitTest/ast/statement/AssertBy.dfy.expect
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -21,8 +21,8 @@ method WellFormedness(x: int)
assume x == 3;
}
}
AssertBy.dfy(6,11): Error: assertion might not hold
AssertBy.dfy(7,11): Error: assertion might not hold
AssertBy.dfy(16,11): Error: assertion might not hold
AssertBy.dfy(6,2): Error: assertion might not hold
AssertBy.dfy(7,2): Error: assertion might not hold
AssertBy.dfy(16,2): Error: assertion might not hold

Dafny program verifier finished with 1 verified, 3 errors
12 changes: 6 additions & 6 deletions Source/IntegrationTests/TestFiles/LitTests/LitTest/ast/statement/calls/CallBy.dfy.expect
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,8 +1,8 @@
CallBy.dfy(26,10): Error: assertion might not hold
CallBy.dfy(32,10): Error: assertion might not hold
CallBy.dfy(39,10): Error: assertion might not hold
CallBy.dfy(50,10): Error: assertion might not hold
CallBy.dfy(56,10): Error: assertion might not hold
CallBy.dfy(66,10): Error: assertion might not hold
CallBy.dfy(26,2): Error: assertion might not hold
CallBy.dfy(32,2): Error: assertion might not hold
CallBy.dfy(39,2): Error: assertion might not hold
CallBy.dfy(50,2): Error: assertion might not hold
CallBy.dfy(56,2): Error: assertion might not hold
CallBy.dfy(66,2): Error: assertion might not hold

Dafny program verifier finished with 4 verified, 6 errors
2 changes: 1 addition & 1 deletion Source/IntegrationTests/TestFiles/LitTests/LitTest/ast/statement/calls/CallByHide.dfy.expect
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,3 +1,3 @@
CallByHide.dfy(15,10): Error: assertion might not hold
CallByHide.dfy(15,2): Error: assertion might not hold

Dafny program verifier finished with 2 verified, 1 error
8 changes: 4 additions & 4 deletions Source/IntegrationTests/TestFiles/LitTests/LitTest/ast/statement/opaqueBlock.dfy.expect
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,6 +1,6 @@
opaqueBlock.dfy(15,11): Error: assertion might not hold
opaqueBlock.dfy(28,11): Error: assertion might not hold
opaqueBlock.dfy(42,11): Error: assertion might not hold
opaqueBlock.dfy(15,2): Error: assertion might not hold
opaqueBlock.dfy(28,2): Error: assertion might not hold
opaqueBlock.dfy(42,2): Error: assertion might not hold
opaqueBlock.dfy(49,14): Error: possible division by zero
opaqueBlock.dfy(54,17): Error: variable 'y', which is subject to definite-assignment rules, might be uninitialized here
opaqueBlock.dfy(71,21): Error: assignment might update an object not in the enclosing context's modifies clause
Expand All @@ -11,6 +11,6 @@ opaqueBlock.dfy(127,12): Error: variable 'y', which is subject to definite-assig
opaqueBlock.dfy(130,17): Error: variable 'z', which is subject to definite-assignment rules, might be uninitialized here
opaqueBlock.dfy(142,12): Error: ensures might not hold
opaqueBlock.dfy(206,6): Error: assignment might update an object not in the enclosing context's modifies clause
opaqueBlock.dfy(218,13): Error: assertion might not hold
opaqueBlock.dfy(218,2): Error: assertion might not hold

Dafny program verifier finished with 3 verified, 14 errors
12 changes: 6 additions & 6 deletions Source/IntegrationTests/TestFiles/LitTests/LitTest/cli/errorLimit.dfy.expect
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,8 +1,8 @@
errorLimit.dfy(5,13): Error: assertion might not hold
errorLimit.dfy(7,13): Error: assertion might not hold
errorLimit.dfy(9,13): Error: assertion might not hold
errorLimit.dfy(11,13): Error: assertion might not hold
errorLimit.dfy(13,13): Error: assertion might not hold
errorLimit.dfy(15,13): Error: assertion might not hold
errorLimit.dfy(5,4): Error: assertion might not hold
errorLimit.dfy(7,4): Error: assertion might not hold
errorLimit.dfy(9,4): Error: assertion might not hold
errorLimit.dfy(11,4): Error: assertion might not hold
errorLimit.dfy(13,4): Error: assertion might not hold
errorLimit.dfy(15,4): Error: assertion might not hold

Dafny program verifier finished with 0 verified, 6 errors
4 changes: 2 additions & 2 deletions Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/Array.dfy.expect
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -5,7 +5,7 @@ Array.dfy(318,64): Warning: deprecated style: a semi-colon is not needed here
Array.dfy(13,7): Error: assignment might update an array element not in the enclosing context's modifies clause
Array.dfy(20,15): Error: target object might be null
Array.dfy(26,5): Error: index out of range
Array.dfy(50,19): Error: assertion might not hold
Array.dfy(50,4): Error: assertion might not hold
Array.dfy(58,7): Error: assignment might update an array element not in the enclosing context's modifies clause
Array.dfy(65,7): Error: assignment might update an array element not in the enclosing context's modifies clause
Array.dfy(108,20): Error: upper bound below lower bound or above length of array
Expand All @@ -30,7 +30,7 @@ Array.dfy(258,6): Error: value does not satisfy the subset constraints of 'nat'
Array.dfy(260,4): Error: value does not satisfy the subset constraints of 'nat'
Array.dfy(332,4): Error: assignment might update an object not in the enclosing context's modifies clause
Array.dfy(338,5): Error: assignment might update an array element not in the enclosing context's modifies clause
Array.dfy(353,17): Error: assertion might not hold
Array.dfy(353,4): Error: assertion might not hold
Array.dfy(358,17): Error: left-hand sides that.x and this.x might refer to the same location

Dafny program verifier finished with 41 verified, 27 errors
4 changes: 2 additions & 2 deletions Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/ArrayElementInit.dfy.expect
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,13 +1,13 @@
ArrayElementInit.dfy(13,31): Error: possible division by zero
ArrayElementInit.dfy(19,11): Error: all array indices must be in the domain of the initialization function
ArrayElementInit.dfy(39,11): Error: all array indices must be in the domain of the initialization function
ArrayElementInit.dfy(66,22): Error: assertion might not hold
ArrayElementInit.dfy(66,2): Error: assertion might not hold
ArrayElementInit.dfy(86,21): Error: unless an initializer is provided for the array elements, a new array of 'D' must have empty size
ArrayElementInit.dfy(88,23): Error: unless an initializer is provided for the array elements, a new array of 'D' must have empty size
ArrayElementInit.dfy(102,24): Error: value does not satisfy the subset constraints of 'nat'
ArrayElementInit.dfy(110,32): Error: value does not satisfy the subset constraints of 'nat'
ArrayElementInit.dfy(113,20): Error: given array size must agree with the number of expressions in the initializing display (4)
ArrayElementInit.dfy(139,14): Error: assertion might not hold
ArrayElementInit.dfy(139,2): Error: assertion might not hold
ArrayElementInit.dfy(144,22): Error: function precondition could not be proved
ArrayElementInit.dfy(152,21): Error: unless an initializer is provided for the array elements, a new array of 'D' must have empty size
ArrayElementInit.dfy(154,21): Error: unless an initializer is provided for the array elements, a new array of 'D' must have empty size
Expand Down
4 changes: 2 additions & 2 deletions Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/ArrayElementInitERR.dfy.expect
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,13 +1,13 @@
ArrayElementInitERR.dfy(13,31): Error: possible division by zero
ArrayElementInitERR.dfy(19,11): Error: all array indices must be in the domain of the initialization function
ArrayElementInitERR.dfy(39,11): Error: all array indices must be in the domain of the initialization function
ArrayElementInitERR.dfy(66,22): Error: assertion might not hold
ArrayElementInitERR.dfy(66,2): Error: assertion might not hold
ArrayElementInitERR.dfy(86,21): Error: unless an initializer is provided for the array elements, a new array of 'D' must have empty size
ArrayElementInitERR.dfy(88,23): Error: unless an initializer is provided for the array elements, a new array of 'D' must have empty size
ArrayElementInitERR.dfy(102,24): Error: value does not satisfy the subset constraints of 'nat'
ArrayElementInitERR.dfy(110,32): Error: value does not satisfy the subset constraints of 'nat'
ArrayElementInitERR.dfy(113,20): Error: given array size must agree with the number of expressions in the initializing display (4)
ArrayElementInitERR.dfy(139,14): Error: assertion might not hold
ArrayElementInitERR.dfy(139,2): Error: assertion might not hold
ArrayElementInitERR.dfy(144,22): Error: function precondition could not be proved
ArrayElementInitERR.dfy(152,21): Error: unless an initializer is provided for the array elements, a new array of 'D' must have empty size
ArrayElementInitERR.dfy(154,21): Error: unless an initializer is provided for the array elements, a new array of 'D' must have empty size
Expand Down
4 changes: 2 additions & 2 deletions ...ationTests/TestFiles/LitTests/LitTest/dafny0/AsIs-UnusedTypeParameters.dfy.refresh.expect
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,7 +1,7 @@
AsIs-UnusedTypeParameters.dfy(39,13): Error: assertion might not hold
AsIs-UnusedTypeParameters.dfy(39,6): Error: assertion might not hold
AsIs-UnusedTypeParameters.dfy(41,12): Error: value of expression (of type 'C<F<X, X>>') is not known to be an instance of type 'C<F<X, int>>'
AsIs-UnusedTypeParameters.dfy(43,15): Error: value of expression (of type 'C<F<X, X>>') is not known to be an instance of type 'C<F<X, int>>'
AsIs-UnusedTypeParameters.dfy(57,13): Error: assertion might not hold
AsIs-UnusedTypeParameters.dfy(57,6): Error: assertion might not hold
AsIs-UnusedTypeParameters.dfy(59,12): Error: value of expression (of type 'C<F<X, int>>') is not known to be an instance of type 'C<F<X, X>>'
AsIs-UnusedTypeParameters.dfy(61,15): Error: value of expression (of type 'C<F<X, int>>') is not known to be an instance of type 'C<F<X, X>>'

Expand Down
12 changes: 6 additions & 6 deletions Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/AsIs.dfy.expect
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -3,11 +3,11 @@ AsIs.dfy(62,15): Error: value of expression (of type 'object') is not known to b
AsIs.dfy(64,15): Error: value of expression (of type 'object') is not known to be an instance of type 'B<W, int>'
AsIs.dfy(66,25): Error: value of expression (of type 'object') is not known to be an instance of type 'B<int, int>'
AsIs.dfy(68,15): Error: value of expression (of type 'object') is not known to be an instance of type 'A<W>'
AsIs.dfy(119,13): Error: assertion might not hold
AsIs.dfy(123,14): Error: assertion might not hold
AsIs.dfy(128,14): Error: assertion might not hold
AsIs.dfy(139,15): Error: assertion might not hold
AsIs.dfy(143,15): Error: assertion might not hold
AsIs.dfy(148,15): Error: assertion might not hold
AsIs.dfy(119,4): Error: assertion might not hold
AsIs.dfy(123,4): Error: assertion might not hold
AsIs.dfy(128,4): Error: assertion might not hold
AsIs.dfy(139,4): Error: assertion might not hold
AsIs.dfy(143,4): Error: assertion might not hold
AsIs.dfy(148,4): Error: assertion might not hold

Dafny program verifier finished with 7 verified, 11 errors
12 changes: 6 additions & 6 deletions Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/AsIsAgain.dfy.expect
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -3,11 +3,11 @@ AsIsAgain.dfy(62,15): Error: value of expression (of type 'object') is not known
AsIsAgain.dfy(64,15): Error: value of expression (of type 'object') is not known to be an instance of type 'B<W, int>'
AsIsAgain.dfy(66,25): Error: value of expression (of type 'object') is not known to be an instance of type 'B<int, int>'
AsIsAgain.dfy(68,15): Error: value of expression (of type 'object') is not known to be an instance of type 'A<W>'
AsIsAgain.dfy(119,13): Error: assertion might not hold
AsIsAgain.dfy(123,14): Error: assertion might not hold
AsIsAgain.dfy(128,14): Error: assertion might not hold
AsIsAgain.dfy(139,15): Error: assertion might not hold
AsIsAgain.dfy(143,15): Error: assertion might not hold
AsIsAgain.dfy(148,15): Error: assertion might not hold
AsIsAgain.dfy(119,4): Error: assertion might not hold
AsIsAgain.dfy(123,4): Error: assertion might not hold
AsIsAgain.dfy(128,4): Error: assertion might not hold
AsIsAgain.dfy(139,4): Error: assertion might not hold
AsIsAgain.dfy(143,4): Error: assertion might not hold
AsIsAgain.dfy(148,4): Error: assertion might not hold

Dafny program verifier finished with 7 verified, 11 errors
18 changes: 9 additions & 9 deletions Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/Basics.dfy.expect
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,22 +1,22 @@
Basics.dfy(13,13): Error: variable 'g', which is subject to definite-assignment rules, might be uninitialized here
Basics.dfy(45,13): Error: assertion might not hold
Basics.dfy(45,4): Error: assertion might not hold
Basics.dfy(69,41): Error: assertion might not hold
Basics.dfy(93,13): Error: assertion might not hold
Basics.dfy(99,13): Error: assertion might not hold
Basics.dfy(93,4): Error: assertion might not hold
Basics.dfy(99,4): Error: assertion might not hold
Basics.dfy(112,27): Error: target object might be null
Basics.dfy(114,13): Error: target object might be null
Basics.dfy(148,15): Error: assertion might not hold
Basics.dfy(148,4): Error: assertion might not hold
Basics.dfy(167,9): Error: when left-hand sides a[b[18]] and a[4] refer to the same location, they must be assigned the same value
Basics.dfy(183,9): Error: when left-hand sides x.f and y.f refer to the same location, they must be assigned the same value
Basics.dfy(195,18): Error: assertion might not hold
Basics.dfy(195,4): Error: assertion might not hold
Basics.dfy(197,9): Error: assignment might update an object not in the enclosing context's modifies clause
Basics.dfy(197,9): Error: target object might be null
Basics.dfy(202,11): Error: left-hand sides m.x and m.x might refer to the same location
Basics.dfy(213,14): Error: assertion might not hold
Basics.dfy(213,4): Error: assertion might not hold
Basics.dfy(273,9): Error: when left-hand sides d.x and c.x refer to the same location, they must be assigned the same value
Basics.dfy(463,11): Error: assertion might not hold
Basics.dfy(474,18): Error: assertion might not hold
Basics.dfy(476,11): Error: assertion might not hold
Basics.dfy(463,2): Error: assertion might not hold
Basics.dfy(474,4): Error: assertion might not hold
Basics.dfy(476,2): Error: assertion might not hold
Basics.dfy(623,17): Error: result of operation might violate newtype constraint for 'int8'

Dafny program verifier finished with 48 verified, 20 errors
6 changes: 3 additions & 3 deletions Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/BigOrdinals.dfy.expect
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,12 +1,12 @@
BigOrdinals.dfy(18,11): Error: a negative integer cannot be converted to an ORDINAL
BigOrdinals.dfy(20,11): Error: value to be converted might be bigger than every natural number
BigOrdinals.dfy(35,13): Error: assertion might not hold
BigOrdinals.dfy(53,13): Error: assertion might not hold
BigOrdinals.dfy(35,4): Error: assertion might not hold
BigOrdinals.dfy(53,4): Error: assertion might not hold
BigOrdinals.dfy(64,15): Error: ORDINAL subtraction might underflow a limit ordinal (that is, RHS might be too large)
BigOrdinals.dfy(66,15): Error: ORDINAL subtraction might underflow a limit ordinal (that is, RHS might be too large)
BigOrdinals.dfy(68,15): Error: ORDINAL subtraction might underflow a limit ordinal (that is, RHS might be too large)
BigOrdinals.dfy(73,15): Error: ORDINAL subtraction might underflow a limit ordinal (that is, RHS might be too large)
BigOrdinals.dfy(88,13): Error: assertion might not hold
BigOrdinals.dfy(88,4): Error: assertion might not hold
BigOrdinals.dfy(113,9): Error: value does not satisfy the subset constraints of 'ConstrainedOrdinal'
BigOrdinals.dfy(120,9): Error: value does not satisfy the subset constraints of 'ConstrainedOrdinal'

Expand Down
Loading
Loading