diff options
author | 2013-08-02 21:12:01 -0700 | |
---|---|---|
committer | 2013-08-02 21:12:01 -0700 | |
commit | 0487bbe1d95c08a458e496240547127f03a7be3b (patch) | |
tree | 35e6c7350b580757691bb0b7f0347ef61a4ed3e7 /Test/dafny0 | |
parent | 41f1a6131273ca0900d03a7adfaec96443a2cb2f (diff) |
More and improved CaptureState info
Diffstat (limited to 'Test/dafny0')
-rw-r--r-- | Test/dafny0/Answer | 424 |
1 files changed, 235 insertions, 189 deletions
diff --git a/Test/dafny0/Answer b/Test/dafny0/Answer index eec55394..c21ddbc8 100644 --- a/Test/dafny0/Answer +++ b/Test/dafny0/Answer @@ -122,11 +122,13 @@ Execution trace: (0,0): anon3_Then
NatTypes.dfy(104,45): Error: value assigned to a nat must be non-negative
Execution trace:
+ (0,0): anon0
(0,0): anon6_Else
(0,0): anon7_Else
(0,0): anon8_Then
NatTypes.dfy(127,21): Error: value assigned to a nat must be non-negative
Execution trace:
+ (0,0): anon0
(0,0): anon3_Then
Dafny program verifier finished with 15 verified, 9 errors
@@ -134,6 +136,7 @@ Dafny program verifier finished with 15 verified, 9 errors -------------------- Definedness.dfy --------------------
Definedness.dfy(8,7): Error: possible division by zero
Execution trace:
+ (0,0): anon0
(0,0): anon3_Else
Definedness.dfy(15,16): Error: possible division by zero
Execution trace:
@@ -201,88 +204,88 @@ Execution trace: (0,0): anon0
Definedness.dfy(105,15): Error: possible division by zero
Execution trace:
- Definedness.dfy(105,5): anon8_LoopHead
- (0,0): anon8_LoopBody
- Definedness.dfy(105,5): anon9_Else
+ Definedness.dfy(105,5): anon7_LoopHead
+ (0,0): anon7_LoopBody
+ Definedness.dfy(105,5): anon8_Else
Definedness.dfy(114,23): Error: possible violation of function precondition
Execution trace:
(0,0): anon0
- Definedness.dfy(113,5): anon13_LoopHead
- (0,0): anon13_LoopBody
- (0,0): anon14_Then
+ Definedness.dfy(113,5): anon12_LoopHead
+ (0,0): anon12_LoopBody
+ (0,0): anon13_Then
Definedness.dfy(120,17): Error: possible violation of function precondition
Execution trace:
(0,0): anon0
- Definedness.dfy(113,5): anon13_LoopHead
- (0,0): anon13_LoopBody
- Definedness.dfy(113,5): anon14_Else
- (0,0): anon15_Then
- Definedness.dfy(119,5): anon16_LoopHead
- (0,0): anon16_LoopBody
- (0,0): anon17_Then
+ Definedness.dfy(113,5): anon12_LoopHead
+ (0,0): anon12_LoopBody
+ Definedness.dfy(113,5): anon13_Else
+ (0,0): anon14_Then
+ Definedness.dfy(119,5): anon15_LoopHead
+ (0,0): anon15_LoopBody
+ (0,0): anon16_Then
Definedness.dfy(130,17): Error: possible violation of function precondition
Execution trace:
(0,0): anon0
- Definedness.dfy(129,5): anon7_LoopHead
- (0,0): anon7_LoopBody
- (0,0): anon8_Then
+ Definedness.dfy(129,5): anon6_LoopHead
+ (0,0): anon6_LoopBody
+ (0,0): anon7_Then
Definedness.dfy(130,22): Error BP5004: This loop invariant might not hold on entry.
Execution trace:
(0,0): anon0
Definedness.dfy(131,17): Error: possible violation of function precondition
Execution trace:
(0,0): anon0
- Definedness.dfy(129,5): anon7_LoopHead
- (0,0): anon7_LoopBody
- (0,0): anon8_Then
+ Definedness.dfy(129,5): anon6_LoopHead
+ (0,0): anon6_LoopBody
+ (0,0): anon7_Then
Definedness.dfy(140,15): Error: possible division by zero
Execution trace:
(0,0): anon0
- Definedness.dfy(140,5): anon9_LoopHead
- (0,0): anon9_LoopBody
- Definedness.dfy(140,5): anon10_Else
+ Definedness.dfy(140,5): anon8_LoopHead
+ (0,0): anon8_LoopBody
+ Definedness.dfy(140,5): anon9_Else
Definedness.dfy(159,15): Error: possible division by zero
Execution trace:
(0,0): anon0
- Definedness.dfy(153,5): anon17_LoopHead
- (0,0): anon17_LoopBody
- Definedness.dfy(153,5): anon18_Else
- (0,0): anon19_Then
+ Definedness.dfy(153,5): anon16_LoopHead
+ (0,0): anon16_LoopBody
+ Definedness.dfy(153,5): anon17_Else
+ (0,0): anon18_Then
(0,0): anon5
- (0,0): anon20_Then
- Definedness.dfy(159,5): anon21_LoopHead
- (0,0): anon21_LoopBody
- Definedness.dfy(159,5): anon22_Else
+ (0,0): anon19_Then
+ Definedness.dfy(159,5): anon20_LoopHead
+ (0,0): anon20_LoopBody
+ Definedness.dfy(159,5): anon21_Else
Definedness.dfy(172,28): Error BP5004: This loop invariant might not hold on entry.
Execution trace:
(0,0): anon0
Definedness.dfy(178,17): Error: possible violation of function precondition
Execution trace:
(0,0): anon0
- Definedness.dfy(170,5): anon19_LoopHead
- (0,0): anon19_LoopBody
- Definedness.dfy(170,5): anon20_Else
- (0,0): anon21_Then
- Definedness.dfy(177,5): anon22_LoopHead
- (0,0): anon22_LoopBody
+ Definedness.dfy(170,5): anon18_LoopHead
+ (0,0): anon18_LoopBody
+ Definedness.dfy(170,5): anon19_Else
+ (0,0): anon20_Then
+ Definedness.dfy(177,5): anon21_LoopHead
+ (0,0): anon21_LoopBody
+ (0,0): anon22_Then
(0,0): anon23_Then
- (0,0): anon24_Then
(0,0): anon11
Definedness.dfy(193,19): Error: possible division by zero
Execution trace:
(0,0): anon0
- Definedness.dfy(191,5): anon7_LoopHead
- (0,0): anon7_LoopBody
- (0,0): anon8_Then
+ Definedness.dfy(191,5): anon6_LoopHead
+ (0,0): anon6_LoopBody
+ (0,0): anon7_Then
Definedness.dfy(193,23): Error BP5004: This loop invariant might not hold on entry.
Execution trace:
(0,0): anon0
Definedness.dfy(193,28): Error: possible division by zero
Execution trace:
(0,0): anon0
- Definedness.dfy(191,5): anon7_LoopHead
- (0,0): anon7_LoopBody
- (0,0): anon8_Then
+ Definedness.dfy(191,5): anon6_LoopHead
+ (0,0): anon6_LoopBody
+ (0,0): anon7_Then
Definedness.dfy(212,10): Error BP5003: A postcondition might not hold on this return path.
Definedness.dfy(214,46): Related location: This is the postcondition that might not hold.
Execution trace:
@@ -290,12 +293,14 @@ Execution trace: (0,0): anon5_Else
Definedness.dfy(221,22): Error: target object may be null
Execution trace:
+ (0,0): anon0
(0,0): anon5_Then
(0,0): anon2
(0,0): anon6_Then
Definedness.dfy(234,10): Error BP5003: A postcondition might not hold on this return path.
Definedness.dfy(237,24): Related location: This is the postcondition that might not hold.
Execution trace:
+ (0,0): anon0
(0,0): anon7_Then
(0,0): anon2
(0,0): anon8_Else
@@ -306,6 +311,7 @@ Dafny program verifier finished with 21 verified, 37 errors FunctionSpecifications.dfy(32,25): Error BP5003: A postcondition might not hold on this return path.
FunctionSpecifications.dfy(28,13): Related location: This is the postcondition that might not hold.
Execution trace:
+ (0,0): anon0
(0,0): anon8_Else
(0,0): anon9_Else
(0,0): anon10_Then
@@ -313,6 +319,7 @@ Execution trace: FunctionSpecifications.dfy(42,3): Error BP5003: A postcondition might not hold on this return path.
FunctionSpecifications.dfy(37,24): Related location: This is the postcondition that might not hold.
Execution trace:
+ (0,0): anon0
(0,0): anon11_Else
(0,0): anon14_Else
(0,0): anon15_Then
@@ -324,6 +331,7 @@ Execution trace: FunctionSpecifications.dfy(56,10): Error BP5003: A postcondition might not hold on this return path.
FunctionSpecifications.dfy(57,22): Related location: This is the postcondition that might not hold.
Execution trace:
+ (0,0): anon0
(0,0): anon5_Else
Dafny program verifier finished with 8 verified, 4 errors
@@ -477,35 +485,41 @@ Execution trace: (0,0): anon11
Array.dfy(117,8): Error: insufficient reads clause to read the indicated range of array elements
Execution trace:
+ (0,0): anon0
(0,0): anon9_Else
(0,0): anon10_Then
(0,0): anon11_Then
(0,0): anon12_Then
Array.dfy(119,8): Error: insufficient reads clause to read the indicated range of array elements
Execution trace:
+ (0,0): anon0
(0,0): anon9_Else
(0,0): anon10_Then
(0,0): anon11_Then
(0,0): anon12_Else
Array.dfy(120,8): Error: insufficient reads clause to read the indicated range of array elements
Execution trace:
+ (0,0): anon0
(0,0): anon9_Else
(0,0): anon10_Then
(0,0): anon11_Then
(0,0): anon12_Else
Array.dfy(121,8): Error: insufficient reads clause to read the indicated range of array elements
Execution trace:
+ (0,0): anon0
(0,0): anon9_Else
(0,0): anon10_Then
(0,0): anon11_Then
(0,0): anon12_Else
Array.dfy(147,6): Error: insufficient reads clause to read array element
Execution trace:
+ (0,0): anon0
(0,0): anon7_Else
(0,0): anon8_Then
(0,0): anon9_Then
Array.dfy(155,6): Error: insufficient reads clause to read array element
Execution trace:
+ (0,0): anon0
(0,0): anon7_Else
(0,0): anon8_Then
(0,0): anon9_Then
@@ -656,6 +670,7 @@ Modules2.dfy(50,11): Error: The name f ambiguously refers to a static member in -------------------- BadFunction.dfy --------------------
BadFunction.dfy(6,3): Error: failure to decrease termination measure
Execution trace:
+ (0,0): anon0
(0,0): anon3_Else
Dafny program verifier finished with 2 verified, 1 error
@@ -768,6 +783,7 @@ Execution trace: (0,0): anon10_Then
ControlStructures.dfy(51,3): Error: missing case in case statement: Red
Execution trace:
+ (0,0): anon0
(0,0): anon8_Else
(0,0): anon9_Else
(0,0): anon10_Else
@@ -780,89 +796,89 @@ Execution trace: ControlStructures.dfy(215,18): Error: assertion violation
Execution trace:
(0,0): anon0
- ControlStructures.dfy(194,3): anon62_LoopHead
+ ControlStructures.dfy(194,3): anon59_LoopHead
+ (0,0): anon59_LoopBody
+ ControlStructures.dfy(194,3): anon60_Else
+ ControlStructures.dfy(194,3): anon61_Else
+ ControlStructures.dfy(198,5): anon62_LoopHead
(0,0): anon62_LoopBody
- ControlStructures.dfy(194,3): anon63_Else
- ControlStructures.dfy(194,3): anon64_Else
- ControlStructures.dfy(198,5): anon65_LoopHead
- (0,0): anon65_LoopBody
- ControlStructures.dfy(198,5): anon66_Else
- ControlStructures.dfy(198,5): anon67_Else
+ ControlStructures.dfy(198,5): anon63_Else
+ ControlStructures.dfy(198,5): anon64_Else
+ (0,0): anon68_Then
+ ControlStructures.dfy(210,9): anon69_LoopHead
+ (0,0): anon69_LoopBody
+ ControlStructures.dfy(210,9): anon70_Else
(0,0): anon71_Then
- ControlStructures.dfy(210,9): anon72_LoopHead
- (0,0): anon72_LoopBody
- ControlStructures.dfy(210,9): anon73_Else
- (0,0): anon74_Then
ControlStructures.dfy(232,21): Error: assertion violation
Execution trace:
(0,0): anon0
- ControlStructures.dfy(194,3): anon62_LoopHead
+ ControlStructures.dfy(194,3): anon59_LoopHead
+ (0,0): anon59_LoopBody
+ ControlStructures.dfy(194,3): anon60_Else
+ ControlStructures.dfy(194,3): anon61_Else
+ ControlStructures.dfy(198,5): anon62_LoopHead
(0,0): anon62_LoopBody
- ControlStructures.dfy(194,3): anon63_Else
- ControlStructures.dfy(194,3): anon64_Else
- ControlStructures.dfy(198,5): anon65_LoopHead
- (0,0): anon65_LoopBody
- ControlStructures.dfy(198,5): anon66_Else
- ControlStructures.dfy(198,5): anon67_Else
- (0,0): anon71_Then
- ControlStructures.dfy(210,9): anon72_LoopHead
- (0,0): anon72_LoopBody
- ControlStructures.dfy(210,9): anon73_Else
- ControlStructures.dfy(210,9): anon74_Else
- (0,0): anon75_Then
+ ControlStructures.dfy(198,5): anon63_Else
+ ControlStructures.dfy(198,5): anon64_Else
+ (0,0): anon68_Then
+ ControlStructures.dfy(210,9): anon69_LoopHead
+ (0,0): anon69_LoopBody
+ ControlStructures.dfy(210,9): anon70_Else
+ ControlStructures.dfy(210,9): anon71_Else
+ (0,0): anon72_Then
(0,0): after_4
- ControlStructures.dfy(221,7): anon77_LoopHead
- (0,0): anon77_LoopBody
- ControlStructures.dfy(221,7): anon78_Else
- ControlStructures.dfy(221,7): anon79_Else
- (0,0): anon81_Then
+ ControlStructures.dfy(221,7): anon74_LoopHead
+ (0,0): anon74_LoopBody
+ ControlStructures.dfy(221,7): anon75_Else
+ ControlStructures.dfy(221,7): anon76_Else
+ (0,0): anon78_Then
(0,0): anon38
(0,0): after_9
- (0,0): anon86_Then
- (0,0): anon53
+ (0,0): anon83_Then
+ (0,0): anon52
ControlStructures.dfy(235,30): Error: assertion violation
Execution trace:
(0,0): anon0
- ControlStructures.dfy(194,3): anon62_LoopHead
+ ControlStructures.dfy(194,3): anon59_LoopHead
+ (0,0): anon59_LoopBody
+ ControlStructures.dfy(194,3): anon60_Else
+ ControlStructures.dfy(194,3): anon61_Else
+ ControlStructures.dfy(198,5): anon62_LoopHead
(0,0): anon62_LoopBody
- ControlStructures.dfy(194,3): anon63_Else
- ControlStructures.dfy(194,3): anon64_Else
- ControlStructures.dfy(198,5): anon65_LoopHead
- (0,0): anon65_LoopBody
- ControlStructures.dfy(198,5): anon66_Else
- ControlStructures.dfy(198,5): anon67_Else
- (0,0): anon68_Then
+ ControlStructures.dfy(198,5): anon63_Else
+ ControlStructures.dfy(198,5): anon64_Else
+ (0,0): anon65_Then
(0,0): after_5
- (0,0): anon87_Then
- (0,0): anon88_Then
- (0,0): anon58
+ (0,0): anon84_Then
+ (0,0): anon85_Then
+ (0,0): anon56
ControlStructures.dfy(238,17): Error: assertion violation
Execution trace:
(0,0): anon0
- ControlStructures.dfy(194,3): anon62_LoopHead
+ ControlStructures.dfy(194,3): anon59_LoopHead
+ (0,0): anon59_LoopBody
+ ControlStructures.dfy(194,3): anon60_Else
+ ControlStructures.dfy(194,3): anon61_Else
+ ControlStructures.dfy(198,5): anon62_LoopHead
(0,0): anon62_LoopBody
- ControlStructures.dfy(194,3): anon63_Else
- ControlStructures.dfy(194,3): anon64_Else
- ControlStructures.dfy(198,5): anon65_LoopHead
- (0,0): anon65_LoopBody
- ControlStructures.dfy(198,5): anon66_Else
- ControlStructures.dfy(198,5): anon67_Else
- (0,0): anon71_Then
- ControlStructures.dfy(210,9): anon72_LoopHead
- (0,0): anon72_LoopBody
- ControlStructures.dfy(210,9): anon73_Else
- ControlStructures.dfy(210,9): anon74_Else
- (0,0): anon75_Then
+ ControlStructures.dfy(198,5): anon63_Else
+ ControlStructures.dfy(198,5): anon64_Else
+ (0,0): anon68_Then
+ ControlStructures.dfy(210,9): anon69_LoopHead
+ (0,0): anon69_LoopBody
+ ControlStructures.dfy(210,9): anon70_Else
+ ControlStructures.dfy(210,9): anon71_Else
+ (0,0): anon72_Then
(0,0): after_4
- ControlStructures.dfy(221,7): anon77_LoopHead
- (0,0): anon77_LoopBody
- ControlStructures.dfy(221,7): anon78_Else
- ControlStructures.dfy(221,7): anon79_Else
+ ControlStructures.dfy(221,7): anon74_LoopHead
+ (0,0): anon74_LoopBody
+ ControlStructures.dfy(221,7): anon75_Else
+ ControlStructures.dfy(221,7): anon76_Else
+ (0,0): anon79_Then
(0,0): anon82_Then
- (0,0): anon85_Then
(0,0): after_8
- (0,0): anon89_Then
- (0,0): anon61
+ (0,0): anon86_Then
+ (0,0): anon58
Dafny program verifier finished with 22 verified, 10 errors
@@ -876,49 +892,50 @@ Execution trace: Termination.dfy(105,3): Error: cannot prove termination; try supplying a decreases clause for the loop
Execution trace:
(0,0): anon0
- Termination.dfy(105,3): anon7_LoopHead
- (0,0): anon7_LoopBody
+ Termination.dfy(105,3): anon6_LoopHead
+ (0,0): anon6_LoopBody
+ Termination.dfy(105,3): anon7_Else
Termination.dfy(105,3): anon8_Else
- Termination.dfy(105,3): anon9_Else
Termination.dfy(113,3): Error: cannot prove termination; try supplying a decreases clause for the loop
Execution trace:
(0,0): anon0
- Termination.dfy(113,3): anon9_LoopHead
- (0,0): anon9_LoopBody
- Termination.dfy(113,3): anon10_Else
- (0,0): anon11_Then
+ Termination.dfy(113,3): anon8_LoopHead
+ (0,0): anon8_LoopBody
+ Termination.dfy(113,3): anon9_Else
+ (0,0): anon10_Then
(0,0): anon5
- Termination.dfy(113,3): anon12_Else
+ Termination.dfy(113,3): anon11_Else
Termination.dfy(122,3): Error: decreases expression might not decrease
Execution trace:
(0,0): anon0
- Termination.dfy(122,3): anon9_LoopHead
- (0,0): anon9_LoopBody
- Termination.dfy(122,3): anon10_Else
- (0,0): anon11_Then
+ Termination.dfy(122,3): anon8_LoopHead
+ (0,0): anon8_LoopBody
+ Termination.dfy(122,3): anon9_Else
+ (0,0): anon10_Then
(0,0): anon5
- Termination.dfy(122,3): anon12_Else
+ Termination.dfy(122,3): anon11_Else
Termination.dfy(123,17): Error: decreases expression must be bounded below by 0 at end of loop iteration
Execution trace:
(0,0): anon0
- Termination.dfy(122,3): anon9_LoopHead
- (0,0): anon9_LoopBody
- Termination.dfy(122,3): anon10_Else
- (0,0): anon11_Then
+ Termination.dfy(122,3): anon8_LoopHead
+ (0,0): anon8_LoopBody
+ Termination.dfy(122,3): anon9_Else
+ (0,0): anon10_Then
(0,0): anon5
- Termination.dfy(122,3): anon12_Else
+ Termination.dfy(122,3): anon11_Else
Termination.dfy(251,35): Error: cannot prove termination; try supplying a decreases clause
Execution trace:
+ (0,0): anon0
(0,0): anon6_Else
(0,0): anon7_Else
(0,0): anon8_Then
Termination.dfy(291,3): Error: decreases expression might not decrease
Execution trace:
- Termination.dfy(291,3): anon10_LoopHead
- (0,0): anon10_LoopBody
+ Termination.dfy(291,3): anon9_LoopHead
+ (0,0): anon9_LoopBody
+ Termination.dfy(291,3): anon10_Else
Termination.dfy(291,3): anon11_Else
- Termination.dfy(291,3): anon12_Else
- (0,0): anon13_Else
+ (0,0): anon12_Else
Dafny program verifier finished with 59 verified, 7 errors
@@ -1088,14 +1105,14 @@ TypeParameters.dfy(175,15): Error BP5005: This loop invariant might not be maint TypeParameters.dfy(175,38): Related location
Execution trace:
(0,0): anon0
- TypeParameters.dfy(168,3): anon17_LoopHead
- (0,0): anon17_LoopBody
- TypeParameters.dfy(168,3): anon18_Else
- (0,0): anon20_Then
- TypeParameters.dfy(174,3): anon21_LoopHead
- (0,0): anon21_LoopBody
- TypeParameters.dfy(174,3): anon22_Else
- TypeParameters.dfy(174,3): anon24_Else
+ TypeParameters.dfy(168,3): anon16_LoopHead
+ (0,0): anon16_LoopBody
+ TypeParameters.dfy(168,3): anon17_Else
+ (0,0): anon19_Then
+ TypeParameters.dfy(174,3): anon20_LoopHead
+ (0,0): anon20_LoopBody
+ TypeParameters.dfy(174,3): anon21_Else
+ TypeParameters.dfy(174,3): anon23_Else
Dafny program verifier finished with 50 verified, 8 errors
@@ -1147,22 +1164,28 @@ Coinductive.dfy(92,21): Error: a recursive copredicate call can only be done in -------------------- Corecursion.dfy --------------------
Corecursion.dfy(15,13): Error: cannot prove termination; try supplying a decreases clause (note that only functions without side effects can be called co-recursively)
Execution trace:
+ (0,0): anon0
(0,0): anon3_Else
Corecursion.dfy(21,13): Error: cannot prove termination; try supplying a decreases clause (note that only functions without any ensures clause can be called co-recursively)
Execution trace:
+ (0,0): anon0
(0,0): anon3_Else
Corecursion.dfy(56,5): Error: cannot prove termination; try supplying a decreases clause
Execution trace:
+ (0,0): anon0
(0,0): anon3_Else
Corecursion.dfy(69,16): Error: cannot prove termination; try supplying a decreases clause (note that calls cannot be co-recursive in this context)
Execution trace:
+ (0,0): anon0
(0,0): anon5_Else
Corecursion.dfy(91,15): Error: cannot prove termination; try supplying a decreases clause (note that a call can be co-recursive only if all intra-cluster calls are in non-destructive contexts)
Execution trace:
+ (0,0): anon0
(0,0): anon5_Else
(0,0): anon6_Then
Corecursion.dfy(101,15): Error: cannot prove termination; try supplying a decreases clause (note that a call can be co-recursive only if all intra-cluster calls are in non-destructive contexts)
Execution trace:
+ (0,0): anon0
(0,0): anon5_Else
(0,0): anon6_Then
@@ -1342,17 +1365,17 @@ Execution trace: LoopModifies.dfy(17,8): Error: assignment may update an array element not in the enclosing context's modifies clause
Execution trace:
(0,0): anon0
- LoopModifies.dfy(14,4): anon9_LoopHead
- (0,0): anon9_LoopBody
- LoopModifies.dfy(14,4): anon10_Else
- LoopModifies.dfy(14,4): anon12_Else
+ LoopModifies.dfy(14,4): anon8_LoopHead
+ (0,0): anon8_LoopBody
+ LoopModifies.dfy(14,4): anon9_Else
+ LoopModifies.dfy(14,4): anon11_Else
LoopModifies.dfy(46,8): Error: assignment may update an array element not in the enclosing context's modifies clause
Execution trace:
(0,0): anon0
- LoopModifies.dfy(42,4): anon9_LoopHead
- (0,0): anon9_LoopBody
- LoopModifies.dfy(42,4): anon10_Else
- LoopModifies.dfy(42,4): anon12_Else
+ LoopModifies.dfy(42,4): anon8_LoopHead
+ (0,0): anon8_LoopBody
+ LoopModifies.dfy(42,4): anon9_Else
+ LoopModifies.dfy(42,4): anon11_Else
LoopModifies.dfy(61,8): Error: assignment may update an array element not in the enclosing context's modifies clause
Execution trace:
(0,0): anon0
@@ -1366,10 +1389,10 @@ Execution trace: LoopModifies.dfy(98,8): Error: assignment may update an array element not in the enclosing context's modifies clause
Execution trace:
(0,0): anon0
- LoopModifies.dfy(90,4): anon9_LoopHead
- (0,0): anon9_LoopBody
- LoopModifies.dfy(90,4): anon10_Else
- LoopModifies.dfy(90,4): anon12_Else
+ LoopModifies.dfy(90,4): anon8_LoopHead
+ (0,0): anon8_LoopBody
+ LoopModifies.dfy(90,4): anon9_Else
+ LoopModifies.dfy(90,4): anon11_Else
LoopModifies.dfy(146,11): Error: assignment may update an array element not in the enclosing context's modifies clause
Execution trace:
(0,0): anon0
@@ -1384,21 +1407,21 @@ Execution trace: LoopModifies.dfy(197,10): Error: assignment may update an array element not in the enclosing context's modifies clause
Execution trace:
(0,0): anon0
- LoopModifies.dfy(193,4): anon9_LoopHead
- (0,0): anon9_LoopBody
- LoopModifies.dfy(193,4): anon10_Else
- LoopModifies.dfy(193,4): anon12_Else
+ LoopModifies.dfy(193,4): anon8_LoopHead
+ (0,0): anon8_LoopBody
+ LoopModifies.dfy(193,4): anon9_Else
+ LoopModifies.dfy(193,4): anon11_Else
LoopModifies.dfy(285,13): Error: assignment may update an array element not in the enclosing context's modifies clause
Execution trace:
(0,0): anon0
- LoopModifies.dfy(273,4): anon17_LoopHead
- (0,0): anon17_LoopBody
- LoopModifies.dfy(273,4): anon18_Else
- LoopModifies.dfy(273,4): anon20_Else
- LoopModifies.dfy(281,7): anon21_LoopHead
- (0,0): anon21_LoopBody
- LoopModifies.dfy(281,7): anon22_Else
- LoopModifies.dfy(281,7): anon24_Else
+ LoopModifies.dfy(273,4): anon16_LoopHead
+ (0,0): anon16_LoopBody
+ LoopModifies.dfy(273,4): anon17_Else
+ LoopModifies.dfy(273,4): anon19_Else
+ LoopModifies.dfy(281,7): anon20_LoopHead
+ (0,0): anon20_LoopBody
+ LoopModifies.dfy(281,7): anon21_Else
+ LoopModifies.dfy(281,7): anon23_Else
Dafny program verifier finished with 23 verified, 9 errors
@@ -1420,6 +1443,7 @@ Execution trace: Refinement.dfy(90,12): Error BP5003: A postcondition might not hold on this return path.
Refinement.dfy(69,15): Related location: This is the postcondition that might not hold.
Execution trace:
+ (0,0): anon0
(0,0): anon3_Else
Refinement.dfy(93,3): Error BP5003: A postcondition might not hold on this return path.
Refinement.dfy(74,15): Related location: This is the postcondition that might not hold.
@@ -1504,9 +1528,11 @@ Dafny program verifier finished with 54 verified, 4 errors -------------------- PredExpr.dfy --------------------
PredExpr.dfy(4,12): Error: condition in assert expression might not hold
Execution trace:
+ (0,0): anon0
(0,0): anon3_Else
PredExpr.dfy(36,15): Error: value assigned to a nat must be non-negative
Execution trace:
+ (0,0): anon0
(0,0): anon5_Else
(0,0): anon6_Else
PredExpr.dfy(49,17): Error: condition in assert expression might not hold
@@ -1556,12 +1582,12 @@ Skeletons.dfy(42,3): Error BP5003: A postcondition might not hold on this return Skeletons.dfy(41,15): Related location: This is the postcondition that might not hold.
Execution trace:
(0,0): anon0
- Skeletons.dfy[C0](29,5): anon12_LoopHead
- (0,0): anon12_LoopBody
- Skeletons.dfy[C0](29,5): anon13_Else
- (0,0): anon14_Then
- Skeletons.dfy[C0](34,19): anon16_Else
- (0,0): anon11
+ Skeletons.dfy[C0](29,5): anon11_LoopHead
+ (0,0): anon11_LoopBody
+ Skeletons.dfy[C0](29,5): anon12_Else
+ (0,0): anon13_Then
+ Skeletons.dfy[C0](34,19): anon15_Else
+ (0,0): anon10
Dafny program verifier finished with 9 verified, 1 error
@@ -1727,28 +1753,28 @@ Execution trace: Iterators.dfy(205,7): Error: an assignment to _new is only allowed to shrink the set
Execution trace:
(0,0): anon0
- Iterators.dfy(194,3): anon17_LoopHead
- (0,0): anon17_LoopBody
- Iterators.dfy(194,3): anon18_Else
- Iterators.dfy(194,3): anon20_Else
- (0,0): anon21_Then
+ Iterators.dfy(194,3): anon16_LoopHead
+ (0,0): anon16_LoopBody
+ Iterators.dfy(194,3): anon17_Else
+ Iterators.dfy(194,3): anon19_Else
+ (0,0): anon20_Then
Iterators.dfy(209,21): Error: assertion violation
Execution trace:
(0,0): anon0
- Iterators.dfy(194,3): anon17_LoopHead
- (0,0): anon17_LoopBody
- Iterators.dfy(194,3): anon18_Else
- Iterators.dfy(194,3): anon20_Else
- (0,0): anon22_Then
+ Iterators.dfy(194,3): anon16_LoopHead
+ (0,0): anon16_LoopBody
+ Iterators.dfy(194,3): anon17_Else
+ Iterators.dfy(194,3): anon19_Else
+ (0,0): anon21_Then
Iterators.dfy(37,14): Error BP5002: A precondition for this call might not hold.
Iterators.dfy(1,10): Related location: This is the precondition that might not hold.
Execution trace:
(0,0): anon0
- (0,0): anon37_Then
+ (0,0): anon35_Then
(0,0): anon2
- (0,0): anon38_Then
+ (0,0): anon36_Then
(0,0): anon5
- (0,0): anon39_Then
+ (0,0): anon37_Then
Iterators.dfy(86,14): Error: assertion violation
Execution trace:
(0,0): anon0
@@ -1769,11 +1795,11 @@ Execution trace: Iterators.dfy(231,14): Error: assertion violation
Execution trace:
(0,0): anon0
- Iterators.dfy(222,3): anon15_LoopHead
- (0,0): anon15_LoopBody
- Iterators.dfy(222,3): anon16_Else
- Iterators.dfy(222,3): anon19_Else
- (0,0): anon20_Else
+ Iterators.dfy(222,3): anon14_LoopHead
+ (0,0): anon14_LoopBody
+ Iterators.dfy(222,3): anon15_Else
+ Iterators.dfy(222,3): anon18_Else
+ (0,0): anon19_Else
Dafny program verifier finished with 38 verified, 11 errors
@@ -1784,18 +1810,22 @@ Dafny program verifier finished with 11 verified, 0 errors -------------------- RankNeg.dfy --------------------
RankNeg.dfy(7,26): Error: cannot prove termination; try supplying a decreases clause
Execution trace:
+ (0,0): anon0
(0,0): anon5_Else
(0,0): anon6_Then
RankNeg.dfy(12,28): Error: cannot prove termination; try supplying a decreases clause
Execution trace:
+ (0,0): anon0
(0,0): anon5_Else
(0,0): anon6_Then
RankNeg.dfy(19,31): Error: cannot prove termination; try supplying a decreases clause
Execution trace:
+ (0,0): anon0
(0,0): anon5_Else
(0,0): anon6_Then
RankNeg.dfy(29,25): Error: cannot prove termination; try supplying a decreases clause
Execution trace:
+ (0,0): anon0
(0,0): anon5_Else
(0,0): anon6_Then
@@ -1808,6 +1838,7 @@ Dafny program verifier finished with 46 verified, 0 errors -------------------- ComputationsNeg.dfy --------------------
ComputationsNeg.dfy(4,3): Error: failure to decrease termination measure
Execution trace:
+ (0,0): anon0
(0,0): anon3_Else
ComputationsNeg.dfy(8,1): Error BP5003: A postcondition might not hold on this return path.
ComputationsNeg.dfy(7,17): Related location: This is the postcondition that might not hold.
@@ -1836,6 +1867,7 @@ Verifying CheckWellformed$$_0_M0.C.Q ... Superposition.dfy(24,15): Error BP5003: A postcondition might not hold on this return path.
Superposition.dfy(25,26): Related location: This is the postcondition that might not hold.
Execution trace:
+ (0,0): anon0
(0,0): anon5_Else
Verifying CheckWellformed$$_0_M0.C.R ...
@@ -1843,6 +1875,7 @@ Verifying CheckWellformed$$_0_M0.C.R ... Superposition.dfy(30,15): Error BP5003: A postcondition might not hold on this return path.
Superposition.dfy(31,26): Related location: This is the postcondition that might not hold.
Execution trace:
+ (0,0): anon0
(0,0): anon5_Else
Verifying CheckWellformed$$_1_M1.C.M ...
@@ -1856,6 +1889,7 @@ Verifying CheckWellformed$$_1_M1.C.P ... Superposition.dfy(47,15): Error BP5003: A postcondition might not hold on this return path.
Superposition.dfy[M1](19,26): Related location: This is the postcondition that might not hold.
Execution trace:
+ (0,0): anon0
(0,0): anon7_Else
(0,0): anon9_Then
(0,0): anon6
@@ -1874,14 +1908,17 @@ Execution trace: (0,0): anon0
SmallTests.dfy(61,36): Error: possible division by zero
Execution trace:
+ (0,0): anon0
(0,0): anon12_Then
SmallTests.dfy(62,51): Error: possible division by zero
Execution trace:
+ (0,0): anon0
(0,0): anon12_Else
(0,0): anon3
(0,0): anon13_Else
SmallTests.dfy(63,22): Error: target object may be null
Execution trace:
+ (0,0): anon0
(0,0): anon12_Then
(0,0): anon3
(0,0): anon13_Then
@@ -1889,9 +1926,9 @@ Execution trace: SmallTests.dfy(82,24): Error: target object may be null
Execution trace:
(0,0): anon0
- SmallTests.dfy(81,5): anon9_LoopHead
- (0,0): anon9_LoopBody
- (0,0): anon10_Then
+ SmallTests.dfy(81,5): anon8_LoopHead
+ (0,0): anon8_LoopBody
+ (0,0): anon9_Then
SmallTests.dfy(116,5): Error: call may violate context's modifies clause
Execution trace:
(0,0): anon0
@@ -1945,6 +1982,7 @@ Execution trace: (0,0): anon0
SmallTests.dfy(375,6): Error: cannot prove termination; try supplying a decreases clause
Execution trace:
+ (0,0): anon0
(0,0): anon3_Else
SmallTests.dfy(669,14): Error: assertion violation
Execution trace:
@@ -1979,10 +2017,12 @@ Execution trace: (0,0): anon0
SmallTests.dfy(343,4): Error: cannot prove termination; try supplying a decreases clause
Execution trace:
+ (0,0): anon0
(0,0): anon3_Else
SmallTests.dfy(387,10): Error BP5003: A postcondition might not hold on this return path.
SmallTests.dfy(390,41): Related location: This is the postcondition that might not hold.
Execution trace:
+ (0,0): anon0
(0,0): anon6_Else
SmallTests.dfy(540,12): Error: assertion violation
Execution trace:
@@ -2054,14 +2094,17 @@ Execution trace: (0,0): anon0
out.tmp.dfy(69,37): Error: possible division by zero
Execution trace:
+ (0,0): anon0
(0,0): anon12_Then
out.tmp.dfy(70,52): Error: possible division by zero
Execution trace:
+ (0,0): anon0
(0,0): anon12_Else
(0,0): anon3
(0,0): anon13_Else
out.tmp.dfy(71,22): Error: target object may be null
Execution trace:
+ (0,0): anon0
(0,0): anon12_Then
(0,0): anon3
(0,0): anon13_Then
@@ -2069,9 +2112,9 @@ Execution trace: out.tmp.dfy(88,24): Error: target object may be null
Execution trace:
(0,0): anon0
- out.tmp.dfy(87,5): anon9_LoopHead
- (0,0): anon9_LoopBody
- (0,0): anon10_Then
+ out.tmp.dfy(87,5): anon8_LoopHead
+ (0,0): anon8_LoopBody
+ (0,0): anon9_Then
out.tmp.dfy(122,5): Error: call may violate context's modifies clause
Execution trace:
(0,0): anon0
@@ -2125,6 +2168,7 @@ Execution trace: (0,0): anon0
out.tmp.dfy(285,6): Error: cannot prove termination; try supplying a decreases clause
Execution trace:
+ (0,0): anon0
(0,0): anon3_Else
out.tmp.dfy(388,14): Error: assertion violation
Execution trace:
@@ -2159,10 +2203,12 @@ Execution trace: (0,0): anon0
out.tmp.dfy(490,4): Error: cannot prove termination; try supplying a decreases clause
Execution trace:
+ (0,0): anon0
(0,0): anon3_Else
out.tmp.dfy(498,10): Error BP5003: A postcondition might not hold on this return path.
out.tmp.dfy(499,41): Related location: This is the postcondition that might not hold.
Execution trace:
+ (0,0): anon0
(0,0): anon6_Else
out.tmp.dfy(536,12): Error: assertion violation
Execution trace:
|