summaryrefslogtreecommitdiff
path: root/Test/dafny0/Answer
diff options
context:
space:
mode:
Diffstat (limited to 'Test/dafny0/Answer')
-rw-r--r--Test/dafny0/Answer123
1 files changed, 73 insertions, 50 deletions
diff --git a/Test/dafny0/Answer b/Test/dafny0/Answer
index c82d3803..75025b2f 100644
--- a/Test/dafny0/Answer
+++ b/Test/dafny0/Answer
@@ -85,7 +85,7 @@ TypeTests.dfy(87,8): Error: sorry, cannot instantiate 'array' type with a subran
NatTypes.dfy(7,5): Error: value assigned to a nat must be non-negative
Execution trace:
(0,0): anon0
-NatTypes.dfy(31,5): Error: value assigned to a nat must be non-negative
+NatTypes.dfy(31,10): Error: value assigned to a nat must be non-negative
Execution trace:
(0,0): anon0
NatTypes.dfy(19,3): anon10_LoopHead
@@ -111,7 +111,7 @@ Execution trace:
(0,0): anon0
(0,0): anon5_Else
(0,0): anon6_Then
-NatTypes.dfy(86,16): Error: value assigned to a nat must be non-negative
+NatTypes.dfy(86,19): Error: value assigned to a nat must be non-negative
Execution trace:
(0,0): anon0
(0,0): anon3_Then
@@ -450,7 +450,7 @@ ParseErrors.dfy(18,18): error: chaining not allowed from the previous operator
9 parse errors detected in ParseErrors.dfy
-------------------- Array.dfy --------------------
-Array.dfy(10,12): Error: assignment may update an array element not in the enclosing method's modifies clause
+Array.dfy(10,8): Error: assignment may update an array element not in the enclosing method's modifies clause
Execution trace:
(0,0): anon0
(0,0): anon5_Then
@@ -465,13 +465,13 @@ Execution trace:
Array.dfy(48,20): Error: assertion violation
Execution trace:
(0,0): anon0
-Array.dfy(56,12): Error: assignment may update an array element not in the enclosing method's modifies clause
+Array.dfy(56,8): Error: assignment may update an array element not in the enclosing method's modifies clause
Execution trace:
(0,0): anon0
(0,0): anon5_Then
(0,0): anon2
(0,0): anon6_Then
-Array.dfy(63,12): Error: assignment may update an array element not in the enclosing method's modifies clause
+Array.dfy(63,8): Error: assignment may update an array element not in the enclosing method's modifies clause
Execution trace:
(0,0): anon0
(0,0): anon5_Then
@@ -490,10 +490,10 @@ Execution trace:
(0,0): anon7_Else
(0,0): anon8_Then
(0,0): anon9_Then
-Array.dfy(131,10): Error: assignment may update an array element not in the enclosing method's modifies clause
+Array.dfy(131,6): Error: assignment may update an array element not in the enclosing method's modifies clause
Execution trace:
(0,0): anon0
-Array.dfy(138,10): Error: assignment may update an array element not in the enclosing method's modifies clause
+Array.dfy(138,6): Error: assignment may update an array element not in the enclosing method's modifies clause
Execution trace:
(0,0): anon0
@@ -598,8 +598,31 @@ Execution trace:
(0,0): anon10
Basics.dfy(66,95): anon18_Else
(0,0): anon12
+Basics.dfy(86,16): Error: assertion violation
+Execution trace:
+ (0,0): anon0
+ (0,0): anon10_Then
+Basics.dfy(99,12): Error: left-hand sides 0 and 1 may refer to the same location
+Execution trace:
+ (0,0): anon0
+ (0,0): anon3
+ (0,0): anon11_Else
+ (0,0): anon6
+ (0,0): anon12_Then
+Basics.dfy(105,10): Error: left-hand sides 0 and 1 may refer to the same location
+Execution trace:
+ (0,0): anon0
+ (0,0): anon10_Then
+ (0,0): anon3
+ (0,0): anon11_Then
+ (0,0): anon6
+ (0,0): anon12_Then
+ (0,0): anon9
+Basics.dfy(119,10): Error: left-hand sides 0 and 1 may refer to the same location
+Execution trace:
+ (0,0): anon0
-Dafny program verifier finished with 7 verified, 2 errors
+Dafny program verifier finished with 9 verified, 6 errors
-------------------- ControlStructures.dfy --------------------
ControlStructures.dfy(5,3): Error: missing case in case statement: Blue
@@ -638,112 +661,112 @@ ControlStructures.dfy(72,3): Error: alternative cases fail to cover all possibil
Execution trace:
(0,0): anon0
(0,0): anon5_Else
-ControlStructures.dfy(218,18): Error: assertion violation
+ControlStructures.dfy(215,18): Error: assertion violation
Execution trace:
(0,0): anon0
- ControlStructures.dfy(197,3): anon62_LoopHead
+ ControlStructures.dfy(194,3): anon62_LoopHead
(0,0): anon62_LoopBody
- ControlStructures.dfy(197,3): anon63_Else
+ ControlStructures.dfy(194,3): anon63_Else
(0,0): anon3
- ControlStructures.dfy(197,3): anon64_Else
+ ControlStructures.dfy(194,3): anon64_Else
(0,0): anon5
- ControlStructures.dfy(201,5): anon65_LoopHead
+ ControlStructures.dfy(198,5): anon65_LoopHead
(0,0): anon65_LoopBody
- ControlStructures.dfy(201,5): anon66_Else
+ ControlStructures.dfy(198,5): anon66_Else
(0,0): anon8
- ControlStructures.dfy(201,5): anon67_Else
+ ControlStructures.dfy(198,5): anon67_Else
(0,0): anon10
(0,0): anon71_Then
- ControlStructures.dfy(213,9): anon72_LoopHead
+ ControlStructures.dfy(210,9): anon72_LoopHead
(0,0): anon72_LoopBody
- ControlStructures.dfy(213,9): anon73_Else
+ ControlStructures.dfy(210,9): anon73_Else
(0,0): anon20
(0,0): anon74_Then
(0,0): anon29
-ControlStructures.dfy(235,21): Error: assertion violation
+ControlStructures.dfy(232,21): Error: assertion violation
Execution trace:
(0,0): anon0
- ControlStructures.dfy(197,3): anon62_LoopHead
+ ControlStructures.dfy(194,3): anon62_LoopHead
(0,0): anon62_LoopBody
- ControlStructures.dfy(197,3): anon63_Else
+ ControlStructures.dfy(194,3): anon63_Else
(0,0): anon3
- ControlStructures.dfy(197,3): anon64_Else
+ ControlStructures.dfy(194,3): anon64_Else
(0,0): anon5
- ControlStructures.dfy(201,5): anon65_LoopHead
+ ControlStructures.dfy(198,5): anon65_LoopHead
(0,0): anon65_LoopBody
- ControlStructures.dfy(201,5): anon66_Else
+ ControlStructures.dfy(198,5): anon66_Else
(0,0): anon8
- ControlStructures.dfy(201,5): anon67_Else
+ ControlStructures.dfy(198,5): anon67_Else
(0,0): anon10
(0,0): anon71_Then
- ControlStructures.dfy(213,9): anon72_LoopHead
+ ControlStructures.dfy(210,9): anon72_LoopHead
(0,0): anon72_LoopBody
- ControlStructures.dfy(213,9): anon73_Else
+ ControlStructures.dfy(210,9): anon73_Else
(0,0): anon20
- ControlStructures.dfy(213,9): anon74_Else
+ ControlStructures.dfy(210,9): anon74_Else
(0,0): anon22
(0,0): anon75_Then
(0,0): after_4
- ControlStructures.dfy(224,7): anon77_LoopHead
+ ControlStructures.dfy(221,7): anon77_LoopHead
(0,0): anon77_LoopBody
- ControlStructures.dfy(224,7): anon78_Else
+ ControlStructures.dfy(221,7): anon78_Else
(0,0): anon33
- ControlStructures.dfy(224,7): anon79_Else
+ ControlStructures.dfy(221,7): anon79_Else
(0,0): anon35
(0,0): anon81_Then
(0,0): anon38
(0,0): after_9
(0,0): anon86_Then
(0,0): anon53
-ControlStructures.dfy(238,30): Error: assertion violation
+ControlStructures.dfy(235,30): Error: assertion violation
Execution trace:
(0,0): anon0
- ControlStructures.dfy(197,3): anon62_LoopHead
+ ControlStructures.dfy(194,3): anon62_LoopHead
(0,0): anon62_LoopBody
- ControlStructures.dfy(197,3): anon63_Else
+ ControlStructures.dfy(194,3): anon63_Else
(0,0): anon3
- ControlStructures.dfy(197,3): anon64_Else
+ ControlStructures.dfy(194,3): anon64_Else
(0,0): anon5
- ControlStructures.dfy(201,5): anon65_LoopHead
+ ControlStructures.dfy(198,5): anon65_LoopHead
(0,0): anon65_LoopBody
- ControlStructures.dfy(201,5): anon66_Else
+ ControlStructures.dfy(198,5): anon66_Else
(0,0): anon8
- ControlStructures.dfy(201,5): anon67_Else
+ ControlStructures.dfy(198,5): anon67_Else
(0,0): anon10
(0,0): anon68_Then
(0,0): after_5
(0,0): anon87_Then
(0,0): anon88_Then
(0,0): anon58
-ControlStructures.dfy(241,17): Error: assertion violation
+ControlStructures.dfy(238,17): Error: assertion violation
Execution trace:
(0,0): anon0
- ControlStructures.dfy(197,3): anon62_LoopHead
+ ControlStructures.dfy(194,3): anon62_LoopHead
(0,0): anon62_LoopBody
- ControlStructures.dfy(197,3): anon63_Else
+ ControlStructures.dfy(194,3): anon63_Else
(0,0): anon3
- ControlStructures.dfy(197,3): anon64_Else
+ ControlStructures.dfy(194,3): anon64_Else
(0,0): anon5
- ControlStructures.dfy(201,5): anon65_LoopHead
+ ControlStructures.dfy(198,5): anon65_LoopHead
(0,0): anon65_LoopBody
- ControlStructures.dfy(201,5): anon66_Else
+ ControlStructures.dfy(198,5): anon66_Else
(0,0): anon8
- ControlStructures.dfy(201,5): anon67_Else
+ ControlStructures.dfy(198,5): anon67_Else
(0,0): anon10
(0,0): anon71_Then
- ControlStructures.dfy(213,9): anon72_LoopHead
+ ControlStructures.dfy(210,9): anon72_LoopHead
(0,0): anon72_LoopBody
- ControlStructures.dfy(213,9): anon73_Else
+ ControlStructures.dfy(210,9): anon73_Else
(0,0): anon20
- ControlStructures.dfy(213,9): anon74_Else
+ ControlStructures.dfy(210,9): anon74_Else
(0,0): anon22
(0,0): anon75_Then
(0,0): after_4
- ControlStructures.dfy(224,7): anon77_LoopHead
+ ControlStructures.dfy(221,7): anon77_LoopHead
(0,0): anon77_LoopBody
- ControlStructures.dfy(224,7): anon78_Else
+ ControlStructures.dfy(221,7): anon78_Else
(0,0): anon33
- ControlStructures.dfy(224,7): anon79_Else
+ ControlStructures.dfy(221,7): anon79_Else
(0,0): anon35
(0,0): anon82_Then
(0,0): anon85_Then
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-30 12:45:37 +0000