diff options
| author |  Clément Pit--Claudel <clement.pitclaudel@live.com> | 2015-07-23 11:57:19 -0700 |
|---|---|---|
| committer | Clément Pit--Claudel <clement.pitclaudel@live.com> | 2015-07-23 11:57:19 -0700 |
| commit | 3f886d1789d50400ffba2befdc2ae0e8d5c79cbe (patch) | |
| tree | 70b54a2e8b21c82dbd06ed46c716a281dc8efa26 | |
| parent | 1763ad8e4d6b631fe966b394ae2dbafa7d803627 (diff) | |
Fix: Unify column numbers in Dafny's errors
Dafny counts from 0, but Boogie counts from 1. Tokens are 1-based. Thus when we
print tokens, we need to decrement the column number. This was done for resolver
errors, but not for verification or parsing errors. In addition, parsing errors
were inconsistent with resolution errors case-wise.
Unfortunately, the fix affects the output of many tests.
95 files changed, 714 insertions, 682 deletions
diff --git a/Source/Dafny/Parser.cs b/Source/Dafny/Parser.cs index 01438f68..d50a4dd6 100644 --- a/Source/Dafny/Parser.cs +++ b/Source/Dafny/Parser.cs @@ -4429,8 +4429,8 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo public class Errors {
public int count = 0; // number of errors detected
public System.IO.TextWriter/*!*/ errorStream = Console.Out; // error messages go to this stream
- public string errMsgFormat = "{0}({1},{2}): error: {3}"; // 0=filename, 1=line, 2=column, 3=text
- public string warningMsgFormat = "{0}({1},{2}): warning: {3}"; // 0=filename, 1=line, 2=column, 3=text
+ public string errMsgFormat = "{0}({1},{2}): Error: {3}"; // 0=filename, 1=line, 2=column, 3=text
+ public string warningMsgFormat = "{0}({1},{2}): Warning: {3}"; // 0=filename, 1=line, 2=column, 3=text
public void SynErr(string filename, int line, int col, int n) {
SynErr(filename, line, col, GetSyntaxErrorString(n));
@@ -4438,7 +4438,7 @@ public class Errors { public virtual void SynErr(string filename, int line, int col, string/*!*/ msg) {
Contract.Requires(msg != null);
- errorStream.WriteLine(errMsgFormat, filename, line, col, msg);
+ errorStream.WriteLine(errMsgFormat, filename, line, col - 1, msg);
count++;
}
@@ -4701,7 +4701,7 @@ public class Errors { public virtual void SemErr(string filename, int line, int col, string/*!*/ msg) {
Contract.Requires(msg != null);
- errorStream.WriteLine(errMsgFormat, filename, line, col, msg);
+ errorStream.WriteLine(errMsgFormat, filename, line, col - 1, msg);
count++;
}
@@ -4713,7 +4713,7 @@ public class Errors { public virtual void Warning(string filename, int line, int col, string msg) {
Contract.Requires(msg != null);
- errorStream.WriteLine(warningMsgFormat, filename, line, col, msg);
+ errorStream.WriteLine(warningMsgFormat, filename, line, col - 1, msg);
}
} // Errors
@@ -4721,6 +4721,4 @@ public class Errors { public class FatalError: Exception {
public FatalError(string m): base(m) {}
}
-
-
}
\ No newline at end of file diff --git a/Source/DafnyDriver/DafnyDriver.cs b/Source/DafnyDriver/DafnyDriver.cs index 9fdc9320..d22899ab 100644 --- a/Source/DafnyDriver/DafnyDriver.cs +++ b/Source/DafnyDriver/DafnyDriver.cs @@ -273,7 +273,13 @@ namespace Microsoft.Dafny {
public override void ReportBplError(IToken tok, string message, bool error, TextWriter tw, string category = null)
{
- base.ReportBplError(tok, message, error, tw, category);
+ // Dafny has 0-indexed columns, but Boogie counts from 1
+ var realigned_tok = new Token(tok.line, tok.col - 1);
+ realigned_tok.kind = tok.kind;
+ realigned_tok.pos = tok.pos;
+ realigned_tok.val = tok.val;
+ realigned_tok.filename = tok.filename;
+ base.ReportBplError(realigned_tok, message, error, tw, category);
if (tok is Dafny.NestedToken)
{
diff --git a/Test/dafny0/AdvancedLHS.dfy.expect b/Test/dafny0/AdvancedLHS.dfy.expect index cb817605..aab12cfc 100644 --- a/Test/dafny0/AdvancedLHS.dfy.expect +++ b/Test/dafny0/AdvancedLHS.dfy.expect @@ -1,4 +1,4 @@ -AdvancedLHS.dfy(34,23): Error: target object may be null
+AdvancedLHS.dfy(34,22): Error: target object may be null
Execution trace:
(0,0): anon0
(0,0): anon15_Else
diff --git a/Test/dafny0/Array.dfy.expect b/Test/dafny0/Array.dfy.expect index 59dcb4bf..40fb318d 100644 --- a/Test/dafny0/Array.dfy.expect +++ b/Test/dafny0/Array.dfy.expect @@ -1,16 +1,16 @@ -Array.dfy(13,8): Error: assignment may update an array element not in the enclosing context's modifies clause
+Array.dfy(13,7): Error: assignment may update an array element not in the enclosing context's modifies clause
Execution trace:
(0,0): anon0
(0,0): anon5_Then
(0,0): anon2
(0,0): anon6_Then
-Array.dfy(20,16): Error: target object may be null
+Array.dfy(20,15): Error: target object may be null
Execution trace:
(0,0): anon0
-Array.dfy(27,6): Error: index out of range
+Array.dfy(27,5): Error: index out of range
Execution trace:
(0,0): anon0
-Array.dfy(51,20): Error: assertion violation
+Array.dfy(51,19): Error: assertion violation
Execution trace:
(0,0): anon0
(0,0): anon12_Then
@@ -21,19 +21,19 @@ Execution trace: (0,0): anon16_Then
(0,0): anon9
(0,0): anon11
-Array.dfy(59,8): Error: assignment may update an array element not in the enclosing context's modifies clause
+Array.dfy(59,7): Error: assignment may update an array element not in the enclosing context's modifies clause
Execution trace:
(0,0): anon0
(0,0): anon5_Then
(0,0): anon2
(0,0): anon6_Then
-Array.dfy(66,8): Error: assignment may update an array element not in the enclosing context's modifies clause
+Array.dfy(66,7): Error: assignment may update an array element not in the enclosing context's modifies clause
Execution trace:
(0,0): anon0
(0,0): anon5_Then
(0,0): anon2
(0,0): anon6_Then
-Array.dfy(110,21): Error: upper bound below lower bound or above length of array
+Array.dfy(110,20): Error: upper bound below lower bound or above length of array
Execution trace:
(0,0): anon0
(0,0): anon14_Else
@@ -41,7 +41,7 @@ Execution trace: (0,0): anon19_Then
(0,0): anon20_Then
(0,0): anon11
-Array.dfy(120,8): Error: insufficient reads clause to read the indicated range of array elements
+Array.dfy(120,7): Error: insufficient reads clause to read the indicated range of array elements
Execution trace:
(0,0): anon0
(0,0): anon10_Else
@@ -49,7 +49,7 @@ Execution trace: (0,0): anon12_Then
(0,0): anon13_Then
(0,0): anon9
-Array.dfy(122,8): Error: insufficient reads clause to read the indicated range of array elements
+Array.dfy(122,7): Error: insufficient reads clause to read the indicated range of array elements
Execution trace:
(0,0): anon0
(0,0): anon10_Else
@@ -57,7 +57,7 @@ Execution trace: (0,0): anon12_Then
(0,0): anon13_Else
(0,0): anon9
-Array.dfy(123,8): Error: insufficient reads clause to read the indicated range of array elements
+Array.dfy(123,7): Error: insufficient reads clause to read the indicated range of array elements
Execution trace:
(0,0): anon0
(0,0): anon10_Else
@@ -65,7 +65,7 @@ Execution trace: (0,0): anon12_Then
(0,0): anon13_Else
(0,0): anon9
-Array.dfy(124,8): Error: insufficient reads clause to read the indicated range of array elements
+Array.dfy(124,7): Error: insufficient reads clause to read the indicated range of array elements
Execution trace:
(0,0): anon0
(0,0): anon10_Else
@@ -73,45 +73,45 @@ Execution trace: (0,0): anon12_Then
(0,0): anon13_Else
(0,0): anon9
-Array.dfy(163,6): Error: insufficient reads clause to read array element
+Array.dfy(163,5): Error: insufficient reads clause to read array element
Execution trace:
(0,0): anon0
(0,0): anon8_Else
(0,0): anon9_Then
(0,0): anon10_Then
(0,0): anon7
-Array.dfy(171,6): Error: insufficient reads clause to read array element
+Array.dfy(171,5): Error: insufficient reads clause to read array element
Execution trace:
(0,0): anon0
(0,0): anon8_Else
(0,0): anon9_Then
(0,0): anon10_Then
(0,0): anon7
-Array.dfy(187,6): Error: assignment may update an array element not in the enclosing context's modifies clause
+Array.dfy(187,5): Error: assignment may update an array element not in the enclosing context's modifies clause
Execution trace:
(0,0): anon0
-Array.dfy(194,6): Error: assignment may update an array element not in the enclosing context's modifies clause
+Array.dfy(194,5): Error: assignment may update an array element not in the enclosing context's modifies clause
Execution trace:
(0,0): anon0
-Array.dfy(219,1): Error BP5003: A postcondition might not hold on this return path.
-Array.dfy(218,11): Related location: This is the postcondition that might not hold.
+Array.dfy(219,0): Error BP5003: A postcondition might not hold on this return path.
+Array.dfy(218,10): Related location: This is the postcondition that might not hold.
Execution trace:
(0,0): anon0
-Array.dfy(243,1): Error BP5003: A postcondition might not hold on this return path.
-Array.dfy(242,11): Related location: This is the postcondition that might not hold.
+Array.dfy(243,0): Error BP5003: A postcondition might not hold on this return path.
+Array.dfy(242,10): Related location: This is the postcondition that might not hold.
Execution trace:
(0,0): anon0
-Array.dfy(249,1): Error BP5003: A postcondition might not hold on this return path.
-Array.dfy(248,11): Related location: This is the postcondition that might not hold.
+Array.dfy(249,0): Error BP5003: A postcondition might not hold on this return path.
+Array.dfy(248,10): Related location: This is the postcondition that might not hold.
Execution trace:
(0,0): anon0
-Array.dfy(264,10): Error: value assigned to a nat must be non-negative
+Array.dfy(264,9): Error: value assigned to a nat must be non-negative
Execution trace:
(0,0): anon0
(0,0): anon5_Then
(0,0): anon2
(0,0): anon6_Then
-Array.dfy(265,5): Error: value assigned to a nat must be non-negative
+Array.dfy(265,4): Error: value assigned to a nat must be non-negative
Execution trace:
(0,0): anon0
(0,0): anon5_Then
diff --git a/Test/dafny0/AutoReq.dfy.expect b/Test/dafny0/AutoReq.dfy.expect index 8486716d..b4b34e14 100644 --- a/Test/dafny0/AutoReq.dfy.expect +++ b/Test/dafny0/AutoReq.dfy.expect @@ -1,43 +1,43 @@ -AutoReq.dfy(247,5): Error: possible violation of function precondition
-AutoReq.dfy(239,14): Related location
+AutoReq.dfy(247,4): Error: possible violation of function precondition
+AutoReq.dfy(239,13): Related location
Execution trace:
(0,0): anon0
(0,0): anon4_Else
-AutoReq.dfy(13,3): Error: possible violation of function precondition
-AutoReq.dfy(5,14): Related location
+AutoReq.dfy(13,2): Error: possible violation of function precondition
+AutoReq.dfy(5,13): Related location
Execution trace:
(0,0): anon0
(0,0): anon4_Else
-AutoReq.dfy(25,3): Error: possible violation of function precondition
-AutoReq.dfy(5,14): Related location
+AutoReq.dfy(25,2): Error: possible violation of function precondition
+AutoReq.dfy(5,13): Related location
Execution trace:
(0,0): anon0
(0,0): anon4_Else
-AutoReq.dfy(38,12): Error: assertion violation
-AutoReq.dfy(31,13): Related location
-AutoReq.dfy(7,5): Related location
+AutoReq.dfy(38,11): Error: assertion violation
+AutoReq.dfy(31,12): Related location
+AutoReq.dfy(7,4): Related location
Execution trace:
(0,0): anon0
(0,0): anon9_Then
-AutoReq.dfy(38,12): Error: possible violation of function precondition
-AutoReq.dfy(5,14): Related location
+AutoReq.dfy(38,11): Error: possible violation of function precondition
+AutoReq.dfy(5,13): Related location
Execution trace:
(0,0): anon0
(0,0): anon9_Then
-AutoReq.dfy(40,12): Error: assertion violation
-AutoReq.dfy(31,27): Related location
-AutoReq.dfy(7,5): Related location
+AutoReq.dfy(40,11): Error: assertion violation
+AutoReq.dfy(31,26): Related location
+AutoReq.dfy(7,4): Related location
Execution trace:
(0,0): anon0
(0,0): anon10_Then
-AutoReq.dfy(40,12): Error: possible violation of function precondition
-AutoReq.dfy(5,14): Related location
+AutoReq.dfy(40,11): Error: possible violation of function precondition
+AutoReq.dfy(5,13): Related location
Execution trace:
(0,0): anon0
(0,0): anon10_Then
-AutoReq.dfy(45,12): Error: assertion violation
-AutoReq.dfy(31,13): Related location
-AutoReq.dfy(7,5): Related location
+AutoReq.dfy(45,11): Error: assertion violation
+AutoReq.dfy(31,12): Related location
+AutoReq.dfy(7,4): Related location
Execution trace:
(0,0): anon0
(0,0): anon11_Then
diff --git a/Test/dafny0/Backticks.dfy.expect b/Test/dafny0/Backticks.dfy.expect index 57761ab4..58977413 100644 --- a/Test/dafny0/Backticks.dfy.expect +++ b/Test/dafny0/Backticks.dfy.expect @@ -1,10 +1,10 @@ -Backticks.dfy(38,5): Error: insufficient reads clause to invoke function
+Backticks.dfy(38,4): Error: insufficient reads clause to invoke function
Execution trace:
(0,0): anon0
(0,0): anon7_Else
(0,0): anon8_Else
(0,0): anon6
-Backticks.dfy(77,8): Error: call may violate context's modifies clause
+Backticks.dfy(77,7): Error: call may violate context's modifies clause
Execution trace:
(0,0): anon0
(0,0): anon3_Then
diff --git a/Test/dafny0/BadFunction.dfy.expect b/Test/dafny0/BadFunction.dfy.expect index 9c4ae81d..1af2608d 100644 --- a/Test/dafny0/BadFunction.dfy.expect +++ b/Test/dafny0/BadFunction.dfy.expect @@ -1,4 +1,4 @@ -BadFunction.dfy(9,3): Error: failure to decrease termination measure
+BadFunction.dfy(9,2): Error: failure to decrease termination measure
Execution trace:
(0,0): anon0
(0,0): anon4_Else
diff --git a/Test/dafny0/Basics.dfy.expect b/Test/dafny0/Basics.dfy.expect index f28df20a..65d5d101 100644 --- a/Test/dafny0/Basics.dfy.expect +++ b/Test/dafny0/Basics.dfy.expect @@ -1,8 +1,8 @@ -Basics.dfy(45,14): Error: assertion violation
+Basics.dfy(45,13): Error: assertion violation
Execution trace:
(0,0): anon0
(0,0): anon3_Else
-Basics.dfy(69,42): Error: assertion violation
+Basics.dfy(69,41): Error: assertion violation
Execution trace:
(0,0): anon0
(0,0): anon13_Then
@@ -12,7 +12,7 @@ Execution trace: Basics.dfy(69,82): anon17_Else
Basics.dfy(69,95): anon18_Else
(0,0): anon12
-Basics.dfy(93,14): Error: assertion violation
+Basics.dfy(93,13): Error: assertion violation
Execution trace:
(0,0): anon0
Basics.dfy(83,14): anon27_Else
@@ -27,7 +27,7 @@ Execution trace: Basics.dfy(91,13): anon34_Else
(0,0): anon35_Then
(0,0): anon15
-Basics.dfy(99,14): Error: assertion violation
+Basics.dfy(99,13): Error: assertion violation
Execution trace:
(0,0): anon0
Basics.dfy(83,14): anon27_Else
@@ -42,7 +42,7 @@ Execution trace: Basics.dfy(97,19): anon40_Else
(0,0): anon41_Then
(0,0): anon26
-Basics.dfy(112,28): Error: target object may be null
+Basics.dfy(112,27): Error: target object may be null
Execution trace:
(0,0): anon0
Basics.dfy(105,20): anon13_Else
@@ -52,7 +52,7 @@ Execution trace: Basics.dfy(107,24): anon15_Else
(0,0): anon6
(0,0): anon16_Then
-Basics.dfy(114,14): Error: target object may be null
+Basics.dfy(114,13): Error: target object may be null
Execution trace:
(0,0): anon0
Basics.dfy(105,20): anon13_Else
@@ -62,11 +62,11 @@ Execution trace: Basics.dfy(107,24): anon15_Else
(0,0): anon6
(0,0): anon16_Else
-Basics.dfy(149,16): Error: assertion violation
+Basics.dfy(149,15): Error: assertion violation
Execution trace:
(0,0): anon0
(0,0): anon10_Then
-Basics.dfy(168,10): Error: when left-hand sides 0 and 1 may refer to the same location, they must be assigned the same value
+Basics.dfy(168,9): Error: when left-hand sides 0 and 1 may refer to the same location, they must be assigned the same value
Execution trace:
(0,0): anon0
(0,0): anon10_Then
@@ -75,28 +75,28 @@ Execution trace: (0,0): anon6
(0,0): anon12_Then
(0,0): anon9
-Basics.dfy(182,10): Error: when left-hand sides 0 and 1 refer to the same location, they must be assigned the same value
+Basics.dfy(182,9): Error: when left-hand sides 0 and 1 refer to the same location, they must be assigned the same value
Execution trace:
(0,0): anon0
-Basics.dfy(194,19): Error: assertion violation
+Basics.dfy(194,18): Error: assertion violation
Execution trace:
(0,0): anon0
(0,0): anon11_Then
-Basics.dfy(196,10): Error: assignment may update an object not in the enclosing context's modifies clause
+Basics.dfy(196,9): Error: assignment may update an object not in the enclosing context's modifies clause
Execution trace:
(0,0): anon0
(0,0): anon3
-Basics.dfy(196,10): Error: target object may be null
+Basics.dfy(196,9): Error: target object may be null
Execution trace:
(0,0): anon0
(0,0): anon3
-Basics.dfy(201,12): Error: left-hand sides 0 and 1 may refer to the same location
+Basics.dfy(201,11): Error: left-hand sides 0 and 1 may refer to the same location
Execution trace:
(0,0): anon0
(0,0): anon11_Then
(0,0): anon3
(0,0): anon12_Then
-Basics.dfy(212,15): Error: assertion violation
+Basics.dfy(212,14): Error: assertion violation
Execution trace:
(0,0): anon0
(0,0): anon11_Then
@@ -106,19 +106,19 @@ Execution trace: (0,0): anon13_Then
(0,0): anon8
(0,0): anon14_Then
-Basics.dfy(274,10): Error: when left-hand sides 0 and 1 refer to the same location, they must be assigned the same value
+Basics.dfy(274,9): Error: when left-hand sides 0 and 1 refer to the same location, they must be assigned the same value
Execution trace:
(0,0): anon0
-Basics.dfy(465,12): Error: assertion violation
+Basics.dfy(465,11): Error: assertion violation
Execution trace:
(0,0): anon0
(0,0): anon4_Then
(0,0): anon3
-Basics.dfy(476,19): Error: assertion violation
+Basics.dfy(476,18): Error: assertion violation
Execution trace:
(0,0): anon0
(0,0): anon4_Else
-Basics.dfy(478,12): Error: assertion violation
+Basics.dfy(478,11): Error: assertion violation
Execution trace:
(0,0): anon0
(0,0): anon4_Then
diff --git a/Test/dafny0/Calculations.dfy.expect b/Test/dafny0/Calculations.dfy.expect index 3427a5cb..d4559f53 100644 --- a/Test/dafny0/Calculations.dfy.expect +++ b/Test/dafny0/Calculations.dfy.expect @@ -1,24 +1,24 @@ -Calculations.dfy(7,6): Error: index out of range
+Calculations.dfy(7,5): Error: index out of range
Execution trace:
(0,0): anon0
(0,0): anon24_Then
-Calculations.dfy(12,15): Error: index out of range
+Calculations.dfy(12,14): Error: index out of range
Execution trace:
(0,0): anon0
(0,0): anon26_Then
-Calculations.dfy(12,19): Error: assertion violation
+Calculations.dfy(12,18): Error: assertion violation
Execution trace:
(0,0): anon0
(0,0): anon26_Then
-Calculations.dfy(56,12): Error: assertion violation
+Calculations.dfy(56,11): Error: assertion violation
Execution trace:
(0,0): anon0
Calculations.dfy(51,3): anon5_Else
-Calculations.dfy(79,15): Error: index out of range
+Calculations.dfy(79,14): Error: index out of range
Execution trace:
(0,0): anon0
(0,0): anon12_Then
-Calculations.dfy(79,19): Error: assertion violation
+Calculations.dfy(79,18): Error: assertion violation
Execution trace:
(0,0): anon0
(0,0): anon12_Then
diff --git a/Test/dafny0/Char.dfy.expect b/Test/dafny0/Char.dfy.expect index 55418934..874aaa65 100644 --- a/Test/dafny0/Char.dfy.expect +++ b/Test/dafny0/Char.dfy.expect @@ -1,14 +1,14 @@ -Char.dfy(48,21): Error: assertion violation
+Char.dfy(48,20): Error: assertion violation
Execution trace:
(0,0): anon0
(0,0): anon9_Then
(0,0): anon10_Then
-Char.dfy(52,21): Error: assertion violation
+Char.dfy(52,20): Error: assertion violation
Execution trace:
(0,0): anon0
(0,0): anon9_Then
(0,0): anon11_Else
-Char.dfy(63,17): Error: assertion violation
+Char.dfy(63,16): Error: assertion violation
Execution trace:
(0,0): anon0
(0,0): anon5_Else
diff --git a/Test/dafny0/CoPrefix.dfy.expect b/Test/dafny0/CoPrefix.dfy.expect index c92a09c1..a7295367 100644 --- a/Test/dafny0/CoPrefix.dfy.expect +++ b/Test/dafny0/CoPrefix.dfy.expect @@ -1,48 +1,48 @@ -CoPrefix.dfy(164,3): Error BP5003: A postcondition might not hold on this return path.
-CoPrefix.dfy(163,15): Related location: This is the postcondition that might not hold.
+CoPrefix.dfy(164,2): Error BP5003: A postcondition might not hold on this return path.
+CoPrefix.dfy(163,14): Related location: This is the postcondition that might not hold.
Execution trace:
(0,0): anon0
(0,0): anon3_Else
-CoPrefix.dfy(169,3): Error BP5003: A postcondition might not hold on this return path.
-CoPrefix.dfy(168,15): Related location: This is the postcondition that might not hold.
+CoPrefix.dfy(169,2): Error BP5003: A postcondition might not hold on this return path.
+CoPrefix.dfy(168,14): Related location: This is the postcondition that might not hold.
Execution trace:
(0,0): anon0
(0,0): anon3_Else
-CoPrefix.dfy(176,11): Error: cannot prove termination; try supplying a decreases clause
+CoPrefix.dfy(176,10): Error: cannot prove termination; try supplying a decreases clause
Execution trace:
(0,0): anon0
(0,0): anon3_Then
-CoPrefix.dfy(63,57): Error: failure to decrease termination measure
+CoPrefix.dfy(63,56): Error: failure to decrease termination measure
Execution trace:
(0,0): anon0
(0,0): anon7_Then
(0,0): anon8_Else
(0,0): anon9_Then
-CoPrefix.dfy(76,56): Error: cannot prove termination; try supplying a decreases clause
+CoPrefix.dfy(76,55): Error: cannot prove termination; try supplying a decreases clause
Execution trace:
(0,0): anon0
(0,0): anon7_Then
(0,0): anon8_Else
(0,0): anon9_Then
-CoPrefix.dfy(114,1): Error BP5003: A postcondition might not hold on this return path.
-CoPrefix.dfy(113,11): Related location: This is the postcondition that might not hold.
-CoPrefix.dfy(101,17): Related location
+CoPrefix.dfy(114,0): Error BP5003: A postcondition might not hold on this return path.
+CoPrefix.dfy(113,10): Related location: This is the postcondition that might not hold.
+CoPrefix.dfy(101,16): Related location
Execution trace:
(0,0): anon0
(0,0): anon3_Then
-CoPrefix.dfy(138,25): Error: assertion violation
+CoPrefix.dfy(138,24): Error: assertion violation
Execution trace:
(0,0): anon0
(0,0): anon9_Then
(0,0): anon10_Then
-CoPrefix.dfy(142,25): Error: assertion violation
-CoPrefix.dfy(117,23): Related location
+CoPrefix.dfy(142,24): Error: assertion violation
+CoPrefix.dfy(117,22): Related location
Execution trace:
(0,0): anon0
(0,0): anon9_Then
(0,0): anon12_Then
-CoPrefix.dfy(151,1): Error BP5003: A postcondition might not hold on this return path.
-CoPrefix.dfy(150,11): Related location: This is the postcondition that might not hold.
+CoPrefix.dfy(151,0): Error BP5003: A postcondition might not hold on this return path.
+CoPrefix.dfy(150,10): Related location: This is the postcondition that might not hold.
Execution trace:
(0,0): anon0
(0,0): anon3_Else
diff --git a/Test/dafny0/CoinductiveProofs.dfy.expect b/Test/dafny0/CoinductiveProofs.dfy.expect index 12ce2f01..2a5a2b0b 100644 --- a/Test/dafny0/CoinductiveProofs.dfy.expect +++ b/Test/dafny0/CoinductiveProofs.dfy.expect @@ -1,48 +1,48 @@ -CoinductiveProofs.dfy(29,12): Error: assertion violation
-CoinductiveProofs.dfy(13,17): Related location
+CoinductiveProofs.dfy(29,11): Error: assertion violation
+CoinductiveProofs.dfy(13,16): Related location
Execution trace:
(0,0): anon0
(0,0): anon5_Then
(0,0): anon6_Then
-CoinductiveProofs.dfy(59,1): Error BP5003: A postcondition might not hold on this return path.
-CoinductiveProofs.dfy(58,11): Related location: This is the postcondition that might not hold.
-CoinductiveProofs.dfy(54,3): Related location
+CoinductiveProofs.dfy(59,0): Error BP5003: A postcondition might not hold on this return path.
+CoinductiveProofs.dfy(58,10): Related location: This is the postcondition that might not hold.
+CoinductiveProofs.dfy(54,2): Related location
Execution trace:
(0,0): anon0
(0,0): anon3_Then
-CoinductiveProofs.dfy(74,12): Error: assertion violation
-CoinductiveProofs.dfy(54,3): Related location
+CoinductiveProofs.dfy(74,11): Error: assertion violation
+CoinductiveProofs.dfy(54,2): Related location
Execution trace:
(0,0): anon0
(0,0): anon5_Then
(0,0): anon6_Then
-CoinductiveProofs.dfy(91,1): Error BP5003: A postcondition might not hold on this return path.
-CoinductiveProofs.dfy(90,11): Related location: This is the postcondition that might not hold.
-CoinductiveProofs.dfy(80,3): Related location
+CoinductiveProofs.dfy(91,0): Error BP5003: A postcondition might not hold on this return path.
+CoinductiveProofs.dfy(90,10): Related location: This is the postcondition that might not hold.
+CoinductiveProofs.dfy(80,2): Related location
Execution trace:
(0,0): anon0
(0,0): anon3_Then
-CoinductiveProofs.dfy(100,12): Error: assertion violation
-CoinductiveProofs.dfy(80,3): Related location
+CoinductiveProofs.dfy(100,11): Error: assertion violation
+CoinductiveProofs.dfy(80,2): Related location
Execution trace:
(0,0): anon0
(0,0): anon5_Then
(0,0): anon6_Then
-CoinductiveProofs.dfy(111,1): Error BP5003: A postcondition might not hold on this return path.
-CoinductiveProofs.dfy(110,11): Related location: This is the postcondition that might not hold.
-CoinductiveProofs.dfy(106,3): Related location
+CoinductiveProofs.dfy(111,0): Error BP5003: A postcondition might not hold on this return path.
+CoinductiveProofs.dfy(110,10): Related location: This is the postcondition that might not hold.
+CoinductiveProofs.dfy(106,2): Related location
Execution trace:
(0,0): anon0
(0,0): anon3_Then
-CoinductiveProofs.dfy(150,1): Error BP5003: A postcondition might not hold on this return path.
-CoinductiveProofs.dfy(149,22): Related location: This is the postcondition that might not hold.
-CoinductiveProofs.dfy(4,24): Related location
+CoinductiveProofs.dfy(150,0): Error BP5003: A postcondition might not hold on this return path.
+CoinductiveProofs.dfy(149,21): Related location: This is the postcondition that might not hold.
+CoinductiveProofs.dfy(4,23): Related location
Execution trace:
(0,0): anon0
(0,0): anon3_Then
-CoinductiveProofs.dfy(156,1): Error BP5003: A postcondition might not hold on this return path.
-CoinductiveProofs.dfy(155,22): Related location: This is the postcondition that might not hold.
-CoinductiveProofs.dfy(4,24): Related location
+CoinductiveProofs.dfy(156,0): Error BP5003: A postcondition might not hold on this return path.
+CoinductiveProofs.dfy(155,21): Related location: This is the postcondition that might not hold.
+CoinductiveProofs.dfy(4,23): Related location
Execution trace:
(0,0): anon0
(0,0): anon3_Then
diff --git a/Test/dafny0/Comprehensions.dfy.expect b/Test/dafny0/Comprehensions.dfy.expect index 88873fd8..887a3249 100644 --- a/Test/dafny0/Comprehensions.dfy.expect +++ b/Test/dafny0/Comprehensions.dfy.expect @@ -1,4 +1,4 @@ -Comprehensions.dfy(12,14): Error: assertion violation
+Comprehensions.dfy(12,13): Error: assertion violation
Execution trace:
(0,0): anon0
(0,0): anon9_Then
diff --git a/Test/dafny0/ComputationsLoop.dfy.expect b/Test/dafny0/ComputationsLoop.dfy.expect index 91dc2af9..84674030 100644 --- a/Test/dafny0/ComputationsLoop.dfy.expect +++ b/Test/dafny0/ComputationsLoop.dfy.expect @@ -1,8 +1,8 @@ -ComputationsLoop.dfy(7,3): Error: failure to decrease termination measure
+ComputationsLoop.dfy(7,2): Error: failure to decrease termination measure
Execution trace:
(0,0): anon0
(0,0): anon4_Else
-ComputationsLoop.dfy(12,26): Error: assertion violation
+ComputationsLoop.dfy(12,25): Error: assertion violation
Execution trace:
(0,0): anon0
diff --git a/Test/dafny0/ComputationsLoop2.dfy.expect b/Test/dafny0/ComputationsLoop2.dfy.expect index 816cbd31..48fc618f 100644 --- a/Test/dafny0/ComputationsLoop2.dfy.expect +++ b/Test/dafny0/ComputationsLoop2.dfy.expect @@ -1,12 +1,12 @@ -ComputationsLoop2.dfy(6,3): Error: cannot prove termination; try supplying a decreases clause
+ComputationsLoop2.dfy(6,2): Error: cannot prove termination; try supplying a decreases clause
Execution trace:
(0,0): anon0
(0,0): anon4_Else
-ComputationsLoop2.dfy(11,3): Error: cannot prove termination; try supplying a decreases clause
+ComputationsLoop2.dfy(11,2): Error: cannot prove termination; try supplying a decreases clause
Execution trace:
(0,0): anon0
(0,0): anon4_Else
-ComputationsLoop2.dfy(16,26): Error: assertion violation
+ComputationsLoop2.dfy(16,25): Error: assertion violation
Execution trace:
(0,0): anon0
diff --git a/Test/dafny0/ComputationsNeg.dfy.expect b/Test/dafny0/ComputationsNeg.dfy.expect index a6318087..598e9fa5 100644 --- a/Test/dafny0/ComputationsNeg.dfy.expect +++ b/Test/dafny0/ComputationsNeg.dfy.expect @@ -1,19 +1,19 @@ -ComputationsNeg.dfy(7,3): Error: failure to decrease termination measure
+ComputationsNeg.dfy(7,2): Error: failure to decrease termination measure
Execution trace:
(0,0): anon0
(0,0): anon4_Else
-ComputationsNeg.dfy(11,1): Error BP5003: A postcondition might not hold on this return path.
-ComputationsNeg.dfy(10,17): Related location: This is the postcondition that might not hold.
+ComputationsNeg.dfy(11,0): Error BP5003: A postcondition might not hold on this return path.
+ComputationsNeg.dfy(10,16): Related location: This is the postcondition that might not hold.
Execution trace:
(0,0): anon0
-ComputationsNeg.dfy(23,1): Error BP5003: A postcondition might not hold on this return path.
-ComputationsNeg.dfy(22,11): Related location: This is the postcondition that might not hold.
+ComputationsNeg.dfy(23,0): Error BP5003: A postcondition might not hold on this return path.
+ComputationsNeg.dfy(22,10): Related location: This is the postcondition that might not hold.
Execution trace:
(0,0): anon0
-ComputationsNeg.dfy(36,13): Error: assertion violation
+ComputationsNeg.dfy(36,12): Error: assertion violation
Execution trace:
(0,0): anon0
-ComputationsNeg.dfy(45,13): Error: assertion violation
+ComputationsNeg.dfy(45,12): Error: assertion violation
Execution trace:
(0,0): anon0
diff --git a/Test/dafny0/ControlStructures.dfy.expect b/Test/dafny0/ControlStructures.dfy.expect index 3f4dce92..5638bcbc 100644 --- a/Test/dafny0/ControlStructures.dfy.expect +++ b/Test/dafny0/ControlStructures.dfy.expect @@ -1,29 +1,29 @@ -ControlStructures.dfy(8,3): Error: missing case in case statement: Purple
+ControlStructures.dfy(8,2): Error: missing case in case statement: Purple
Execution trace:
(0,0): anon0
(0,0): anon6_Else
(0,0): anon7_Else
(0,0): anon8_Then
-ControlStructures.dfy(8,3): Error: missing case in case statement: Blue
+ControlStructures.dfy(8,2): Error: missing case in case statement: Blue
Execution trace:
(0,0): anon0
(0,0): anon6_Else
(0,0): anon7_Else
(0,0): anon8_Else
(0,0): anon9_Then
-ControlStructures.dfy(17,3): Error: missing case in case statement: Purple
+ControlStructures.dfy(17,2): Error: missing case in case statement: Purple
Execution trace:
(0,0): anon0
(0,0): anon6_Else
(0,0): anon7_Else
(0,0): anon8_Then
-ControlStructures.dfy(46,5): Error: missing case in case statement: Red
+ControlStructures.dfy(46,4): Error: missing case in case statement: Red
Execution trace:
(0,0): anon0
(0,0): anon8_Then
(0,0): anon9_Else
(0,0): anon10_Then
-ControlStructures.dfy(54,3): Error: missing case in case statement: Red
+ControlStructures.dfy(54,2): Error: missing case in case statement: Red
Execution trace:
(0,0): anon0
(0,0): anon9_Else
@@ -31,11 +31,11 @@ Execution trace: (0,0): anon11_Else
(0,0): anon12_Else
(0,0): anon13_Then
-ControlStructures.dfy(75,3): Error: alternative cases fail to cover all possibilties
+ControlStructures.dfy(75,2): Error: alternative cases fail to cover all possibilties
Execution trace:
(0,0): anon0
(0,0): anon5_Else
-ControlStructures.dfy(218,18): Error: assertion violation
+ControlStructures.dfy(218,17): Error: assertion violation
Execution trace:
(0,0): anon0
ControlStructures.dfy(197,3): anon59_LoopHead
@@ -51,7 +51,7 @@ Execution trace: (0,0): anon69_LoopBody
ControlStructures.dfy(213,9): anon70_Else
(0,0): anon71_Then
-ControlStructures.dfy(235,21): Error: assertion violation
+ControlStructures.dfy(235,20): Error: assertion violation
Execution trace:
(0,0): anon0
ControlStructures.dfy(197,3): anon59_LoopHead
@@ -77,7 +77,7 @@ Execution trace: (0,0): anon38
(0,0): anon83_Then
(0,0): anon52
-ControlStructures.dfy(238,30): Error: assertion violation
+ControlStructures.dfy(238,29): Error: assertion violation
Execution trace:
(0,0): anon0
ControlStructures.dfy(197,3): anon59_LoopHead
@@ -92,7 +92,7 @@ Execution trace: (0,0): anon84_Then
(0,0): anon85_Then
(0,0): anon56
-ControlStructures.dfy(241,17): Error: assertion violation
+ControlStructures.dfy(241,16): Error: assertion violation
Execution trace:
(0,0): anon0
ControlStructures.dfy(197,3): anon59_LoopHead
diff --git a/Test/dafny0/Corecursion.dfy.expect b/Test/dafny0/Corecursion.dfy.expect index 619a9c84..a6b3fdce 100644 --- a/Test/dafny0/Corecursion.dfy.expect +++ b/Test/dafny0/Corecursion.dfy.expect @@ -1,34 +1,34 @@ -Corecursion.dfy(17,13): Error: cannot prove termination; try supplying a decreases clause (note that only functions without side effects can be called co-recursively)
+Corecursion.dfy(17,12): 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): anon4_Else
-Corecursion.dfy(23,13): Error: cannot prove termination; try supplying a decreases clause (note that only functions without any ensures clause can be called co-recursively)
+Corecursion.dfy(23,12): 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): anon4_Else
-Corecursion.dfy(58,5): Error: cannot prove termination; try supplying a decreases clause
+Corecursion.dfy(58,4): Error: cannot prove termination; try supplying a decreases clause
Execution trace:
(0,0): anon0
(0,0): anon4_Else
-Corecursion.dfy(71,16): Error: cannot prove termination; try supplying a decreases clause (note that calls cannot be co-recursive in this context)
+Corecursion.dfy(71,15): 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): anon7_Else
-Corecursion.dfy(93,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)
+Corecursion.dfy(93,14): 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): anon7_Else
(0,0): anon8_Then
-Corecursion.dfy(103,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)
+Corecursion.dfy(103,14): 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): anon7_Else
(0,0): anon8_Then
-Corecursion.dfy(148,13): Error: failure to decrease termination measure (note that a call can be co-recursive only if all intra-cluster calls are in non-destructive contexts)
+Corecursion.dfy(148,12): Error: failure to decrease termination measure (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): anon4_Else
-Corecursion.dfy(161,13): Error: failure to decrease termination measure (note that a call can be co-recursive only if all intra-cluster calls are in non-destructive contexts)
+Corecursion.dfy(161,12): Error: failure to decrease termination measure (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): anon4_Else
diff --git a/Test/dafny0/DTypes.dfy.expect b/Test/dafny0/DTypes.dfy.expect index 9b4288e9..76088e9b 100644 --- a/Test/dafny0/DTypes.dfy.expect +++ b/Test/dafny0/DTypes.dfy.expect @@ -1,27 +1,27 @@ -DTypes.dfy(182,3): Error BP5003: A postcondition might not hold on this return path.
-DTypes.dfy(181,15): Related location: This is the postcondition that might not hold.
+DTypes.dfy(182,2): Error BP5003: A postcondition might not hold on this return path.
+DTypes.dfy(181,14): Related location: This is the postcondition that might not hold.
Execution trace:
(0,0): anon0
-DTypes.dfy(18,14): Error: assertion violation
+DTypes.dfy(18,13): Error: assertion violation
Execution trace:
(0,0): anon0
-DTypes.dfy(56,18): Error: assertion violation
+DTypes.dfy(56,17): Error: assertion violation
Execution trace:
(0,0): anon0
-DTypes.dfy(121,13): Error: assertion violation
-DTypes.dfy(93,30): Related location
+DTypes.dfy(121,12): Error: assertion violation
+DTypes.dfy(93,29): Related location
Execution trace:
(0,0): anon0
-DTypes.dfy(127,13): Error: assertion violation
-DTypes.dfy(93,20): Related location
+DTypes.dfy(127,12): Error: assertion violation
+DTypes.dfy(93,19): Related location
Execution trace:
(0,0): anon0
-DTypes.dfy(137,12): Error: assertion violation
-DTypes.dfy(132,6): Related location
-DTypes.dfy(93,20): Related location
+DTypes.dfy(137,11): Error: assertion violation
+DTypes.dfy(132,5): Related location
+DTypes.dfy(93,19): Related location
Execution trace:
(0,0): anon0
-DTypes.dfy(158,12): Error: assertion violation
+DTypes.dfy(158,11): Error: assertion violation
Execution trace:
(0,0): anon0
(0,0): anon5_Then
diff --git a/Test/dafny0/Datatypes.dfy.expect b/Test/dafny0/Datatypes.dfy.expect index 4c0b1e96..7147ca60 100644 --- a/Test/dafny0/Datatypes.dfy.expect +++ b/Test/dafny0/Datatypes.dfy.expect @@ -1,43 +1,43 @@ -Datatypes.dfy(297,10): Error BP5003: A postcondition might not hold on this return path.
-Datatypes.dfy(295,15): Related location: This is the postcondition that might not hold.
+Datatypes.dfy(297,9): Error BP5003: A postcondition might not hold on this return path.
+Datatypes.dfy(295,14): Related location: This is the postcondition that might not hold.
Execution trace:
(0,0): anon0
(0,0): anon13_Then
(0,0): anon14_Else
(0,0): anon15_Then
(0,0): anon6
-Datatypes.dfy(298,12): Error: missing case in case statement: Appendix
+Datatypes.dfy(298,11): Error: missing case in case statement: Appendix
Execution trace:
(0,0): anon0
(0,0): anon13_Then
(0,0): anon14_Else
(0,0): anon15_Else
(0,0): anon16_Then
-Datatypes.dfy(349,5): Error: missing case in case statement: Cons
+Datatypes.dfy(349,4): Error: missing case in case statement: Cons
Execution trace:
(0,0): anon0
(0,0): anon7_Else
(0,0): anon8_Then
-Datatypes.dfy(349,5): Error: missing case in case statement: Nil
+Datatypes.dfy(349,4): Error: missing case in case statement: Nil
Execution trace:
(0,0): anon0
(0,0): anon7_Else
(0,0): anon8_Else
(0,0): anon9_Then
-Datatypes.dfy(356,8): Error: missing case in case statement: Cons
+Datatypes.dfy(356,7): Error: missing case in case statement: Cons
Execution trace:
(0,0): anon0
(0,0): anon10_Else
(0,0): anon11_Then
(0,0): anon12_Then
-Datatypes.dfy(356,8): Error: missing case in case statement: Nil
+Datatypes.dfy(356,7): Error: missing case in case statement: Nil
Execution trace:
(0,0): anon0
(0,0): anon10_Else
(0,0): anon11_Then
(0,0): anon12_Else
(0,0): anon13_Then
-Datatypes.dfy(82,20): Error: assertion violation
+Datatypes.dfy(82,19): Error: assertion violation
Execution trace:
(0,0): anon0
(0,0): anon20_Else
@@ -47,23 +47,23 @@ Execution trace: (0,0): anon23_Then
(0,0): anon24_Else
(0,0): anon25_Then
-Datatypes.dfy(170,16): Error: assertion violation
+Datatypes.dfy(170,15): Error: assertion violation
Execution trace:
(0,0): anon0
(0,0): anon4_Then
-Datatypes.dfy(172,16): Error: assertion violation
+Datatypes.dfy(172,15): Error: assertion violation
Execution trace:
(0,0): anon0
(0,0): anon4_Else
(0,0): anon5_Then
-Datatypes.dfy(201,13): Error: destructor 'Car' can only be applied to datatype values constructed by 'XCons'
+Datatypes.dfy(201,12): Error: destructor 'Car' can only be applied to datatype values constructed by 'XCons'
Execution trace:
(0,0): anon0
-Datatypes.dfy(204,17): Error: destructor 'Car' can only be applied to datatype values constructed by 'XCons'
+Datatypes.dfy(204,16): Error: destructor 'Car' can only be applied to datatype values constructed by 'XCons'
Execution trace:
(0,0): anon0
(0,0): anon6_Then
-Datatypes.dfy(225,17): Error: destructor 'c' can only be applied to datatype values constructed by 'T''
+Datatypes.dfy(225,16): Error: destructor 'c' can only be applied to datatype values constructed by 'T''
Execution trace:
(0,0): anon0
(0,0): anon5_Then
diff --git a/Test/dafny0/Definedness.dfy.expect b/Test/dafny0/Definedness.dfy.expect index af5b62b9..b5b015ad 100644 --- a/Test/dafny0/Definedness.dfy.expect +++ b/Test/dafny0/Definedness.dfy.expect @@ -1,87 +1,87 @@ -Definedness.dfy(11,7): Error: possible division by zero
+Definedness.dfy(11,6): Error: possible division by zero
Execution trace:
(0,0): anon0
(0,0): anon4_Else
-Definedness.dfy(18,16): Error: possible division by zero
+Definedness.dfy(18,15): Error: possible division by zero
Execution trace:
(0,0): anon0
-Definedness.dfy(27,16): Error: target object may be null
+Definedness.dfy(27,15): Error: target object may be null
Execution trace:
(0,0): anon0
-Definedness.dfy(28,21): Error: target object may be null
+Definedness.dfy(28,20): Error: target object may be null
Execution trace:
(0,0): anon0
(0,0): anon3_Then
-Definedness.dfy(29,17): Error: possible division by zero
+Definedness.dfy(29,16): Error: possible division by zero
Execution trace:
(0,0): anon0
-Definedness.dfy(36,16): Error: target object may be null
+Definedness.dfy(36,15): Error: target object may be null
Execution trace:
(0,0): anon0
-Definedness.dfy(45,16): Error: target object may be null
+Definedness.dfy(45,15): Error: target object may be null
Execution trace:
(0,0): anon0
-Definedness.dfy(53,18): Error: target object may be null
+Definedness.dfy(53,17): Error: target object may be null
Execution trace:
(0,0): anon0
-Definedness.dfy(54,3): Error BP5003: A postcondition might not hold on this return path.
-Definedness.dfy(53,22): Related location: This is the postcondition that might not hold.
+Definedness.dfy(54,2): Error BP5003: A postcondition might not hold on this return path.
+Definedness.dfy(53,21): Related location: This is the postcondition that might not hold.
Execution trace:
(0,0): anon0
-Definedness.dfy(60,18): Error: target object may be null
+Definedness.dfy(60,17): Error: target object may be null
Execution trace:
(0,0): anon0
-Definedness.dfy(61,3): Error BP5003: A postcondition might not hold on this return path.
-Definedness.dfy(60,22): Related location: This is the postcondition that might not hold.
+Definedness.dfy(61,2): Error BP5003: A postcondition might not hold on this return path.
+Definedness.dfy(60,21): Related location: This is the postcondition that might not hold.
Execution trace:
(0,0): anon0
-Definedness.dfy(68,3): Error BP5003: A postcondition might not hold on this return path.
-Definedness.dfy(67,22): Related location: This is the postcondition that might not hold.
+Definedness.dfy(68,2): Error BP5003: A postcondition might not hold on this return path.
+Definedness.dfy(67,21): Related location: This is the postcondition that might not hold.
Execution trace:
(0,0): anon0
-Definedness.dfy(88,7): Error: target object may be null
+Definedness.dfy(88,6): Error: target object may be null
Execution trace:
(0,0): anon0
-Definedness.dfy(89,5): Error: possible violation of function precondition
-Definedness.dfy(79,16): Related location
+Definedness.dfy(89,4): Error: possible violation of function precondition
+Definedness.dfy(79,15): Related location
Execution trace:
(0,0): anon0
-Definedness.dfy(89,10): Error: assignment may update an object not in the enclosing context's modifies clause
+Definedness.dfy(89,9): Error: assignment may update an object not in the enclosing context's modifies clause
Execution trace:
(0,0): anon0
-Definedness.dfy(89,10): Error: target object may be null
+Definedness.dfy(89,9): Error: target object may be null
Execution trace:
(0,0): anon0
-Definedness.dfy(90,10): Error: possible violation of function precondition
-Definedness.dfy(79,16): Related location
+Definedness.dfy(90,9): Error: possible violation of function precondition
+Definedness.dfy(79,15): Related location
Execution trace:
(0,0): anon0
-Definedness.dfy(95,14): Error: possible division by zero
+Definedness.dfy(95,13): Error: possible division by zero
Execution trace:
(0,0): anon0
-Definedness.dfy(95,23): Error: possible division by zero
+Definedness.dfy(95,22): Error: possible division by zero
Execution trace:
(0,0): anon0
-Definedness.dfy(96,15): Error: possible division by zero
+Definedness.dfy(96,14): Error: possible division by zero
Execution trace:
(0,0): anon0
-Definedness.dfy(101,12): Error: possible division by zero
+Definedness.dfy(101,11): Error: possible division by zero
Execution trace:
(0,0): anon0
-Definedness.dfy(108,15): Error: possible division by zero
+Definedness.dfy(108,14): Error: possible division by zero
Execution trace:
Definedness.dfy(108,5): anon7_LoopHead
(0,0): anon7_LoopBody
Definedness.dfy(108,5): anon8_Else
-Definedness.dfy(117,23): Error: possible violation of function precondition
-Definedness.dfy(79,16): Related location
+Definedness.dfy(117,22): Error: possible violation of function precondition
+Definedness.dfy(79,15): Related location
Execution trace:
(0,0): anon0
Definedness.dfy(116,5): anon12_LoopHead
(0,0): anon12_LoopBody
(0,0): anon13_Then
-Definedness.dfy(123,17): Error: possible violation of function precondition
-Definedness.dfy(79,16): Related location
+Definedness.dfy(123,16): Error: possible violation of function precondition
+Definedness.dfy(79,15): Related location
Execution trace:
(0,0): anon0
Definedness.dfy(116,5): anon12_LoopHead
@@ -91,30 +91,30 @@ Execution trace: Definedness.dfy(122,5): anon15_LoopHead
(0,0): anon15_LoopBody
(0,0): anon16_Then
-Definedness.dfy(133,17): Error: possible violation of function precondition
-Definedness.dfy(79,16): Related location
+Definedness.dfy(133,16): Error: possible violation of function precondition
+Definedness.dfy(79,15): Related location
Execution trace:
(0,0): anon0
Definedness.dfy(132,5): anon6_LoopHead
(0,0): anon6_LoopBody
(0,0): anon7_Then
-Definedness.dfy(133,22): Error BP5004: This loop invariant might not hold on entry.
+Definedness.dfy(133,21): Error BP5004: This loop invariant might not hold on entry.
Execution trace:
(0,0): anon0
-Definedness.dfy(134,17): Error: possible violation of function precondition
-Definedness.dfy(79,16): Related location
+Definedness.dfy(134,16): Error: possible violation of function precondition
+Definedness.dfy(79,15): Related location
Execution trace:
(0,0): anon0
Definedness.dfy(132,5): anon6_LoopHead
(0,0): anon6_LoopBody
(0,0): anon7_Then
-Definedness.dfy(143,15): Error: possible division by zero
+Definedness.dfy(143,14): Error: possible division by zero
Execution trace:
(0,0): anon0
Definedness.dfy(143,5): anon8_LoopHead
(0,0): anon8_LoopBody
Definedness.dfy(143,5): anon9_Else
-Definedness.dfy(162,15): Error: possible division by zero
+Definedness.dfy(162,14): Error: possible division by zero
Execution trace:
(0,0): anon0
Definedness.dfy(156,5): anon16_LoopHead
@@ -126,11 +126,11 @@ Execution trace: Definedness.dfy(162,5): anon20_LoopHead
(0,0): anon20_LoopBody
Definedness.dfy(162,5): anon21_Else
-Definedness.dfy(175,28): Error BP5004: This loop invariant might not hold on entry.
+Definedness.dfy(175,27): Error BP5004: This loop invariant might not hold on entry.
Execution trace:
(0,0): anon0
-Definedness.dfy(181,17): Error: possible violation of function precondition
-Definedness.dfy(79,16): Related location
+Definedness.dfy(181,16): Error: possible violation of function precondition
+Definedness.dfy(79,15): Related location
Execution trace:
(0,0): anon0
Definedness.dfy(173,5): anon18_LoopHead
@@ -142,32 +142,32 @@ Execution trace: (0,0): anon22_Then
(0,0): anon23_Then
(0,0): anon11
-Definedness.dfy(196,19): Error: possible division by zero
+Definedness.dfy(196,18): Error: possible division by zero
Execution trace:
(0,0): anon0
Definedness.dfy(194,5): anon6_LoopHead
(0,0): anon6_LoopBody
(0,0): anon7_Then
-Definedness.dfy(196,23): Error BP5004: This loop invariant might not hold on entry.
+Definedness.dfy(196,22): Error BP5004: This loop invariant might not hold on entry.
Execution trace:
(0,0): anon0
-Definedness.dfy(196,28): Error: possible division by zero
+Definedness.dfy(196,27): Error: possible division by zero
Execution trace:
(0,0): anon0
Definedness.dfy(194,5): anon6_LoopHead
(0,0): anon6_LoopBody
(0,0): anon7_Then
-Definedness.dfy(215,10): Error BP5003: A postcondition might not hold on this return path.
-Definedness.dfy(217,46): Related location: This is the postcondition that might not hold.
+Definedness.dfy(215,9): Error BP5003: A postcondition might not hold on this return path.
+Definedness.dfy(217,45): Related location: This is the postcondition that might not hold.
Execution trace:
(0,0): anon0
(0,0): anon4_Else
-Definedness.dfy(224,22): Error: target object may be null
+Definedness.dfy(224,21): Error: target object may be null
Execution trace:
(0,0): anon0
(0,0): anon4_Then
-Definedness.dfy(237,10): Error BP5003: A postcondition might not hold on this return path.
-Definedness.dfy(240,24): Related location: This is the postcondition that might not hold.
+Definedness.dfy(237,9): Error BP5003: A postcondition might not hold on this return path.
+Definedness.dfy(240,23): Related location: This is the postcondition that might not hold.
Execution trace:
(0,0): anon0
(0,0): anon4_Else
diff --git a/Test/dafny0/DeterministicPick.dfy.expect b/Test/dafny0/DeterministicPick.dfy.expect index 0999294e..aef97ebd 100644 --- a/Test/dafny0/DeterministicPick.dfy.expect +++ b/Test/dafny0/DeterministicPick.dfy.expect @@ -1,4 +1,4 @@ -DeterministicPick.dfy(13,5): Error: to be compilable, the value of a let-such-that expression must be uniquely determined
+DeterministicPick.dfy(13,4): Error: to be compilable, the value of a let-such-that expression must be uniquely determined
Execution trace:
(0,0): anon0
(0,0): anon4_Else
diff --git a/Test/dafny0/DiamondImports.dfy.expect b/Test/dafny0/DiamondImports.dfy.expect index e9e8c2b9..1acca075 100644 --- a/Test/dafny0/DiamondImports.dfy.expect +++ b/Test/dafny0/DiamondImports.dfy.expect @@ -1,12 +1,12 @@ -DiamondImports.dfy(34,16): Error: assertion violation
+DiamondImports.dfy(34,15): Error: assertion violation
Execution trace:
(0,0): anon0
-DiamondImports.dfy(50,16): Error: assertion violation
+DiamondImports.dfy(50,15): Error: assertion violation
Execution trace:
(0,0): anon0
(0,0): anon3_Then
(0,0): anon2
-DiamondImports.dfy(101,16): Error: assertion violation
+DiamondImports.dfy(101,15): Error: assertion violation
Execution trace:
(0,0): anon0
(0,0): anon7_Then
@@ -14,7 +14,7 @@ Execution trace: (0,0): anon8_Then
(0,0): anon9_Then
(0,0): anon6
-DiamondImports.dfy(120,16): Error: assertion violation
+DiamondImports.dfy(120,15): Error: assertion violation
Execution trace:
(0,0): anon0
(0,0): anon9_Then
@@ -25,7 +25,7 @@ Execution trace: (0,0): anon6
(0,0): anon12_Then
(0,0): anon8
-DiamondImports.dfy(140,26): Error: assertion violation
+DiamondImports.dfy(140,25): Error: assertion violation
Execution trace:
(0,0): anon0
diff --git a/Test/dafny0/Fuel.dfy.expect b/Test/dafny0/Fuel.dfy.expect index 4c180a9c..90fe877d 100644 --- a/Test/dafny0/Fuel.dfy.expect +++ b/Test/dafny0/Fuel.dfy.expect @@ -1,94 +1,94 @@ -Fuel.dfy(17,23): Error: assertion violation
+Fuel.dfy(17,22): Error: assertion violation
Execution trace:
(0,0): anon0
-Fuel.dfy(65,28): Error: assertion violation
+Fuel.dfy(65,27): Error: assertion violation
Execution trace:
(0,0): anon0
(0,0): anon6_Else
-Fuel.dfy(69,28): Error: assertion violation
+Fuel.dfy(69,27): Error: assertion violation
Execution trace:
(0,0): anon0
(0,0): anon6_Then
(0,0): anon7_Then
-Fuel.dfy(92,23): Error: assertion violation
+Fuel.dfy(92,22): Error: assertion violation
Execution trace:
(0,0): anon0
-Fuel.dfy(94,23): Error: assertion violation
+Fuel.dfy(94,22): Error: assertion violation
Execution trace:
(0,0): anon0
-Fuel.dfy(120,23): Error: assertion violation
+Fuel.dfy(120,22): Error: assertion violation
Execution trace:
(0,0): anon0
-Fuel.dfy(122,23): Error: assertion violation
+Fuel.dfy(122,22): Error: assertion violation
Execution trace:
(0,0): anon0
-Fuel.dfy(129,39): Error: assertion violation
+Fuel.dfy(129,38): Error: assertion violation
Execution trace:
(0,0): anon0
-Fuel.dfy(132,27): Error: assertion violation
+Fuel.dfy(132,26): Error: assertion violation
Execution trace:
(0,0): anon0
(0,0): anon3_Then
-Fuel.dfy(133,27): Error: assertion violation
+Fuel.dfy(133,26): Error: assertion violation
Execution trace:
(0,0): anon0
(0,0): anon3_Then
-Fuel.dfy(157,23): Error: assertion violation
+Fuel.dfy(157,22): Error: assertion violation
Execution trace:
(0,0): anon0
(0,0): anon10_Else
(0,0): anon9
-Fuel.dfy(200,56): Error: assertion violation
+Fuel.dfy(200,55): Error: assertion violation
Execution trace:
(0,0): anon0
-Fuel.dfy(245,23): Error: assertion violation
+Fuel.dfy(245,22): Error: assertion violation
Execution trace:
(0,0): anon0
-Fuel.dfy(247,23): Error: assertion violation
+Fuel.dfy(247,22): Error: assertion violation
Execution trace:
(0,0): anon0
-Fuel.dfy(280,27): Error: assertion violation
+Fuel.dfy(280,26): Error: assertion violation
Execution trace:
(0,0): anon0
(0,0): anon7_Then
-Fuel.dfy(335,27): Error: possible violation of function precondition
-Fuel.dfy(324,22): Related location
+Fuel.dfy(335,26): Error: possible violation of function precondition
+Fuel.dfy(324,21): Related location
Execution trace:
(0,0): anon0
(0,0): anon7_Else
(0,0): anon8_Then
-Fuel.dfy(335,50): Error: destructor 't' can only be applied to datatype values constructed by 'VTuple'
+Fuel.dfy(335,49): Error: destructor 't' can only be applied to datatype values constructed by 'VTuple'
Execution trace:
(0,0): anon0
(0,0): anon7_Else
(0,0): anon8_Then
-Fuel.dfy(335,51): Error: index out of range
+Fuel.dfy(335,50): Error: index out of range
Execution trace:
(0,0): anon0
(0,0): anon7_Else
(0,0): anon8_Then
-Fuel.dfy(336,39): Error: index out of range
+Fuel.dfy(336,38): Error: index out of range
Execution trace:
(0,0): anon0
(0,0): anon7_Else
(0,0): anon8_Then
-Fuel.dfy(336,43): Error: destructor 'u' can only be applied to datatype values constructed by 'VUint64'
+Fuel.dfy(336,42): Error: destructor 'u' can only be applied to datatype values constructed by 'VUint64'
Execution trace:
(0,0): anon0
(0,0): anon7_Else
(0,0): anon8_Then
-Fuel.dfy(346,43): Error: destructor 'u' can only be applied to datatype values constructed by 'VUint64'
+Fuel.dfy(346,42): Error: destructor 'u' can only be applied to datatype values constructed by 'VUint64'
Execution trace:
(0,0): anon0
(0,0): anon7_Else
(0,0): anon8_Then
-Fuel.dfy(397,23): Error: assertion violation
+Fuel.dfy(397,22): Error: assertion violation
Execution trace:
(0,0): anon0
-Fuel.dfy(398,23): Error: assertion violation
+Fuel.dfy(398,22): Error: assertion violation
Execution trace:
(0,0): anon0
-Fuel.dfy(407,39): Error: assertion violation
+Fuel.dfy(407,38): Error: assertion violation
Execution trace:
(0,0): anon0
diff --git a/Test/dafny0/FunctionSpecifications.dfy.expect b/Test/dafny0/FunctionSpecifications.dfy.expect index 9f76313a..078afaef 100644 --- a/Test/dafny0/FunctionSpecifications.dfy.expect +++ b/Test/dafny0/FunctionSpecifications.dfy.expect @@ -1,5 +1,5 @@ -FunctionSpecifications.dfy(29,10): Error BP5003: A postcondition might not hold on this return path.
-FunctionSpecifications.dfy(31,13): Related location: This is the postcondition that might not hold.
+FunctionSpecifications.dfy(29,9): Error BP5003: A postcondition might not hold on this return path.
+FunctionSpecifications.dfy(31,12): Related location: This is the postcondition that might not hold.
Execution trace:
(0,0): anon0
(0,0): anon10_Else
@@ -7,64 +7,64 @@ Execution trace: (0,0): anon12_Then
(0,0): anon13_Else
(0,0): anon9
-FunctionSpecifications.dfy(38,10): Error BP5003: A postcondition might not hold on this return path.
-FunctionSpecifications.dfy(40,24): Related location: This is the postcondition that might not hold.
+FunctionSpecifications.dfy(38,9): Error BP5003: A postcondition might not hold on this return path.
+FunctionSpecifications.dfy(40,23): Related location: This is the postcondition that might not hold.
Execution trace:
(0,0): anon0
(0,0): anon15_Else
(0,0): anon18_Else
(0,0): anon19_Then
(0,0): anon14
-FunctionSpecifications.dfy(53,11): Error: cannot prove termination; try supplying a decreases clause
+FunctionSpecifications.dfy(53,10): Error: cannot prove termination; try supplying a decreases clause
Execution trace:
(0,0): anon0
(0,0): anon11_Then
(0,0): anon5
-FunctionSpecifications.dfy(59,10): Error BP5003: A postcondition might not hold on this return path.
-FunctionSpecifications.dfy(60,22): Related location: This is the postcondition that might not hold.
+FunctionSpecifications.dfy(59,9): Error BP5003: A postcondition might not hold on this return path.
+FunctionSpecifications.dfy(60,21): Related location: This is the postcondition that might not hold.
Execution trace:
(0,0): anon0
(0,0): anon7_Else
-FunctionSpecifications.dfy(108,23): Error: assertion violation
+FunctionSpecifications.dfy(108,22): Error: assertion violation
Execution trace:
(0,0): anon0
-FunctionSpecifications.dfy(111,23): Error: assertion violation
+FunctionSpecifications.dfy(111,22): Error: assertion violation
Execution trace:
(0,0): anon0
-FunctionSpecifications.dfy(126,27): Error: assertion violation
+FunctionSpecifications.dfy(126,26): Error: assertion violation
Execution trace:
(0,0): anon0
(0,0): anon3_Then
-FunctionSpecifications.dfy(130,27): Error: assertion violation
+FunctionSpecifications.dfy(130,26): Error: assertion violation
Execution trace:
(0,0): anon0
(0,0): anon3_Else
-FunctionSpecifications.dfy(158,3): Error: cannot prove termination; try supplying a decreases clause
+FunctionSpecifications.dfy(158,2): Error: cannot prove termination; try supplying a decreases clause
Execution trace:
(0,0): anon0
(0,0): anon4_Else
-FunctionSpecifications.dfy(167,11): Error: cannot prove termination; try supplying a decreases clause
+FunctionSpecifications.dfy(167,10): Error: cannot prove termination; try supplying a decreases clause
Execution trace:
(0,0): anon0
(0,0): anon4_Else
-FunctionSpecifications.dfy(135,20): Error BP5003: A postcondition might not hold on this return path.
-FunctionSpecifications.dfy(137,29): Related location: This is the postcondition that might not hold.
+FunctionSpecifications.dfy(135,19): Error BP5003: A postcondition might not hold on this return path.
+FunctionSpecifications.dfy(137,28): Related location: This is the postcondition that might not hold.
Execution trace:
(0,0): anon0
(0,0): anon4_Else
-FunctionSpecifications.dfy(146,3): Error: failure to decrease termination measure
+FunctionSpecifications.dfy(146,2): Error: failure to decrease termination measure
Execution trace:
(0,0): anon0
(0,0): anon4_Else
-FunctionSpecifications.dfy(153,3): Error: failure to decrease termination measure
+FunctionSpecifications.dfy(153,2): Error: failure to decrease termination measure
Execution trace:
(0,0): anon0
(0,0): anon4_Else
-FunctionSpecifications.dfy(174,3): Error: cannot prove termination; try supplying a decreases clause
+FunctionSpecifications.dfy(174,2): Error: cannot prove termination; try supplying a decreases clause
Execution trace:
(0,0): anon0
(0,0): anon4_Else
-FunctionSpecifications.dfy(171,20): Error: cannot prove termination; try supplying a decreases clause
+FunctionSpecifications.dfy(171,19): Error: cannot prove termination; try supplying a decreases clause
Execution trace:
(0,0): anon0
diff --git a/Test/dafny0/IMaps.dfy.expect b/Test/dafny0/IMaps.dfy.expect index c2da9505..28ca8ca3 100644 --- a/Test/dafny0/IMaps.dfy.expect +++ b/Test/dafny0/IMaps.dfy.expect @@ -1,4 +1,4 @@ -IMaps.dfy(52,8): Error: element may not be in domain
+IMaps.dfy(52,7): Error: element may not be in domain
Execution trace:
(0,0): anon0
(0,0): anon5_Then
diff --git a/Test/dafny0/Include.dfy.expect b/Test/dafny0/Include.dfy.expect index 0921cec9..d4543afe 100644 --- a/Test/dafny0/Include.dfy.expect +++ b/Test/dafny0/Include.dfy.expect @@ -1,13 +1,13 @@ -Include.dfy(19,19): Error BP5003: A postcondition might not hold on this return path.
-Includee.dfy(17,20): Related location: This is the postcondition that might not hold.
+Include.dfy(19,18): Error BP5003: A postcondition might not hold on this return path.
+Includee.dfy(17,19): Related location: This is the postcondition that might not hold.
Execution trace:
(0,0): anon0
(0,0): anon4_Else
-Includee.dfy[Concrete](22,16): Error: assertion violation
+Includee.dfy[Concrete](22,15): Error: assertion violation
Execution trace:
(0,0): anon0
-Include.dfy(27,7): Error BP5003: A postcondition might not hold on this return path.
-Includee.dfy[Concrete](20,15): Related location: This is the postcondition that might not hold.
+Include.dfy(27,6): Error BP5003: A postcondition might not hold on this return path.
+Includee.dfy[Concrete](20,14): Related location: This is the postcondition that might not hold.
Execution trace:
(0,0): anon0
(0,0): anon6_Then
diff --git a/Test/dafny0/Includee.dfy.expect b/Test/dafny0/Includee.dfy.expect index e0f0689c..ce61e32a 100644 --- a/Test/dafny0/Includee.dfy.expect +++ b/Test/dafny0/Includee.dfy.expect @@ -1,12 +1,12 @@ -Includee.dfy(21,3): Error BP5003: A postcondition might not hold on this return path.
-Includee.dfy(20,15): Related location: This is the postcondition that might not hold.
+Includee.dfy(21,2): Error BP5003: A postcondition might not hold on this return path.
+Includee.dfy(20,14): Related location: This is the postcondition that might not hold.
Execution trace:
(0,0): anon0
-Includee.dfy(24,18): Error: assertion violation
+Includee.dfy(24,17): Error: assertion violation
Execution trace:
(0,0): anon0
-Includee.dfy(6,1): Error BP5003: A postcondition might not hold on this return path.
-Includee.dfy(5,13): Related location: This is the postcondition that might not hold.
+Includee.dfy(6,0): Error BP5003: A postcondition might not hold on this return path.
+Includee.dfy(5,12): Related location: This is the postcondition that might not hold.
Execution trace:
(0,0): anon0
diff --git a/Test/dafny0/IndexIntoUpdate.dfy.expect b/Test/dafny0/IndexIntoUpdate.dfy.expect index 3423a20b..2db3aa0a 100644 --- a/Test/dafny0/IndexIntoUpdate.dfy.expect +++ b/Test/dafny0/IndexIntoUpdate.dfy.expect @@ -1,4 +1,4 @@ -IndexIntoUpdate.dfy(7,19): Error: assertion violation
+IndexIntoUpdate.dfy(7,18): Error: assertion violation
Execution trace:
(0,0): anon0
(0,0): anon3_Then
diff --git a/Test/dafny0/InductivePredicates.dfy.expect b/Test/dafny0/InductivePredicates.dfy.expect index b09b7903..ccf30643 100644 --- a/Test/dafny0/InductivePredicates.dfy.expect +++ b/Test/dafny0/InductivePredicates.dfy.expect @@ -1,8 +1,8 @@ -InductivePredicates.dfy(64,10): Error: assertion violation
+InductivePredicates.dfy(64,9): Error: assertion violation
Execution trace:
(0,0): anon0
(0,0): anon3_Then
-InductivePredicates.dfy(76,11): Error: assertion violation
+InductivePredicates.dfy(76,10): Error: assertion violation
Execution trace:
(0,0): anon0
diff --git a/Test/dafny0/Inverses.dfy.expect b/Test/dafny0/Inverses.dfy.expect index a04f21dc..29c67e5d 100644 --- a/Test/dafny0/Inverses.dfy.expect +++ b/Test/dafny0/Inverses.dfy.expect @@ -1,10 +1,10 @@ -Inverses.dfy(70,1): Error BP5003: A postcondition might not hold on this return path.
-Inverses.dfy(69,11): Related location: This is the postcondition that might not hold.
+Inverses.dfy(70,0): Error BP5003: A postcondition might not hold on this return path.
+Inverses.dfy(69,10): Related location: This is the postcondition that might not hold.
Execution trace:
(0,0): anon0
(0,0): anon6_Else
-Inverses.dfy(83,1): Error BP5003: A postcondition might not hold on this return path.
-Inverses.dfy(82,11): Related location: This is the postcondition that might not hold.
+Inverses.dfy(83,0): Error BP5003: A postcondition might not hold on this return path.
+Inverses.dfy(82,10): Related location: This is the postcondition that might not hold.
Execution trace:
(0,0): anon0
(0,0): anon9_Else
diff --git a/Test/dafny0/Iterators.dfy.expect b/Test/dafny0/Iterators.dfy.expect index f0c6e400..d9129e3e 100644 --- a/Test/dafny0/Iterators.dfy.expect +++ b/Test/dafny0/Iterators.dfy.expect @@ -1,55 +1,55 @@ -Iterators.dfy(251,10): Error: failure to decrease termination measure
+Iterators.dfy(251,9): Error: failure to decrease termination measure
Execution trace:
(0,0): anon0
(0,0): anon5_Else
(0,0): anon6_Else
-Iterators.dfy(274,10): Error: failure to decrease termination measure
+Iterators.dfy(274,9): Error: failure to decrease termination measure
Execution trace:
(0,0): anon0
(0,0): anon5_Else
(0,0): anon6_Else
-Iterators.dfy(284,32): Error: failure to decrease termination measure
+Iterators.dfy(284,31): Error: failure to decrease termination measure
Execution trace:
(0,0): anon0
-Iterators.dfy(296,10): Error: cannot prove termination; try supplying a decreases clause
+Iterators.dfy(296,9): Error: cannot prove termination; try supplying a decreases clause
Execution trace:
(0,0): anon0
(0,0): anon5_Else
(0,0): anon6_Else
-Iterators.dfy(317,10): Error: cannot prove termination; try supplying a decreases clause
+Iterators.dfy(317,9): Error: cannot prove termination; try supplying a decreases clause
Execution trace:
(0,0): anon0
(0,0): anon5_Else
(0,0): anon6_Else
-Iterators.dfy(326,32): Error: cannot prove termination; try supplying a decreases clause
+Iterators.dfy(326,31): Error: cannot prove termination; try supplying a decreases clause
Execution trace:
(0,0): anon0
-Iterators.dfy(343,10): Error: failure to decrease termination measure
+Iterators.dfy(343,9): Error: failure to decrease termination measure
Execution trace:
(0,0): anon0
(0,0): anon5_Else
(0,0): anon6_Else
-Iterators.dfy(353,32): Error: cannot prove termination; try supplying a decreases clause
+Iterators.dfy(353,31): Error: cannot prove termination; try supplying a decreases clause
Execution trace:
(0,0): anon0
-Iterators.dfy(370,10): Error: failure to decrease termination measure
+Iterators.dfy(370,9): Error: failure to decrease termination measure
Execution trace:
(0,0): anon0
(0,0): anon5_Else
(0,0): anon6_Else
-Iterators.dfy(103,22): Error: assertion violation
+Iterators.dfy(103,21): Error: assertion violation
Execution trace:
(0,0): anon0
-Iterators.dfy(106,14): Error: assertion violation
+Iterators.dfy(106,13): Error: assertion violation
Execution trace:
(0,0): anon0
(0,0): anon4_Then
(0,0): anon3
-Iterators.dfy(177,28): Error: assertion violation
+Iterators.dfy(177,27): Error: assertion violation
Execution trace:
(0,0): anon0
(0,0): anon15_Then
-Iterators.dfy(208,7): Error: an assignment to _new is only allowed to shrink the set
+Iterators.dfy(208,6): Error: an assignment to _new is only allowed to shrink the set
Execution trace:
(0,0): anon0
Iterators.dfy(197,3): anon16_LoopHead
@@ -57,7 +57,7 @@ Execution trace: Iterators.dfy(197,3): anon17_Else
Iterators.dfy(197,3): anon19_Else
(0,0): anon20_Then
-Iterators.dfy(212,21): Error: assertion violation
+Iterators.dfy(212,20): Error: assertion violation
Execution trace:
(0,0): anon0
Iterators.dfy(197,3): anon16_LoopHead
@@ -65,8 +65,8 @@ Execution trace: Iterators.dfy(197,3): anon17_Else
Iterators.dfy(197,3): anon19_Else
(0,0): anon21_Then
-Iterators.dfy(40,22): Error BP5002: A precondition for this call might not hold.
-Iterators.dfy(4,10): Related location: This is the precondition that might not hold.
+Iterators.dfy(40,21): Error BP5002: A precondition for this call might not hold.
+Iterators.dfy(4,9): Related location: This is the precondition that might not hold.
Execution trace:
(0,0): anon0
(0,0): anon35_Then
@@ -74,24 +74,24 @@ Execution trace: (0,0): anon36_Then
(0,0): anon5
(0,0): anon37_Then
-Iterators.dfy(89,14): Error: assertion violation
+Iterators.dfy(89,13): Error: assertion violation
Execution trace:
(0,0): anon0
-Iterators.dfy(119,16): Error: assertion violation
+Iterators.dfy(119,15): Error: assertion violation
Execution trace:
(0,0): anon0
(0,0): anon3_Else
-Iterators.dfy(150,16): Error: assertion violation
+Iterators.dfy(150,15): Error: assertion violation
Execution trace:
(0,0): anon0
(0,0): anon4_Else
-Iterators.dfy(155,24): Error BP5002: A precondition for this call might not hold.
-Iterators.dfy(125,10): Related location: This is the precondition that might not hold.
+Iterators.dfy(155,23): Error BP5002: A precondition for this call might not hold.
+Iterators.dfy(125,9): Related location: This is the precondition that might not hold.
Execution trace:
(0,0): anon0
(0,0): anon4_Then
(0,0): anon3
-Iterators.dfy(234,21): Error: assertion violation
+Iterators.dfy(234,20): Error: assertion violation
Execution trace:
(0,0): anon0
Iterators.dfy(225,3): anon14_LoopHead
diff --git a/Test/dafny0/LetExpr.dfy.expect b/Test/dafny0/LetExpr.dfy.expect index 66dc2764..f0f51274 100644 --- a/Test/dafny0/LetExpr.dfy.expect +++ b/Test/dafny0/LetExpr.dfy.expect @@ -1,35 +1,35 @@ -LetExpr.dfy(109,23): Error: assertion violation
+LetExpr.dfy(109,22): Error: assertion violation
Execution trace:
(0,0): anon0
(0,0): anon11_Then
-LetExpr.dfy(9,12): Error: assertion violation
+LetExpr.dfy(9,11): Error: assertion violation
Execution trace:
(0,0): anon0
-LetExpr.dfy(254,19): Error: value assigned to a nat must be non-negative
+LetExpr.dfy(254,18): Error: value assigned to a nat must be non-negative
Execution trace:
(0,0): anon0
(0,0): anon5_Then
-LetExpr.dfy(257,19): Error: value assigned to a nat must be non-negative
+LetExpr.dfy(257,18): Error: value assigned to a nat must be non-negative
Execution trace:
(0,0): anon0
(0,0): anon6_Then
-LetExpr.dfy(259,24): Error: value assigned to a nat must be non-negative
+LetExpr.dfy(259,23): Error: value assigned to a nat must be non-negative
Execution trace:
(0,0): anon0
(0,0): anon6_Else
-LetExpr.dfy(288,14): Error: RHS is not certain to look like the pattern 'Agnes'
+LetExpr.dfy(288,13): Error: RHS is not certain to look like the pattern 'Agnes'
Execution trace:
(0,0): anon0
(0,0): anon3_Else
-LetExpr.dfy(305,42): Error: value assigned to a nat must be non-negative
+LetExpr.dfy(305,41): Error: value assigned to a nat must be non-negative
Execution trace:
(0,0): anon0
(0,0): anon7_Else
-LetExpr.dfy(307,12): Error: assertion violation
+LetExpr.dfy(307,11): Error: assertion violation
Execution trace:
(0,0): anon0
(0,0): anon7_Else
-LetExpr.dfy(317,12): Error: to be compilable, the value of a let-such-that expression must be uniquely determined
+LetExpr.dfy(317,11): Error: to be compilable, the value of a let-such-that expression must be uniquely determined
Execution trace:
(0,0): anon0
(0,0): anon10_Then
diff --git a/Test/dafny0/LhsDuplicates.dfy.expect b/Test/dafny0/LhsDuplicates.dfy.expect index a864390f..d6689047 100644 --- a/Test/dafny0/LhsDuplicates.dfy.expect +++ b/Test/dafny0/LhsDuplicates.dfy.expect @@ -1,27 +1,27 @@ -LhsDuplicates.dfy(18,10): Error: left-hand sides for different forall-statement bound variables may refer to the same location
+LhsDuplicates.dfy(18,9): Error: left-hand sides for different forall-statement bound variables may refer to the same location
Execution trace:
(0,0): anon0
(0,0): anon16_Else
(0,0): anon18_Else
(0,0): anon21_Then
(0,0): anon13
-LhsDuplicates.dfy(34,12): Error: left-hand sides for different forall-statement bound variables may refer to the same location
+LhsDuplicates.dfy(34,11): Error: left-hand sides for different forall-statement bound variables may refer to the same location
Execution trace:
(0,0): anon0
(0,0): anon16_Else
(0,0): anon18_Else
(0,0): anon21_Then
(0,0): anon13
-LhsDuplicates.dfy(42,12): Error: when left-hand sides 1 and 3 refer to the same location, they must be assigned the same value
+LhsDuplicates.dfy(42,11): Error: when left-hand sides 1 and 3 refer to the same location, they must be assigned the same value
Execution trace:
(0,0): anon0
-LhsDuplicates.dfy(51,18): Error: when left-hand sides 0 and 2 refer to the same location, they must be assigned the same value
+LhsDuplicates.dfy(51,17): Error: when left-hand sides 0 and 2 refer to the same location, they must be assigned the same value
Execution trace:
(0,0): anon0
-LhsDuplicates.dfy(60,16): Error: when left-hand sides 1 and 2 may refer to the same location, they must be assigned the same value
+LhsDuplicates.dfy(60,15): Error: when left-hand sides 1 and 2 may refer to the same location, they must be assigned the same value
Execution trace:
(0,0): anon0
-LhsDuplicates.dfy(69,20): Error: when left-hand sides 1 and 2 refer to the same location, they must be assigned the same value
+LhsDuplicates.dfy(69,19): Error: when left-hand sides 1 and 2 refer to the same location, they must be assigned the same value
Execution trace:
(0,0): anon0
diff --git a/Test/dafny0/LoopModifies.dfy.expect b/Test/dafny0/LoopModifies.dfy.expect index 682975fb..a7ded8a4 100644 --- a/Test/dafny0/LoopModifies.dfy.expect +++ b/Test/dafny0/LoopModifies.dfy.expect @@ -1,38 +1,38 @@ -LoopModifies.dfy(8,5): Error: assignment may update an array element not in the enclosing context's modifies clause
+LoopModifies.dfy(8,4): Error: assignment may update an array element not in the enclosing context's modifies clause
Execution trace:
(0,0): anon0
-LoopModifies.dfy(19,8): Error: assignment may update an array element not in the enclosing context's modifies clause
+LoopModifies.dfy(19,7): Error: assignment may update an array element not in the enclosing context's modifies clause
Execution trace:
(0,0): anon0
LoopModifies.dfy(16,4): anon8_LoopHead
(0,0): anon8_LoopBody
LoopModifies.dfy(16,4): anon9_Else
LoopModifies.dfy(16,4): anon11_Else
-LoopModifies.dfy(48,8): Error: assignment may update an array element not in the enclosing context's modifies clause
+LoopModifies.dfy(48,7): Error: assignment may update an array element not in the enclosing context's modifies clause
Execution trace:
(0,0): anon0
LoopModifies.dfy(44,4): anon8_LoopHead
(0,0): anon8_LoopBody
LoopModifies.dfy(44,4): anon9_Else
LoopModifies.dfy(44,4): anon11_Else
-LoopModifies.dfy(63,8): Error: assignment may update an array element not in the enclosing context's modifies clause
+LoopModifies.dfy(63,7): Error: assignment may update an array element not in the enclosing context's modifies clause
Execution trace:
(0,0): anon0
LoopModifies.dfy(59,4): anon9_LoopHead
(0,0): anon9_LoopBody
LoopModifies.dfy(59,4): anon10_Else
LoopModifies.dfy(59,4): anon12_Else
-LoopModifies.dfy(76,4): Error: loop modifies clause may violate context's modifies clause
+LoopModifies.dfy(76,3): Error: loop modifies clause may violate context's modifies clause
Execution trace:
(0,0): anon0
-LoopModifies.dfy(100,8): Error: assignment may update an array element not in the enclosing context's modifies clause
+LoopModifies.dfy(100,7): Error: assignment may update an array element not in the enclosing context's modifies clause
Execution trace:
(0,0): anon0
LoopModifies.dfy(92,4): anon8_LoopHead
(0,0): anon8_LoopBody
LoopModifies.dfy(92,4): anon9_Else
LoopModifies.dfy(92,4): anon11_Else
-LoopModifies.dfy(148,11): Error: assignment may update an array element not in the enclosing context's modifies clause
+LoopModifies.dfy(148,10): Error: assignment may update an array element not in the enclosing context's modifies clause
Execution trace:
(0,0): anon0
LoopModifies.dfy(136,4): anon17_LoopHead
@@ -43,14 +43,14 @@ Execution trace: (0,0): anon21_LoopBody
LoopModifies.dfy(141,7): anon22_Else
LoopModifies.dfy(141,7): anon24_Else
-LoopModifies.dfy(199,10): Error: assignment may update an array element not in the enclosing context's modifies clause
+LoopModifies.dfy(199,9): Error: assignment may update an array element not in the enclosing context's modifies clause
Execution trace:
(0,0): anon0
LoopModifies.dfy(195,4): anon8_LoopHead
(0,0): anon8_LoopBody
LoopModifies.dfy(195,4): anon9_Else
LoopModifies.dfy(195,4): anon11_Else
-LoopModifies.dfy(287,13): Error: assignment may update an array element not in the enclosing context's modifies clause
+LoopModifies.dfy(287,12): Error: assignment may update an array element not in the enclosing context's modifies clause
Execution trace:
(0,0): anon0
LoopModifies.dfy(275,4): anon16_LoopHead
diff --git a/Test/dafny0/Maps.dfy.expect b/Test/dafny0/Maps.dfy.expect index f46549dd..8b4a6a36 100644 --- a/Test/dafny0/Maps.dfy.expect +++ b/Test/dafny0/Maps.dfy.expect @@ -1,7 +1,7 @@ -Maps.dfy(78,8): Error: element may not be in domain
+Maps.dfy(78,7): Error: element may not be in domain
Execution trace:
(0,0): anon0
-Maps.dfy(128,13): Error: assertion violation
+Maps.dfy(128,12): Error: assertion violation
Execution trace:
(0,0): anon0
diff --git a/Test/dafny0/ModifyStmt.dfy.expect b/Test/dafny0/ModifyStmt.dfy.expect index 4ea872e0..019453d1 100644 --- a/Test/dafny0/ModifyStmt.dfy.expect +++ b/Test/dafny0/ModifyStmt.dfy.expect @@ -1,19 +1,19 @@ -ModifyStmt.dfy(27,14): Error: assertion violation
+ModifyStmt.dfy(27,13): Error: assertion violation
Execution trace:
(0,0): anon0
-ModifyStmt.dfy(42,5): Error: modify statement may violate context's modifies clause
+ModifyStmt.dfy(42,4): Error: modify statement may violate context's modifies clause
Execution trace:
(0,0): anon0
-ModifyStmt.dfy(48,5): Error: modify statement may violate context's modifies clause
+ModifyStmt.dfy(48,4): Error: modify statement may violate context's modifies clause
Execution trace:
(0,0): anon0
-ModifyStmt.dfy(61,5): Error: modify statement may violate context's modifies clause
+ModifyStmt.dfy(61,4): Error: modify statement may violate context's modifies clause
Execution trace:
(0,0): anon0
-ModifyStmt.dfy(70,14): Error: assertion violation
+ModifyStmt.dfy(70,13): Error: assertion violation
Execution trace:
(0,0): anon0
-ModifyStmt.dfy(89,14): Error: assertion violation
+ModifyStmt.dfy(89,13): Error: assertion violation
Execution trace:
(0,0): anon0
(0,0): anon9_Then
@@ -22,20 +22,20 @@ Execution trace: ModifyStmt.dfy(81,7): anon11_Else
(0,0): anon12_Then
(0,0): anon8
-ModifyStmt.dfy(99,14): Error: assertion violation
+ModifyStmt.dfy(99,13): Error: assertion violation
Execution trace:
(0,0): anon0
-ModifyStmt.dfy(110,14): Error: assertion violation
+ModifyStmt.dfy(110,13): Error: assertion violation
Execution trace:
(0,0): anon0
-ModifyStmt.dfy(122,16): Error: assertion violation
+ModifyStmt.dfy(122,15): Error: assertion violation
Execution trace:
(0,0): anon0
(0,0): anon3_Then
-ModifyStmt.dfy(134,7): Error: assignment may update an object not in the enclosing context's modifies clause
+ModifyStmt.dfy(134,6): Error: assignment may update an object not in the enclosing context's modifies clause
Execution trace:
(0,0): anon0
-ModifyStmt.dfy(172,15): Error: assertion violation
+ModifyStmt.dfy(172,14): Error: assertion violation
Execution trace:
(0,0): anon0
diff --git a/Test/dafny0/Modules0.dfy.expect b/Test/dafny0/Modules0.dfy.expect index c63ed937..e4b46cce 100644 --- a/Test/dafny0/Modules0.dfy.expect +++ b/Test/dafny0/Modules0.dfy.expect @@ -1,5 +1,5 @@ -Modules0.dfy(333,3): warning: module-level functions are always non-instance, so the 'static' keyword is not allowed here
-Modules0.dfy(335,3): warning: module-level methods are always non-instance, so the 'static' keyword is not allowed here
+Modules0.dfy(333,2): Warning: module-level functions are always non-instance, so the 'static' keyword is not allowed here
+Modules0.dfy(335,2): Warning: module-level methods are always non-instance, so the 'static' keyword is not allowed here
Modules0.dfy(8,8): Error: Duplicate name of top-level declaration: WazzupA
Modules0.dfy(9,11): Error: Duplicate name of top-level declaration: WazzupA
Modules0.dfy(10,7): Error: Duplicate name of top-level declaration: WazzupA
diff --git a/Test/dafny0/Modules1.dfy.expect b/Test/dafny0/Modules1.dfy.expect index 342b5808..feddf46a 100644 --- a/Test/dafny0/Modules1.dfy.expect +++ b/Test/dafny0/Modules1.dfy.expect @@ -1,20 +1,20 @@ -Modules1.dfy(79,16): Error: assertion violation
+Modules1.dfy(79,15): Error: assertion violation
Execution trace:
(0,0): anon0
(0,0): anon3_Then
-Modules1.dfy(92,16): Error: assertion violation
+Modules1.dfy(92,15): Error: assertion violation
Execution trace:
(0,0): anon0
(0,0): anon3_Then
-Modules1.dfy(94,18): Error: assertion violation
+Modules1.dfy(94,17): Error: assertion violation
Execution trace:
(0,0): anon0
(0,0): anon3_Else
-Modules1.dfy(56,9): Error: decreases expression must be bounded below by 0
-Modules1.dfy(54,13): Related location
+Modules1.dfy(56,8): Error: decreases expression must be bounded below by 0
+Modules1.dfy(54,12): Related location
Execution trace:
(0,0): anon0
-Modules1.dfy(62,9): Error: failure to decrease termination measure
+Modules1.dfy(62,8): Error: failure to decrease termination measure
Execution trace:
(0,0): anon0
diff --git a/Test/dafny0/MultiDimArray.dfy.expect b/Test/dafny0/MultiDimArray.dfy.expect index 597ade30..f2bf74de 100644 --- a/Test/dafny0/MultiDimArray.dfy.expect +++ b/Test/dafny0/MultiDimArray.dfy.expect @@ -1,9 +1,9 @@ -MultiDimArray.dfy(56,21): Error: assertion violation
+MultiDimArray.dfy(56,20): Error: assertion violation
Execution trace:
(0,0): anon0
(0,0): anon11_Then
(0,0): anon12_Then
-MultiDimArray.dfy(83,25): Error: assertion violation
+MultiDimArray.dfy(83,24): Error: assertion violation
Execution trace:
(0,0): anon0
(0,0): anon5_Then
diff --git a/Test/dafny0/MultiSets.dfy.expect b/Test/dafny0/MultiSets.dfy.expect index 30534b11..aed70bd2 100644 --- a/Test/dafny0/MultiSets.dfy.expect +++ b/Test/dafny0/MultiSets.dfy.expect @@ -1,24 +1,24 @@ -MultiSets.dfy(159,3): Error BP5003: A postcondition might not hold on this return path.
-MultiSets.dfy(158,15): Related location: This is the postcondition that might not hold.
+MultiSets.dfy(159,2): Error BP5003: A postcondition might not hold on this return path.
+MultiSets.dfy(158,14): Related location: This is the postcondition that might not hold.
Execution trace:
(0,0): anon0
-MultiSets.dfy(165,3): Error BP5003: A postcondition might not hold on this return path.
-MultiSets.dfy(164,15): Related location: This is the postcondition that might not hold.
+MultiSets.dfy(165,2): Error BP5003: A postcondition might not hold on this return path.
+MultiSets.dfy(164,14): Related location: This is the postcondition that might not hold.
Execution trace:
(0,0): anon0
-MultiSets.dfy(178,11): Error: new number of occurrences might be negative
+MultiSets.dfy(178,10): Error: new number of occurrences might be negative
Execution trace:
(0,0): anon0
(0,0): anon4_Then
(0,0): anon3
-MultiSets.dfy(269,24): Error: assertion violation
+MultiSets.dfy(269,23): Error: assertion violation
Execution trace:
(0,0): anon0
(0,0): anon11_Then
(0,0): anon3
(0,0): anon12_Then
(0,0): anon14_Else
-MultiSets.dfy(292,16): Error: assertion violation
+MultiSets.dfy(292,15): Error: assertion violation
Execution trace:
(0,0): anon0
(0,0): anon8_Then
diff --git a/Test/dafny0/NatTypes.dfy.expect b/Test/dafny0/NatTypes.dfy.expect index 5af90253..2bc00e95 100644 --- a/Test/dafny0/NatTypes.dfy.expect +++ b/Test/dafny0/NatTypes.dfy.expect @@ -1,41 +1,41 @@ -NatTypes.dfy(35,12): Error: value assigned to a nat must be non-negative
+NatTypes.dfy(35,11): Error: value assigned to a nat must be non-negative
Execution trace:
(0,0): anon0
NatTypes.dfy(23,5): anon10_LoopHead
(0,0): anon10_LoopBody
NatTypes.dfy(23,5): anon11_Else
(0,0): anon12_Then
-NatTypes.dfy(10,5): Error: value assigned to a nat must be non-negative
+NatTypes.dfy(10,4): Error: value assigned to a nat must be non-negative
Execution trace:
(0,0): anon0
-NatTypes.dfy(43,14): Error: assertion violation
+NatTypes.dfy(43,13): Error: assertion violation
Execution trace:
(0,0): anon0
(0,0): anon4_Then
-NatTypes.dfy(45,14): Error: assertion violation
+NatTypes.dfy(45,13): Error: assertion violation
Execution trace:
(0,0): anon0
(0,0): anon4_Then
-NatTypes.dfy(62,16): Error: assertion violation
+NatTypes.dfy(62,15): Error: assertion violation
Execution trace:
(0,0): anon0
(0,0): anon3_Then
-NatTypes.dfy(76,16): Error: assertion violation
+NatTypes.dfy(76,15): Error: assertion violation
Execution trace:
(0,0): anon0
(0,0): anon5_Else
(0,0): anon6_Then
-NatTypes.dfy(94,22): Error: value assigned to a nat must be non-negative
+NatTypes.dfy(94,21): Error: value assigned to a nat must be non-negative
Execution trace:
(0,0): anon0
(0,0): anon3_Then
-NatTypes.dfy(109,45): Error: value assigned to a nat must be non-negative
+NatTypes.dfy(109,44): Error: value assigned to a nat must be non-negative
Execution trace:
(0,0): anon0
(0,0): anon8_Else
(0,0): anon9_Else
(0,0): anon10_Then
-NatTypes.dfy(132,35): Error: value assigned to a nat must be non-negative
+NatTypes.dfy(132,34): Error: value assigned to a nat must be non-negative
Execution trace:
(0,0): anon0
(0,0): anon4_Then
diff --git a/Test/dafny0/Newtypes.dfy.expect b/Test/dafny0/Newtypes.dfy.expect index 8e6ff4c5..425ee9a9 100644 --- a/Test/dafny0/Newtypes.dfy.expect +++ b/Test/dafny0/Newtypes.dfy.expect @@ -1,54 +1,54 @@ -Newtypes.dfy(74,11): Error: cannot find witness that shows type is inhabited (sorry, for now, only tried 0)
+Newtypes.dfy(74,10): Error: cannot find witness that shows type is inhabited (sorry, for now, only tried 0)
Execution trace:
(0,0): anon0
-Newtypes.dfy(76,45): Error: possible division by zero
+Newtypes.dfy(76,44): Error: possible division by zero
Execution trace:
(0,0): anon0
(0,0): anon3_Then
-Newtypes.dfy(87,14): Error: result of operation might violate newtype constraint
+Newtypes.dfy(87,13): Error: result of operation might violate newtype constraint
Execution trace:
(0,0): anon0
-Newtypes.dfy(95,12): Error: result of operation might violate newtype constraint
+Newtypes.dfy(95,11): Error: result of operation might violate newtype constraint
Execution trace:
(0,0): anon0
(0,0): anon3_Then
-Newtypes.dfy(97,14): Error: result of operation might violate newtype constraint
+Newtypes.dfy(97,13): Error: result of operation might violate newtype constraint
Execution trace:
(0,0): anon0
(0,0): anon3_Else
-Newtypes.dfy(104,16): Error: result of operation might violate newtype constraint
+Newtypes.dfy(104,15): Error: result of operation might violate newtype constraint
Execution trace:
(0,0): anon0
-Newtypes.dfy(177,14): Error: result of operation might violate newtype constraint
+Newtypes.dfy(177,13): Error: result of operation might violate newtype constraint
Execution trace:
(0,0): anon0
-Newtypes.dfy(193,64): Error: index 0 out of range
+Newtypes.dfy(193,63): Error: index 0 out of range
Execution trace:
(0,0): anon0
(0,0): anon32_Then
(0,0): anon33_Then
(0,0): anon16
-Newtypes.dfy(194,67): Error: index 1 out of range
+Newtypes.dfy(194,66): Error: index 1 out of range
Execution trace:
(0,0): anon0
(0,0): anon34_Then
(0,0): anon35_Then
(0,0): anon19
-Newtypes.dfy(222,16): Error: new number of occurrences might be negative
+Newtypes.dfy(222,15): Error: new number of occurrences might be negative
Execution trace:
(0,0): anon0
(0,0): anon6_Then
-Newtypes.dfy(225,40): Error: result of operation might violate newtype constraint
+Newtypes.dfy(225,39): Error: result of operation might violate newtype constraint
Execution trace:
(0,0): anon0
(0,0): anon8_Then
-Newtypes.dfy(237,19): Error: result of operation might violate newtype constraint
+Newtypes.dfy(237,18): Error: result of operation might violate newtype constraint
Execution trace:
(0,0): anon0
Newtypes.dfy(236,5): anon9_LoopHead
(0,0): anon9_LoopBody
(0,0): anon10_Then
-Newtypes.dfy(277,19): Error: result of operation might violate newtype constraint
+Newtypes.dfy(277,18): Error: result of operation might violate newtype constraint
Execution trace:
(0,0): anon0
Newtypes.dfy(276,5): anon9_LoopHead
diff --git a/Test/dafny0/OpaqueFunctions.dfy.expect b/Test/dafny0/OpaqueFunctions.dfy.expect index 2fb1701f..e9f6e60c 100644 --- a/Test/dafny0/OpaqueFunctions.dfy.expect +++ b/Test/dafny0/OpaqueFunctions.dfy.expect @@ -1,86 +1,86 @@ -OpaqueFunctions.dfy(27,16): Error: assertion violation
+OpaqueFunctions.dfy(27,15): Error: assertion violation
Execution trace:
(0,0): anon0
-OpaqueFunctions.dfy(52,8): Error BP5002: A precondition for this call might not hold.
-OpaqueFunctions.dfy(24,16): Related location: This is the precondition that might not hold.
+OpaqueFunctions.dfy(52,7): Error BP5002: A precondition for this call might not hold.
+OpaqueFunctions.dfy(24,15): Related location: This is the precondition that might not hold.
Execution trace:
(0,0): anon0
-OpaqueFunctions.dfy(58,20): Error: assertion violation
+OpaqueFunctions.dfy(58,19): Error: assertion violation
Execution trace:
(0,0): anon0
-OpaqueFunctions.dfy(60,21): Error: assertion violation
+OpaqueFunctions.dfy(60,20): Error: assertion violation
Execution trace:
(0,0): anon0
(0,0): anon5_Then
-OpaqueFunctions.dfy(63,21): Error: assertion violation
+OpaqueFunctions.dfy(63,20): Error: assertion violation
Execution trace:
(0,0): anon0
(0,0): anon6_Then
-OpaqueFunctions.dfy(66,21): Error: assertion violation
+OpaqueFunctions.dfy(66,20): Error: assertion violation
Execution trace:
(0,0): anon0
(0,0): anon6_Else
-OpaqueFunctions.dfy(77,21): Error: assertion violation
+OpaqueFunctions.dfy(77,20): Error: assertion violation
Execution trace:
(0,0): anon0
(0,0): anon3_Then
-OpaqueFunctions.dfy(79,10): Error BP5002: A precondition for this call might not hold.
-OpaqueFunctions.dfy[A'](24,16): Related location: This is the precondition that might not hold.
+OpaqueFunctions.dfy(79,9): Error BP5002: A precondition for this call might not hold.
+OpaqueFunctions.dfy[A'](24,15): Related location: This is the precondition that might not hold.
Execution trace:
(0,0): anon0
(0,0): anon3_Else
-OpaqueFunctions.dfy(86,20): Error: assertion violation
+OpaqueFunctions.dfy(86,19): Error: assertion violation
Execution trace:
(0,0): anon0
-OpaqueFunctions.dfy(88,21): Error: assertion violation
+OpaqueFunctions.dfy(88,20): Error: assertion violation
Execution trace:
(0,0): anon0
(0,0): anon5_Then
-OpaqueFunctions.dfy(91,21): Error: assertion violation
+OpaqueFunctions.dfy(91,20): Error: assertion violation
Execution trace:
(0,0): anon0
(0,0): anon6_Then
-OpaqueFunctions.dfy(94,21): Error: assertion violation
+OpaqueFunctions.dfy(94,20): Error: assertion violation
Execution trace:
(0,0): anon0
(0,0): anon6_Else
-OpaqueFunctions.dfy(105,21): Error: assertion violation
+OpaqueFunctions.dfy(105,20): Error: assertion violation
Execution trace:
(0,0): anon0
(0,0): anon3_Then
-OpaqueFunctions.dfy(107,10): Error BP5002: A precondition for this call might not hold.
-OpaqueFunctions.dfy[A'](24,16): Related location: This is the precondition that might not hold.
+OpaqueFunctions.dfy(107,9): Error BP5002: A precondition for this call might not hold.
+OpaqueFunctions.dfy[A'](24,15): Related location: This is the precondition that might not hold.
Execution trace:
(0,0): anon0
(0,0): anon3_Else
-OpaqueFunctions.dfy(114,20): Error: assertion violation
+OpaqueFunctions.dfy(114,19): Error: assertion violation
Execution trace:
(0,0): anon0
-OpaqueFunctions.dfy(116,21): Error: assertion violation
+OpaqueFunctions.dfy(116,20): Error: assertion violation
Execution trace:
(0,0): anon0
(0,0): anon5_Then
-OpaqueFunctions.dfy(119,21): Error: assertion violation
+OpaqueFunctions.dfy(119,20): Error: assertion violation
Execution trace:
(0,0): anon0
(0,0): anon6_Then
-OpaqueFunctions.dfy(122,21): Error: assertion violation
+OpaqueFunctions.dfy(122,20): Error: assertion violation
Execution trace:
(0,0): anon0
(0,0): anon6_Else
-OpaqueFunctions.dfy(138,13): Error: assertion violation
+OpaqueFunctions.dfy(138,12): Error: assertion violation
Execution trace:
(0,0): anon0
-OpaqueFunctions.dfy(202,12): Error: assertion violation
+OpaqueFunctions.dfy(202,11): Error: assertion violation
Execution trace:
(0,0): anon0
-OpaqueFunctions.dfy(218,12): Error: assertion violation
+OpaqueFunctions.dfy(218,11): Error: assertion violation
Execution trace:
(0,0): anon0
-OpaqueFunctions.dfy(170,16): Error: assertion violation
+OpaqueFunctions.dfy(170,15): Error: assertion violation
Execution trace:
(0,0): anon0
-OpaqueFunctions.dfy(185,20): Error: assertion violation
+OpaqueFunctions.dfy(185,19): Error: assertion violation
Execution trace:
(0,0): anon0
diff --git a/Test/dafny0/Parallel.dfy.expect b/Test/dafny0/Parallel.dfy.expect index db551bba..5d9b044f 100644 --- a/Test/dafny0/Parallel.dfy.expect +++ b/Test/dafny0/Parallel.dfy.expect @@ -1,9 +1,9 @@ -Parallel.dfy(297,22): Error: assertion violation
+Parallel.dfy(297,21): Error: assertion violation
Execution trace:
(0,0): anon0
(0,0): anon4_Else
-Parallel.dfy(34,10): Error BP5002: A precondition for this call might not hold.
-Parallel.dfy(60,14): Related location: This is the precondition that might not hold.
+Parallel.dfy(34,9): Error BP5002: A precondition for this call might not hold.
+Parallel.dfy(60,13): Related location: This is the precondition that might not hold.
Execution trace:
(0,0): anon0
(0,0): anon29_Else
@@ -12,7 +12,7 @@ Execution trace: (0,0): anon34_Then
(0,0): anon35_Then
(0,0): anon14
-Parallel.dfy(38,5): Error: target object may be null
+Parallel.dfy(38,4): Error: target object may be null
Execution trace:
(0,0): anon0
(0,0): anon29_Else
@@ -22,7 +22,7 @@ Execution trace: (0,0): anon37_Then
(0,0): anon38_Then
(0,0): anon20
-Parallel.dfy(42,18): Error: possible violation of postcondition of forall statement
+Parallel.dfy(42,17): Error: possible violation of postcondition of forall statement
Execution trace:
(0,0): anon0
(0,0): anon29_Else
@@ -32,7 +32,7 @@ Execution trace: (0,0): anon39_Then
(0,0): anon40_Then
(0,0): anon26
-Parallel.dfy(47,19): Error: assertion violation
+Parallel.dfy(47,18): Error: assertion violation
Execution trace:
(0,0): anon0
(0,0): anon29_Else
@@ -41,24 +41,24 @@ Execution trace: (0,0): anon36_Else
(0,0): anon39_Then
(0,0): anon40_Then
-Parallel.dfy(93,19): Error: assertion violation
+Parallel.dfy(93,18): Error: assertion violation
Execution trace:
(0,0): anon0
(0,0): anon10_Else
(0,0): anon11_Then
-Parallel.dfy(99,20): Error: possible violation of postcondition of forall statement
+Parallel.dfy(99,19): Error: possible violation of postcondition of forall statement
Execution trace:
(0,0): anon0
(0,0): anon10_Else
(0,0): anon11_Then
(0,0): anon12_Then
-Parallel.dfy(122,12): Error: value assigned to a nat must be non-negative
+Parallel.dfy(122,11): Error: value assigned to a nat must be non-negative
Execution trace:
(0,0): anon0
(0,0): anon6_Then
(0,0): anon7_Then
(0,0): anon3
-Parallel.dfy(185,12): Error: left-hand sides for different forall-statement bound variables may refer to the same location
+Parallel.dfy(185,11): Error: left-hand sides for different forall-statement bound variables may refer to the same location
Execution trace:
(0,0): anon0
(0,0): anon19_Then
diff --git a/Test/dafny0/ParseErrors.dfy.expect b/Test/dafny0/ParseErrors.dfy.expect index 30898479..660ed926 100644 --- a/Test/dafny0/ParseErrors.dfy.expect +++ b/Test/dafny0/ParseErrors.dfy.expect @@ -1,17 +1,17 @@ -ParseErrors.dfy(7,19): error: a chain cannot have more than one != operator
-ParseErrors.dfy(9,37): error: this operator chain cannot continue with a descending operator
-ParseErrors.dfy(10,38): error: this operator chain cannot continue with an ascending operator
-ParseErrors.dfy(15,24): error: this operator chain cannot continue with a descending operator
-ParseErrors.dfy(18,18): error: this operator cannot be part of a chain
-ParseErrors.dfy(19,19): error: this operator cannot be part of a chain
-ParseErrors.dfy(20,18): error: this operator cannot be part of a chain
-ParseErrors.dfy(21,18): error: chaining not allowed from the previous operator
-ParseErrors.dfy(28,19): error: chaining not allowed from the previous operator
-ParseErrors.dfy(31,20): error: can only chain disjoint (!!) with itself.
-ParseErrors.dfy(58,8): error: the main operator of a calculation must be transitive
-ParseErrors.dfy(74,2): error: this operator cannot continue this calculation
-ParseErrors.dfy(75,2): error: this operator cannot continue this calculation
-ParseErrors.dfy(80,2): error: this operator cannot continue this calculation
-ParseErrors.dfy(81,2): error: this operator cannot continue this calculation
-ParseErrors.dfy(87,2): error: this operator cannot continue this calculation
+ParseErrors.dfy(7,18): Error: a chain cannot have more than one != operator
+ParseErrors.dfy(9,36): Error: this operator chain cannot continue with a descending operator
+ParseErrors.dfy(10,37): Error: this operator chain cannot continue with an ascending operator
+ParseErrors.dfy(15,23): Error: this operator chain cannot continue with a descending operator
+ParseErrors.dfy(18,17): Error: this operator cannot be part of a chain
+ParseErrors.dfy(19,18): Error: this operator cannot be part of a chain
+ParseErrors.dfy(20,17): Error: this operator cannot be part of a chain
+ParseErrors.dfy(21,17): Error: chaining not allowed from the previous operator
+ParseErrors.dfy(28,18): Error: chaining not allowed from the previous operator
+ParseErrors.dfy(31,19): Error: can only chain disjoint (!!) with itself.
+ParseErrors.dfy(58,7): Error: the main operator of a calculation must be transitive
+ParseErrors.dfy(74,1): Error: this operator cannot continue this calculation
+ParseErrors.dfy(75,1): Error: this operator cannot continue this calculation
+ParseErrors.dfy(80,1): Error: this operator cannot continue this calculation
+ParseErrors.dfy(81,1): Error: this operator cannot continue this calculation
+ParseErrors.dfy(87,1): Error: this operator cannot continue this calculation
16 parse errors detected in ParseErrors.dfy
diff --git a/Test/dafny0/PredExpr.dfy.expect b/Test/dafny0/PredExpr.dfy.expect index 18d5d73f..80f311cb 100644 --- a/Test/dafny0/PredExpr.dfy.expect +++ b/Test/dafny0/PredExpr.dfy.expect @@ -1,16 +1,16 @@ -PredExpr.dfy(7,12): Error: assertion violation
+PredExpr.dfy(7,11): Error: assertion violation
Execution trace:
(0,0): anon0
(0,0): anon4_Else
-PredExpr.dfy(39,15): Error: value assigned to a nat must be non-negative
+PredExpr.dfy(39,14): Error: value assigned to a nat must be non-negative
Execution trace:
(0,0): anon0
(0,0): anon7_Else
(0,0): anon8_Else
-PredExpr.dfy(52,17): Error: assertion violation
+PredExpr.dfy(52,16): Error: assertion violation
Execution trace:
(0,0): anon0
-PredExpr.dfy(77,14): Error: assertion violation
+PredExpr.dfy(77,13): Error: assertion violation
Execution trace:
(0,0): anon0
(0,0): anon8_Else
diff --git a/Test/dafny0/Predicates.dfy.expect b/Test/dafny0/Predicates.dfy.expect index dac4eb3c..2d7ea6f1 100644 --- a/Test/dafny0/Predicates.dfy.expect +++ b/Test/dafny0/Predicates.dfy.expect @@ -1,26 +1,26 @@ -Predicates.dfy[B](21,5): Error BP5003: A postcondition might not hold on this return path.
-Predicates.dfy[B](20,15): Related location: This is the postcondition that might not hold.
-Predicates.dfy(31,9): Related location
+Predicates.dfy[B](21,4): Error BP5003: A postcondition might not hold on this return path.
+Predicates.dfy[B](20,14): Related location: This is the postcondition that might not hold.
+Predicates.dfy(31,8): Related location
Execution trace:
(0,0): anon0
-Predicates.dfy(88,16): Error: assertion violation
+Predicates.dfy(88,15): Error: assertion violation
Execution trace:
(0,0): anon0
-Predicates.dfy(92,14): Error: assertion violation
+Predicates.dfy(92,13): Error: assertion violation
Execution trace:
(0,0): anon0
-Predicates.dfy[Tricky_Full](126,5): Error BP5003: A postcondition might not hold on this return path.
-Predicates.dfy[Tricky_Full](125,15): Related location: This is the postcondition that might not hold.
-Predicates.dfy(136,7): Related location
-Predicates.dfy[Tricky_Full](116,9): Related location
+Predicates.dfy[Tricky_Full](126,4): Error BP5003: A postcondition might not hold on this return path.
+Predicates.dfy[Tricky_Full](125,14): Related location: This is the postcondition that might not hold.
+Predicates.dfy(136,6): Related location
+Predicates.dfy[Tricky_Full](116,8): Related location
Execution trace:
(0,0): anon0
-Predicates.dfy(164,5): Error BP5003: A postcondition might not hold on this return path.
-Predicates.dfy(163,15): Related location: This is the postcondition that might not hold.
+Predicates.dfy(164,4): Error BP5003: A postcondition might not hold on this return path.
+Predicates.dfy(163,14): Related location: This is the postcondition that might not hold.
Execution trace:
(0,0): anon0
-Predicates.dfy[Q1](154,5): Error BP5003: A postcondition might not hold on this return path.
-Predicates.dfy[Q1](153,15): Related location: This is the postcondition that might not hold.
+Predicates.dfy[Q1](154,4): Error BP5003: A postcondition might not hold on this return path.
+Predicates.dfy[Q1](153,14): Related location: This is the postcondition that might not hold.
Execution trace:
(0,0): anon0
diff --git a/Test/dafny0/Protected.dfy.expect b/Test/dafny0/Protected.dfy.expect index d50f2dd5..6796e847 100644 --- a/Test/dafny0/Protected.dfy.expect +++ b/Test/dafny0/Protected.dfy.expect @@ -1,20 +1,20 @@ -Protected.dfy(17,20): Error: assertion violation
+Protected.dfy(17,19): Error: assertion violation
Execution trace:
(0,0): anon0
(0,0): anon9_Then
-Protected.dfy(31,18): Error: assertion violation
+Protected.dfy(31,17): Error: assertion violation
Execution trace:
(0,0): anon0
(0,0): anon12_Then
(0,0): anon6
(0,0): anon13_Else
-Protected.dfy(35,16): Error: assertion violation
+Protected.dfy(35,15): Error: assertion violation
Execution trace:
(0,0): anon0
-Protected.dfy(48,20): Error: assertion violation
+Protected.dfy(48,19): Error: assertion violation
Execution trace:
(0,0): anon0
-Protected.dfy(55,20): Error: assertion violation
+Protected.dfy(55,19): Error: assertion violation
Execution trace:
(0,0): anon0
diff --git a/Test/dafny0/RankNeg.dfy.expect b/Test/dafny0/RankNeg.dfy.expect index b2686b43..33cd4f1e 100644 --- a/Test/dafny0/RankNeg.dfy.expect +++ b/Test/dafny0/RankNeg.dfy.expect @@ -1,19 +1,19 @@ -RankNeg.dfy(10,26): Error: cannot prove termination; try supplying a decreases clause
+RankNeg.dfy(10,25): Error: cannot prove termination; try supplying a decreases clause
Execution trace:
(0,0): anon0
(0,0): anon7_Else
(0,0): anon8_Then
-RankNeg.dfy(15,28): Error: cannot prove termination; try supplying a decreases clause
+RankNeg.dfy(15,27): Error: cannot prove termination; try supplying a decreases clause
Execution trace:
(0,0): anon0
(0,0): anon7_Else
(0,0): anon8_Then
-RankNeg.dfy(22,31): Error: cannot prove termination; try supplying a decreases clause
+RankNeg.dfy(22,30): Error: cannot prove termination; try supplying a decreases clause
Execution trace:
(0,0): anon0
(0,0): anon7_Else
(0,0): anon8_Then
-RankNeg.dfy(32,25): Error: cannot prove termination; try supplying a decreases clause
+RankNeg.dfy(32,24): Error: cannot prove termination; try supplying a decreases clause
Execution trace:
(0,0): anon0
(0,0): anon7_Else
diff --git a/Test/dafny0/Reads.dfy.expect b/Test/dafny0/Reads.dfy.expect index 1199797f..0ef90aec 100644 --- a/Test/dafny0/Reads.dfy.expect +++ b/Test/dafny0/Reads.dfy.expect @@ -1,32 +1,32 @@ -Reads.dfy(133,11): Error: insufficient reads clause to read field
+Reads.dfy(133,10): Error: insufficient reads clause to read field
Execution trace:
(0,0): anon0
-Reads.dfy(9,30): Error: insufficient reads clause to read field
+Reads.dfy(9,29): Error: insufficient reads clause to read field
Execution trace:
(0,0): anon0
-Reads.dfy(18,30): Error: insufficient reads clause to read field
+Reads.dfy(18,29): Error: insufficient reads clause to read field
Execution trace:
(0,0): anon0
-Reads.dfy(28,50): Error: insufficient reads clause to read field
+Reads.dfy(28,49): Error: insufficient reads clause to read field
Execution trace:
(0,0): anon0
-Reads.dfy(37,43): Error: insufficient reads clause to read field
+Reads.dfy(37,42): Error: insufficient reads clause to read field
Execution trace:
(0,0): anon0
(0,0): anon7_Then
(0,0): anon4
-Reads.dfy(51,30): Error: insufficient reads clause to read field
+Reads.dfy(51,29): Error: insufficient reads clause to read field
Execution trace:
(0,0): anon0
(0,0): anon10_Then
(0,0): anon4
-Reads.dfy(117,36): Error: insufficient reads clause to invoke function
+Reads.dfy(117,35): Error: insufficient reads clause to invoke function
Execution trace:
(0,0): anon0
-Reads.dfy(117,36): Error: possible violation of function precondition
+Reads.dfy(117,35): Error: possible violation of function precondition
Execution trace:
(0,0): anon0
-Reads.dfy(120,38): Error: insufficient reads clause to invoke function
+Reads.dfy(120,37): Error: insufficient reads clause to invoke function
Execution trace:
(0,0): anon0
diff --git a/Test/dafny0/RealCompare.dfy.expect b/Test/dafny0/RealCompare.dfy.expect index 5b25fa25..48524bdf 100644 --- a/Test/dafny0/RealCompare.dfy.expect +++ b/Test/dafny0/RealCompare.dfy.expect @@ -1,19 +1,19 @@ -RealCompare.dfy(35,6): Error: failure to decrease termination measure
+RealCompare.dfy(35,5): Error: failure to decrease termination measure
Execution trace:
(0,0): anon0
(0,0): anon3_Then
-RealCompare.dfy(50,4): Error: decreases expression must be bounded below by 0.0
-RealCompare.dfy(48,13): Related location
+RealCompare.dfy(50,3): Error: decreases expression must be bounded below by 0.0
+RealCompare.dfy(48,12): Related location
Execution trace:
(0,0): anon0
-RealCompare.dfy(141,12): Error: assertion violation
+RealCompare.dfy(141,11): Error: assertion violation
Execution trace:
(0,0): anon0
RealCompare.dfy(133,3): anon7_LoopHead
(0,0): anon7_LoopBody
RealCompare.dfy(133,3): anon8_Else
(0,0): anon9_Then
-RealCompare.dfy(156,12): Error: assertion violation
+RealCompare.dfy(156,11): Error: assertion violation
Execution trace:
(0,0): anon0
RealCompare.dfy(147,3): anon9_LoopHead
diff --git a/Test/dafny0/RealTypes.dfy.expect b/Test/dafny0/RealTypes.dfy.expect index 0d132948..0fce4634 100644 --- a/Test/dafny0/RealTypes.dfy.expect +++ b/Test/dafny0/RealTypes.dfy.expect @@ -1,22 +1,22 @@ -RealTypes.dfy(12,16): Error: the real-based number must be an integer (if you want truncation, apply .Trunc to the real-based number)
+RealTypes.dfy(12,15): Error: the real-based number must be an integer (if you want truncation, apply .Trunc to the real-based number)
Execution trace:
(0,0): anon0
(0,0): anon6_Then
-RealTypes.dfy(14,28): Error: assertion violation
+RealTypes.dfy(14,27): Error: assertion violation
Execution trace:
(0,0): anon0
(0,0): anon7_Then
-RealTypes.dfy(21,12): Error: possible division by zero
+RealTypes.dfy(21,11): Error: possible division by zero
Execution trace:
(0,0): anon0
RealTypes.dfy(20,23): anon3_Else
(0,0): anon2
-RealTypes.dfy(21,20): Error: assertion violation
+RealTypes.dfy(21,19): Error: assertion violation
Execution trace:
(0,0): anon0
RealTypes.dfy(20,23): anon3_Else
(0,0): anon2
-RealTypes.dfy(29,12): Error: assertion violation
+RealTypes.dfy(29,11): Error: assertion violation
Execution trace:
(0,0): anon0
diff --git a/Test/dafny0/Refinement.dfy.expect b/Test/dafny0/Refinement.dfy.expect index d03b9412..339c86b4 100644 --- a/Test/dafny0/Refinement.dfy.expect +++ b/Test/dafny0/Refinement.dfy.expect @@ -1,40 +1,40 @@ -Refinement.dfy(15,5): Error BP5003: A postcondition might not hold on this return path.
-Refinement.dfy(14,17): Related location: This is the postcondition that might not hold.
+Refinement.dfy(15,4): Error BP5003: A postcondition might not hold on this return path.
+Refinement.dfy(14,16): Related location: This is the postcondition that might not hold.
Execution trace:
(0,0): anon0
-Refinement.dfy[B](15,5): Error BP5003: A postcondition might not hold on this return path.
-Refinement.dfy(33,20): Related location: This is the postcondition that might not hold.
+Refinement.dfy[B](15,4): Error BP5003: A postcondition might not hold on this return path.
+Refinement.dfy(33,19): Related location: This is the postcondition that might not hold.
Execution trace:
(0,0): anon0
-Refinement.dfy(69,16): Error: assertion violation
+Refinement.dfy(69,15): Error: assertion violation
Execution trace:
(0,0): anon0
-Refinement.dfy(80,17): Error: assertion violation
+Refinement.dfy(80,16): Error: assertion violation
Execution trace:
(0,0): anon0
-Refinement.dfy(99,12): Error BP5003: A postcondition might not hold on this return path.
-Refinement.dfy(78,15): Related location: This is the postcondition that might not hold.
+Refinement.dfy(99,11): Error BP5003: A postcondition might not hold on this return path.
+Refinement.dfy(78,14): Related location: This is the postcondition that might not hold.
Execution trace:
(0,0): anon0
(0,0): anon4_Else
-Refinement.dfy(102,3): Error BP5003: A postcondition might not hold on this return path.
-Refinement.dfy(83,15): Related location: This is the postcondition that might not hold.
+Refinement.dfy(102,2): Error BP5003: A postcondition might not hold on this return path.
+Refinement.dfy(83,14): Related location: This is the postcondition that might not hold.
Execution trace:
(0,0): anon0
-Refinement.dfy(189,5): Error BP5003: A postcondition might not hold on this return path.
-Refinement.dfy[IncorrectConcrete](121,15): Related location: This is the postcondition that might not hold.
-Refinement.dfy(186,9): Related location
+Refinement.dfy(189,4): Error BP5003: A postcondition might not hold on this return path.
+Refinement.dfy[IncorrectConcrete](121,14): Related location: This is the postcondition that might not hold.
+Refinement.dfy(186,8): Related location
Execution trace:
(0,0): anon0
-Refinement.dfy(193,5): Error BP5003: A postcondition might not hold on this return path.
-Refinement.dfy[IncorrectConcrete](129,15): Related location: This is the postcondition that might not hold.
-Refinement.dfy(186,9): Related location
+Refinement.dfy(193,4): Error BP5003: A postcondition might not hold on this return path.
+Refinement.dfy[IncorrectConcrete](129,14): Related location: This is the postcondition that might not hold.
+Refinement.dfy(186,8): Related location
Execution trace:
(0,0): anon0
(0,0): anon4_Then
(0,0): anon3
-Refinement.dfy(199,7): Error: assertion violation
-Refinement.dfy[IncorrectConcrete](137,24): Related location
+Refinement.dfy(199,6): Error: assertion violation
+Refinement.dfy[IncorrectConcrete](137,23): Related location
Execution trace:
(0,0): anon0
diff --git a/Test/dafny0/Skeletons.dfy.expect b/Test/dafny0/Skeletons.dfy.expect index 43b372c3..4b48bad0 100644 --- a/Test/dafny0/Skeletons.dfy.expect +++ b/Test/dafny0/Skeletons.dfy.expect @@ -1,5 +1,5 @@ -Skeletons.dfy(45,3): Error BP5003: A postcondition might not hold on this return path.
-Skeletons.dfy(44,15): Related location: This is the postcondition that might not hold.
+Skeletons.dfy(45,2): Error BP5003: A postcondition might not hold on this return path.
+Skeletons.dfy(44,14): Related location: This is the postcondition that might not hold.
Execution trace:
(0,0): anon0
Skeletons.dfy[C0](32,5): anon11_LoopHead
diff --git a/Test/dafny0/SmallTests.dfy.expect b/Test/dafny0/SmallTests.dfy.expect index b0605d8e..eee0d4f1 100644 --- a/Test/dafny0/SmallTests.dfy.expect +++ b/Test/dafny0/SmallTests.dfy.expect @@ -1,41 +1,41 @@ -SmallTests.dfy(34,11): Error: index out of range
+SmallTests.dfy(34,10): Error: index out of range
Execution trace:
(0,0): anon0
-SmallTests.dfy(65,36): Error: possible division by zero
+SmallTests.dfy(65,35): Error: possible division by zero
Execution trace:
(0,0): anon0
(0,0): anon13_Then
-SmallTests.dfy(66,51): Error: possible division by zero
+SmallTests.dfy(66,50): Error: possible division by zero
Execution trace:
(0,0): anon0
(0,0): anon13_Else
(0,0): anon14_Else
-SmallTests.dfy(67,22): Error: target object may be null
+SmallTests.dfy(67,21): Error: target object may be null
Execution trace:
(0,0): anon0
(0,0): anon13_Then
(0,0): anon14_Then
(0,0): anon15_Then
-SmallTests.dfy(86,24): Error: target object may be null
+SmallTests.dfy(86,23): Error: target object may be null
Execution trace:
(0,0): anon0
SmallTests.dfy(85,5): anon8_LoopHead
(0,0): anon8_LoopBody
(0,0): anon9_Then
-SmallTests.dfy(120,6): Error: call may violate context's modifies clause
+SmallTests.dfy(120,5): Error: call may violate context's modifies clause
Execution trace:
(0,0): anon0
(0,0): anon4_Else
(0,0): anon3
-SmallTests.dfy(133,10): Error: call may violate context's modifies clause
+SmallTests.dfy(133,9): Error: call may violate context's modifies clause
Execution trace:
(0,0): anon0
(0,0): anon3_Then
-SmallTests.dfy(135,10): Error: call may violate context's modifies clause
+SmallTests.dfy(135,9): Error: call may violate context's modifies clause
Execution trace:
(0,0): anon0
(0,0): anon3_Else
-SmallTests.dfy(175,9): Error: assignment may update an object field not in the enclosing context's modifies clause
+SmallTests.dfy(175,8): Error: assignment may update an object field not in the enclosing context's modifies clause
Execution trace:
(0,0): anon0
(0,0): anon22_Else
@@ -44,23 +44,23 @@ Execution trace: (0,0): anon28_Then
(0,0): anon29_Then
(0,0): anon19
-SmallTests.dfy(199,14): Error: assertion violation
+SmallTests.dfy(199,13): Error: assertion violation
Execution trace:
(0,0): anon0
(0,0): anon9_Then
-SmallTests.dfy(206,14): Error: assertion violation
+SmallTests.dfy(206,13): Error: assertion violation
Execution trace:
(0,0): anon0
(0,0): anon9_Else
(0,0): anon3
(0,0): anon10_Then
-SmallTests.dfy(208,14): Error: assertion violation
+SmallTests.dfy(208,13): Error: assertion violation
Execution trace:
(0,0): anon0
(0,0): anon9_Else
(0,0): anon3
(0,0): anon10_Else
-SmallTests.dfy(213,14): Error: assertion violation
+SmallTests.dfy(213,13): Error: assertion violation
Execution trace:
(0,0): anon0
(0,0): anon9_Else
@@ -68,7 +68,7 @@ Execution trace: (0,0): anon10_Then
(0,0): anon6
(0,0): anon11_Then
-SmallTests.dfy(215,14): Error: assertion violation
+SmallTests.dfy(215,13): Error: assertion violation
Execution trace:
(0,0): anon0
(0,0): anon9_Else
@@ -76,37 +76,37 @@ Execution trace: (0,0): anon10_Then
(0,0): anon6
(0,0): anon11_Else
-SmallTests.dfy(261,24): Error BP5002: A precondition for this call might not hold.
-SmallTests.dfy(239,30): Related location: This is the precondition that might not hold.
+SmallTests.dfy(261,23): Error BP5002: A precondition for this call might not hold.
+SmallTests.dfy(239,29): Related location: This is the precondition that might not hold.
Execution trace:
(0,0): anon0
SmallTests.dfy(256,19): anon3_Else
(0,0): anon2
-SmallTests.dfy(367,12): Error: assertion violation
+SmallTests.dfy(367,11): Error: assertion violation
Execution trace:
(0,0): anon0
-SmallTests.dfy(377,12): Error: assertion violation
+SmallTests.dfy(377,11): Error: assertion violation
Execution trace:
(0,0): anon0
-SmallTests.dfy(387,6): Error: cannot prove termination; try supplying a decreases clause
+SmallTests.dfy(387,5): Error: cannot prove termination; try supplying a decreases clause
Execution trace:
(0,0): anon0
(0,0): anon4_Else
-SmallTests.dfy(692,14): Error: assertion violation
+SmallTests.dfy(692,13): Error: assertion violation
Execution trace:
(0,0): anon0
SmallTests.dfy(689,5): anon7_LoopHead
(0,0): anon7_LoopBody
SmallTests.dfy(689,5): anon8_Else
(0,0): anon9_Then
-SmallTests.dfy(713,14): Error: assertion violation
+SmallTests.dfy(713,13): Error: assertion violation
Execution trace:
(0,0): anon0
(0,0): anon7_Then
(0,0): anon8_Then
(0,0): anon3
-SmallTests.dfy(296,3): Error BP5003: A postcondition might not hold on this return path.
-SmallTests.dfy(290,11): Related location: This is the postcondition that might not hold.
+SmallTests.dfy(296,2): Error BP5003: A postcondition might not hold on this return path.
+SmallTests.dfy(290,10): Related location: This is the postcondition that might not hold.
Execution trace:
(0,0): anon0
(0,0): anon18_Else
@@ -114,29 +114,29 @@ Execution trace: (0,0): anon24_Then
(0,0): anon15
(0,0): anon25_Else
-SmallTests.dfy(338,12): Error: assertion violation
+SmallTests.dfy(338,11): Error: assertion violation
Execution trace:
(0,0): anon0
(0,0): anon8_Then
(0,0): anon7
-SmallTests.dfy(345,10): Error: assertion violation
+SmallTests.dfy(345,9): Error: assertion violation
Execution trace:
(0,0): anon0
-SmallTests.dfy(355,4): Error: cannot prove termination; try supplying a decreases clause
+SmallTests.dfy(355,3): Error: cannot prove termination; try supplying a decreases clause
Execution trace:
(0,0): anon0
(0,0): anon4_Else
-SmallTests.dfy(399,10): Error BP5003: A postcondition might not hold on this return path.
-SmallTests.dfy(402,41): Related location: This is the postcondition that might not hold.
+SmallTests.dfy(399,9): Error BP5003: A postcondition might not hold on this return path.
+SmallTests.dfy(402,40): Related location: This is the postcondition that might not hold.
Execution trace:
(0,0): anon0
(0,0): anon7_Else
-SmallTests.dfy(563,12): Error: assertion violation
+SmallTests.dfy(563,11): Error: assertion violation
Execution trace:
(0,0): anon0
(0,0): anon3_Then
(0,0): anon2
-SmallTests.dfy(577,20): Error: left-hand sides 0 and 1 may refer to the same location
+SmallTests.dfy(577,19): Error: left-hand sides 0 and 1 may refer to the same location
Execution trace:
(0,0): anon0
(0,0): anon27_Then
@@ -148,7 +148,7 @@ Execution trace: (0,0): anon31_Then
(0,0): anon32_Then
(0,0): anon12
-SmallTests.dfy(579,15): Error: left-hand sides 1 and 2 may refer to the same location
+SmallTests.dfy(579,14): Error: left-hand sides 1 and 2 may refer to the same location
Execution trace:
(0,0): anon0
(0,0): anon27_Then
@@ -163,16 +163,16 @@ Execution trace: (0,0): anon37_Then
(0,0): anon22
(0,0): anon38_Then
-SmallTests.dfy(586,25): Error: target object may be null
+SmallTests.dfy(586,24): Error: target object may be null
Execution trace:
(0,0): anon0
-SmallTests.dfy(599,10): Error: assertion violation
+SmallTests.dfy(599,9): Error: assertion violation
Execution trace:
(0,0): anon0
-SmallTests.dfy(623,5): Error: cannot establish the existence of LHS values that satisfy the such-that predicate
+SmallTests.dfy(623,4): Error: cannot establish the existence of LHS values that satisfy the such-that predicate
Execution trace:
(0,0): anon0
-SmallTests.dfy(646,23): Error: assertion violation
+SmallTests.dfy(646,22): Error: assertion violation
Execution trace:
(0,0): anon0
(0,0): anon8_Then
@@ -180,17 +180,17 @@ Execution trace: (0,0): anon4
(0,0): anon10_Then
(0,0): anon7
-SmallTests.dfy(660,10): Error: cannot establish the existence of LHS values that satisfy the such-that predicate
+SmallTests.dfy(660,9): Error: cannot establish the existence of LHS values that satisfy the such-that predicate
Execution trace:
(0,0): anon0
(0,0): anon5_Then
(0,0): anon6_Then
(0,0): anon3
-SmallTests.dfy(662,10): Error: cannot establish the existence of LHS values that satisfy the such-that predicate
+SmallTests.dfy(662,9): Error: cannot establish the existence of LHS values that satisfy the such-that predicate
Execution trace:
(0,0): anon0
(0,0): anon5_Else
-SmallTests.dfy(675,9): Error: cannot establish the existence of LHS values that satisfy the such-that predicate
+SmallTests.dfy(675,8): Error: cannot establish the existence of LHS values that satisfy the such-that predicate
Execution trace:
(0,0): anon0
diff --git a/Test/dafny0/SplitExpr.dfy.expect b/Test/dafny0/SplitExpr.dfy.expect index b7ef524f..29dd6eda 100644 --- a/Test/dafny0/SplitExpr.dfy.expect +++ b/Test/dafny0/SplitExpr.dfy.expect @@ -1,5 +1,5 @@ -SplitExpr.dfy(92,15): Error: loop invariant violation
-SplitExpr.dfy(86,44): Related location
+SplitExpr.dfy(92,14): Error: loop invariant violation
+SplitExpr.dfy(86,43): Related location
Execution trace:
SplitExpr.dfy(91,3): anon7_LoopHead
diff --git a/Test/dafny0/StatementExpressions.dfy.expect b/Test/dafny0/StatementExpressions.dfy.expect index 9de6a5d1..936a3954 100644 --- a/Test/dafny0/StatementExpressions.dfy.expect +++ b/Test/dafny0/StatementExpressions.dfy.expect @@ -1,22 +1,22 @@ -StatementExpressions.dfy(55,12): Error: cannot prove termination; try supplying a decreases clause
+StatementExpressions.dfy(55,11): Error: cannot prove termination; try supplying a decreases clause
Execution trace:
(0,0): anon0
(0,0): anon6_Then
(0,0): anon8_Then
-StatementExpressions.dfy(59,14): Error: assertion violation
+StatementExpressions.dfy(59,13): Error: assertion violation
Execution trace:
(0,0): anon0
(0,0): anon6_Then
StatementExpressions.dfy(53,7): anon8_Else
-StatementExpressions.dfy(77,6): Error: possible division by zero
+StatementExpressions.dfy(77,5): Error: possible division by zero
Execution trace:
(0,0): anon0
(0,0): anon4_Else
-StatementExpressions.dfy(88,5): Error: value assigned to a nat must be non-negative
+StatementExpressions.dfy(88,4): Error: value assigned to a nat must be non-negative
Execution trace:
(0,0): anon0
(0,0): anon4_Else
-StatementExpressions.dfy(98,18): Error: cannot prove termination; try supplying a decreases clause
+StatementExpressions.dfy(98,17): Error: cannot prove termination; try supplying a decreases clause
Execution trace:
(0,0): anon0
(0,0): anon6_Then
diff --git a/Test/dafny0/Superposition.dfy.expect b/Test/dafny0/Superposition.dfy.expect index 6497c712..04ec2f7d 100644 --- a/Test/dafny0/Superposition.dfy.expect +++ b/Test/dafny0/Superposition.dfy.expect @@ -10,16 +10,16 @@ Verifying CheckWellformed$$_0_M0.C.P ... Verifying CheckWellformed$$_0_M0.C.Q ...
[5 proof obligations] error
-Superposition.dfy(27,15): Error BP5003: A postcondition might not hold on this return path.
-Superposition.dfy(28,26): Related location: This is the postcondition that might not hold.
+Superposition.dfy(27,14): Error BP5003: A postcondition might not hold on this return path.
+Superposition.dfy(28,25): Related location: This is the postcondition that might not hold.
Execution trace:
(0,0): anon0
(0,0): anon7_Else
Verifying CheckWellformed$$_0_M0.C.R ...
[5 proof obligations] error
-Superposition.dfy(33,15): Error BP5003: A postcondition might not hold on this return path.
-Superposition.dfy(34,26): Related location: This is the postcondition that might not hold.
+Superposition.dfy(33,14): Error BP5003: A postcondition might not hold on this return path.
+Superposition.dfy(34,25): Related location: This is the postcondition that might not hold.
Execution trace:
(0,0): anon0
(0,0): anon7_Else
@@ -32,8 +32,8 @@ Verifying Impl$$_1_M1.C.M ... Verifying CheckWellformed$$_1_M1.C.P ...
[2 proof obligations] error
-Superposition.dfy(50,25): Error BP5003: A postcondition might not hold on this return path.
-Superposition.dfy[M1](22,26): Related location: This is the postcondition that might not hold.
+Superposition.dfy(50,24): Error BP5003: A postcondition might not hold on this return path.
+Superposition.dfy[M1](22,25): Related location: This is the postcondition that might not hold.
Execution trace:
(0,0): anon0
(0,0): anon9_Else
diff --git a/Test/dafny0/Termination.dfy.expect b/Test/dafny0/Termination.dfy.expect index 77a9e70e..69cb360d 100644 --- a/Test/dafny0/Termination.dfy.expect +++ b/Test/dafny0/Termination.dfy.expect @@ -1,20 +1,20 @@ -Termination.dfy[TerminationRefinement1](441,6): Error: failure to decrease termination measure
+Termination.dfy[TerminationRefinement1](441,5): Error: failure to decrease termination measure
Execution trace:
(0,0): anon0
-Termination.dfy(361,47): Error: failure to decrease termination measure
+Termination.dfy(361,46): Error: failure to decrease termination measure
Execution trace:
(0,0): anon0
(0,0): anon9_Else
(0,0): anon10_Then
(0,0): anon11_Else
-Termination.dfy(108,3): Error: cannot prove termination; try supplying a decreases clause for the loop
+Termination.dfy(108,2): Error: cannot prove termination; try supplying a decreases clause for the loop
Execution trace:
(0,0): anon0
Termination.dfy(108,3): anon6_LoopHead
(0,0): anon6_LoopBody
Termination.dfy(108,3): anon7_Else
Termination.dfy(108,3): anon8_Else
-Termination.dfy(116,3): Error: cannot prove termination; try supplying a decreases clause for the loop
+Termination.dfy(116,2): Error: cannot prove termination; try supplying a decreases clause for the loop
Execution trace:
(0,0): anon0
Termination.dfy(116,3): anon8_LoopHead
@@ -23,7 +23,7 @@ Execution trace: (0,0): anon10_Then
(0,0): anon5
Termination.dfy(116,3): anon11_Else
-Termination.dfy(125,3): Error: decreases expression might not decrease
+Termination.dfy(125,2): Error: decreases expression might not decrease
Execution trace:
(0,0): anon0
Termination.dfy(125,3): anon8_LoopHead
@@ -32,7 +32,7 @@ Execution trace: (0,0): anon10_Then
(0,0): anon5
Termination.dfy(125,3): anon11_Else
-Termination.dfy(126,17): Error: decreases expression must be bounded below by 0 at end of loop iteration
+Termination.dfy(126,16): Error: decreases expression must be bounded below by 0 at end of loop iteration
Execution trace:
(0,0): anon0
Termination.dfy(125,3): anon8_LoopHead
@@ -41,13 +41,13 @@ Execution trace: (0,0): anon10_Then
(0,0): anon5
Termination.dfy(125,3): anon11_Else
-Termination.dfy(255,35): Error: cannot prove termination; try supplying a decreases clause
+Termination.dfy(255,34): Error: cannot prove termination; try supplying a decreases clause
Execution trace:
(0,0): anon0
(0,0): anon8_Else
(0,0): anon9_Else
(0,0): anon10_Then
-Termination.dfy(296,3): Error: decreases expression might not decrease
+Termination.dfy(296,2): Error: decreases expression might not decrease
Execution trace:
Termination.dfy(296,3): anon9_LoopHead
(0,0): anon9_LoopBody
diff --git a/Test/dafny0/Trait/TraitUsingParentMembers.dfy.expect b/Test/dafny0/Trait/TraitUsingParentMembers.dfy.expect index 9960c1d9..1517dee4 100644 --- a/Test/dafny0/Trait/TraitUsingParentMembers.dfy.expect +++ b/Test/dafny0/Trait/TraitUsingParentMembers.dfy.expect @@ -1,4 +1,4 @@ -TraitUsingParentMembers.dfy(10,8): Error: assignment may update an array element not in the enclosing context's modifies clause
+TraitUsingParentMembers.dfy(10,7): Error: assignment may update an array element not in the enclosing context's modifies clause
Execution trace:
(0,0): anon0
(0,0): anon5_Then
diff --git a/Test/dafny0/Trait/TraitsDecreases.dfy.expect b/Test/dafny0/Trait/TraitsDecreases.dfy.expect index 2607a0c6..7d646bd1 100644 --- a/Test/dafny0/Trait/TraitsDecreases.dfy.expect +++ b/Test/dafny0/Trait/TraitsDecreases.dfy.expect @@ -1,34 +1,34 @@ -TraitsDecreases.dfy(117,15): Error: predicate's decreases clause must be below or equal to that in the trait
+TraitsDecreases.dfy(117,14): Error: predicate's decreases clause must be below or equal to that in the trait
Execution trace:
(0,0): anon0
-TraitsDecreases.dfy(124,15): Error: predicate's decreases clause must be below or equal to that in the trait
+TraitsDecreases.dfy(124,14): Error: predicate's decreases clause must be below or equal to that in the trait
Execution trace:
(0,0): anon0
-TraitsDecreases.dfy(131,15): Error: predicate's decreases clause must be below or equal to that in the trait
+TraitsDecreases.dfy(131,14): Error: predicate's decreases clause must be below or equal to that in the trait
Execution trace:
(0,0): anon0
-TraitsDecreases.dfy(138,15): Error: predicate's decreases clause must be below or equal to that in the trait
+TraitsDecreases.dfy(138,14): Error: predicate's decreases clause must be below or equal to that in the trait
Execution trace:
(0,0): anon0
-TraitsDecreases.dfy(145,15): Error: predicate's decreases clause must be below or equal to that in the trait
+TraitsDecreases.dfy(145,14): Error: predicate's decreases clause must be below or equal to that in the trait
Execution trace:
(0,0): anon0
-TraitsDecreases.dfy(152,12): Error: method's decreases clause must be below or equal to that in the trait
+TraitsDecreases.dfy(152,11): Error: method's decreases clause must be below or equal to that in the trait
Execution trace:
(0,0): anon0
-TraitsDecreases.dfy(57,10): Error: method's decreases clause must be below or equal to that in the trait
+TraitsDecreases.dfy(57,9): Error: method's decreases clause must be below or equal to that in the trait
Execution trace:
(0,0): anon0
-TraitsDecreases.dfy(69,10): Error: method's decreases clause must be below or equal to that in the trait
+TraitsDecreases.dfy(69,9): Error: method's decreases clause must be below or equal to that in the trait
Execution trace:
(0,0): anon0
-TraitsDecreases.dfy(72,10): Error: method's decreases clause must be below or equal to that in the trait
+TraitsDecreases.dfy(72,9): Error: method's decreases clause must be below or equal to that in the trait
Execution trace:
(0,0): anon0
-TraitsDecreases.dfy(78,10): Error: method's decreases clause must be below or equal to that in the trait
+TraitsDecreases.dfy(78,9): Error: method's decreases clause must be below or equal to that in the trait
Execution trace:
(0,0): anon0
-TraitsDecreases.dfy(88,10): Error: method's decreases clause must be below or equal to that in the trait
+TraitsDecreases.dfy(88,9): Error: method's decreases clause must be below or equal to that in the trait
Execution trace:
(0,0): anon0
diff --git a/Test/dafny0/Tuples.dfy.expect b/Test/dafny0/Tuples.dfy.expect index 13c706d3..9b5f3a83 100644 --- a/Test/dafny0/Tuples.dfy.expect +++ b/Test/dafny0/Tuples.dfy.expect @@ -1,7 +1,7 @@ -Tuples.dfy(22,19): Error: assertion violation
+Tuples.dfy(22,18): Error: assertion violation
Execution trace:
(0,0): anon0
-Tuples.dfy(24,21): Error: possible division by zero
+Tuples.dfy(24,20): Error: possible division by zero
Execution trace:
(0,0): anon0
diff --git a/Test/dafny0/TypeAntecedents.dfy.expect b/Test/dafny0/TypeAntecedents.dfy.expect index d6eb08e4..2e2f606d 100644 --- a/Test/dafny0/TypeAntecedents.dfy.expect +++ b/Test/dafny0/TypeAntecedents.dfy.expect @@ -1,8 +1,8 @@ -TypeAntecedents.dfy(35,13): Error: assertion violation
+TypeAntecedents.dfy(35,12): Error: assertion violation
Execution trace:
(0,0): anon0
-TypeAntecedents.dfy(58,1): Error BP5003: A postcondition might not hold on this return path.
-TypeAntecedents.dfy(57,15): Related location: This is the postcondition that might not hold.
+TypeAntecedents.dfy(58,0): Error BP5003: A postcondition might not hold on this return path.
+TypeAntecedents.dfy(57,14): Related location: This is the postcondition that might not hold.
Execution trace:
(0,0): anon0
(0,0): anon25_Then
@@ -16,7 +16,7 @@ Execution trace: (0,0): anon34_Then
(0,0): anon35_Then
(0,0): anon24
-TypeAntecedents.dfy(66,16): Error: assertion violation
+TypeAntecedents.dfy(66,15): Error: assertion violation
Execution trace:
(0,0): anon0
(0,0): anon25_Else
diff --git a/Test/dafny0/TypeParameters.dfy.expect b/Test/dafny0/TypeParameters.dfy.expect index 3d00e89a..aca0694d 100644 --- a/Test/dafny0/TypeParameters.dfy.expect +++ b/Test/dafny0/TypeParameters.dfy.expect @@ -1,43 +1,43 @@ -TypeParameters.dfy(47,22): Error: assertion violation
+TypeParameters.dfy(47,21): Error: assertion violation
Execution trace:
(0,0): anon0
-TypeParameters.dfy(69,27): Error: assertion violation
+TypeParameters.dfy(69,26): Error: assertion violation
Execution trace:
(0,0): anon0
(0,0): anon3_Then
(0,0): anon2
-TypeParameters.dfy(156,12): Error: assertion violation
-TypeParameters.dfy(156,28): Related location
+TypeParameters.dfy(156,11): Error: assertion violation
+TypeParameters.dfy(156,27): Related location
Execution trace:
(0,0): anon0
(0,0): anon20_Then
TypeParameters.dfy(156,32): anon21_Else
(0,0): anon5
-TypeParameters.dfy(158,12): Error: assertion violation
-TypeParameters.dfy(158,33): Related location
+TypeParameters.dfy(158,11): Error: assertion violation
+TypeParameters.dfy(158,32): Related location
Execution trace:
(0,0): anon0
(0,0): anon23_Then
TypeParameters.dfy(158,37): anon24_Else
(0,0): anon11
-TypeParameters.dfy(160,12): Error: assertion violation
-TypeParameters.dfy(160,20): Related location
+TypeParameters.dfy(160,11): Error: assertion violation
+TypeParameters.dfy(160,19): Related location
Execution trace:
(0,0): anon0
(0,0): anon25_Then
-TypeParameters.dfy(162,12): Error: assertion violation
-TypeParameters.dfy(147,5): Related location
-TypeParameters.dfy(162,21): Related location
+TypeParameters.dfy(162,11): Error: assertion violation
+TypeParameters.dfy(147,4): Related location
+TypeParameters.dfy(162,20): Related location
Execution trace:
(0,0): anon0
(0,0): anon26_Then
-TypeParameters.dfy(164,12): Error: assertion violation
-TypeParameters.dfy(149,8): Related location
+TypeParameters.dfy(164,11): Error: assertion violation
+TypeParameters.dfy(149,7): Related location
Execution trace:
(0,0): anon0
(0,0): anon27_Then
-TypeParameters.dfy(178,15): Error BP5005: This loop invariant might not be maintained by the loop.
-TypeParameters.dfy(178,38): Related location
+TypeParameters.dfy(178,14): Error BP5005: This loop invariant might not be maintained by the loop.
+TypeParameters.dfy(178,37): Related location
Execution trace:
(0,0): anon0
TypeParameters.dfy(171,3): anon16_LoopHead
diff --git a/Test/dafny0/columns.dfy b/Test/dafny0/columns.dfy new file mode 100644 index 00000000..e36142be --- /dev/null +++ b/Test/dafny0/columns.dfy @@ -0,0 +1,10 @@ +// RUN: %dafny "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+
+// Dafny counts columns from 0, but Boogie from one, so for a while there were small bugs with that.
+
+static method A(x:int) requires x > 0 { // error os 's'
+ assert (forall y :: y > x ==> y > 100); // error on '('
+ assert x != 1; // error on '!'
+ assert x in {}; // error on 'i'
+}
diff --git a/Test/dafny0/columns.dfy.expect b/Test/dafny0/columns.dfy.expect new file mode 100644 index 00000000..295ca351 --- /dev/null +++ b/Test/dafny0/columns.dfy.expect @@ -0,0 +1,18 @@ +columns.dfy(6,0): Warning: module-level methods are always non-instance, so the 'static' keyword is not allowed here
+columns.dfy(7,9): Error: assertion violation
+Execution trace:
+ (0,0): anon0
+ (0,0): anon3_Then
+ (0,0): anon2
+columns.dfy(8,11): Error: assertion violation
+Execution trace:
+ (0,0): anon0
+ (0,0): anon3_Then
+ (0,0): anon2
+columns.dfy(9,11): Error: assertion violation
+Execution trace:
+ (0,0): anon0
+ (0,0): anon3_Then
+ (0,0): anon2
+
+Dafny program verifier finished with 1 verified, 3 errors
diff --git a/Test/dafny0/snapshots/Snapshots0.run.dfy.expect b/Test/dafny0/snapshots/Snapshots0.run.dfy.expect index 96c280d9..d32cd9bb 100644 --- a/Test/dafny0/snapshots/Snapshots0.run.dfy.expect +++ b/Test/dafny0/snapshots/Snapshots0.run.dfy.expect @@ -18,7 +18,7 @@ Processing command (at <unknown location>) a##cached##0 := a##cached##0 && ##ext >>> AssumeNegationOfAssumptionVariable
Processing command (at Snapshots0.v1.dfy(4,10)) assert Lit(false);
>>> MarkAsPartiallyVerified
-Snapshots0.v1.dfy(4,10): Error: assertion violation
+Snapshots0.v1.dfy(4,9): Error: assertion violation
Execution trace:
(0,0): anon0
diff --git a/Test/dafny0/snapshots/Snapshots1.run.dfy.expect b/Test/dafny0/snapshots/Snapshots1.run.dfy.expect index 878f9905..6d5e43f8 100644 --- a/Test/dafny0/snapshots/Snapshots1.run.dfy.expect +++ b/Test/dafny0/snapshots/Snapshots1.run.dfy.expect @@ -14,7 +14,7 @@ Processing command (at Snapshots1.v1.dfy(3,4)) assert (forall<alpha> $o: ref, $f >>> MarkAsFullyVerified
Processing command (at Snapshots1.v1.dfy(4,10)) assert Lit(false);
>>> DoNothingToAssert
-Snapshots1.v1.dfy(4,10): Error: assertion violation
+Snapshots1.v1.dfy(4,9): Error: assertion violation
Execution trace:
(0,0): anon0
diff --git a/Test/dafny0/snapshots/Snapshots2.run.dfy.expect b/Test/dafny0/snapshots/Snapshots2.run.dfy.expect index a6a9bc4c..ee2ceecd 100644 --- a/Test/dafny0/snapshots/Snapshots2.run.dfy.expect +++ b/Test/dafny0/snapshots/Snapshots2.run.dfy.expect @@ -26,7 +26,7 @@ Processing command (at Snapshots2.v1.dfy(3,4)) assert (forall<alpha> $o: ref, $f >>> MarkAsFullyVerified
Processing command (at Snapshots2.v1.dfy(4,10)) assert Lit(false);
>>> DoNothingToAssert
-Snapshots2.v1.dfy(4,10): Error: assertion violation
+Snapshots2.v1.dfy(4,9): Error: assertion violation
Execution trace:
(0,0): anon0
Processing command (at Snapshots2.v1.dfy(11,11)) assert true;
diff --git a/Test/dafny0/snapshots/Snapshots3.run.dfy.expect b/Test/dafny0/snapshots/Snapshots3.run.dfy.expect index 07e2d063..accacd90 100644 --- a/Test/dafny0/snapshots/Snapshots3.run.dfy.expect +++ b/Test/dafny0/snapshots/Snapshots3.run.dfy.expect @@ -1,6 +1,6 @@ Processing command (at Snapshots3.v0.dfy(9,14)) assert Lit(0 != 0);
>>> DoNothingToAssert
-Snapshots3.v0.dfy(9,14): Error: assertion violation
+Snapshots3.v0.dfy(9,13): Error: assertion violation
Execution trace:
(0,0): anon0
(0,0): anon3_Else
@@ -10,7 +10,7 @@ Processing command (at Snapshots3.v1.dfy(5,12)) assert Lit(true); >>> DoNothingToAssert
Processing command (at Snapshots3.v1.dfy(9,14)) assert Lit(0 != 0);
>>> RecycleError
-Snapshots3.v0.dfy(9,14): Error: assertion violation
+Snapshots3.v0.dfy(9,13): Error: assertion violation
Execution trace:
(0,0): anon0
(0,0): anon3_Else
diff --git a/Test/dafny0/snapshots/Snapshots4.run.dfy.expect b/Test/dafny0/snapshots/Snapshots4.run.dfy.expect index fdc97775..d56eb9d0 100644 --- a/Test/dafny0/snapshots/Snapshots4.run.dfy.expect +++ b/Test/dafny0/snapshots/Snapshots4.run.dfy.expect @@ -8,11 +8,11 @@ Processing command (at Snapshots4.v1.dfy(9,14)) assert LitInt(0) == LitInt(0); >>> MarkAsFullyVerified
Processing command (at Snapshots4.v1.dfy(10,14)) assert Lit(2 != 2);
>>> DoNothingToAssert
-Snapshots4.v1.dfy(5,14): Error: assertion violation
+Snapshots4.v1.dfy(5,13): Error: assertion violation
Execution trace:
(0,0): anon0
(0,0): anon3_Then
-Snapshots4.v1.dfy(10,14): Error: assertion violation
+Snapshots4.v1.dfy(10,13): Error: assertion violation
Execution trace:
(0,0): anon0
(0,0): anon3_Else
diff --git a/Test/dafny0/snapshots/Snapshots6.run.dfy.expect b/Test/dafny0/snapshots/Snapshots6.run.dfy.expect index af440327..bef5a87d 100644 --- a/Test/dafny0/snapshots/Snapshots6.run.dfy.expect +++ b/Test/dafny0/snapshots/Snapshots6.run.dfy.expect @@ -4,7 +4,7 @@ Processing command (at Snapshots6.v0.dfy(20,14)) assert Lit(false); Dafny program verifier finished with 4 verified, 0 errors
Processing command (at Snapshots6.v1.dfy(20,14)) assert Lit(false);
>>> DoNothingToAssert
-Snapshots6.v1.dfy(20,14): Error: assertion violation
+Snapshots6.v1.dfy(20,13): Error: assertion violation
Execution trace:
(0,0): anon0
diff --git a/Test/dafny0/snapshots/Snapshots7.run.dfy.expect b/Test/dafny0/snapshots/Snapshots7.run.dfy.expect index 7c073a9a..b90a6034 100644 --- a/Test/dafny0/snapshots/Snapshots7.run.dfy.expect +++ b/Test/dafny0/snapshots/Snapshots7.run.dfy.expect @@ -24,7 +24,7 @@ Processing command (at <unknown location>) a##cached##0 := a##cached##0 && ##ext >>> AssumeNegationOfAssumptionVariable
Processing command (at Snapshots7.v1.dfy(19,14)) assert Lit(false);
>>> MarkAsPartiallyVerified
-Snapshots7.v1.dfy(19,14): Error: assertion violation
+Snapshots7.v1.dfy(19,13): Error: assertion violation
Execution trace:
(0,0): anon0
diff --git a/Test/dafny1/MoreInduction.dfy.expect b/Test/dafny1/MoreInduction.dfy.expect index c8785e56..5de0ace6 100644 --- a/Test/dafny1/MoreInduction.dfy.expect +++ b/Test/dafny1/MoreInduction.dfy.expect @@ -1,17 +1,17 @@ -MoreInduction.dfy(78,1): Error BP5003: A postcondition might not hold on this return path.
-MoreInduction.dfy(77,11): Related location: This is the postcondition that might not hold.
+MoreInduction.dfy(78,0): Error BP5003: A postcondition might not hold on this return path.
+MoreInduction.dfy(77,10): Related location: This is the postcondition that might not hold.
Execution trace:
(0,0): anon0
-MoreInduction.dfy(83,1): Error BP5003: A postcondition might not hold on this return path.
-MoreInduction.dfy(82,21): Related location: This is the postcondition that might not hold.
+MoreInduction.dfy(83,0): Error BP5003: A postcondition might not hold on this return path.
+MoreInduction.dfy(82,20): Related location: This is the postcondition that might not hold.
Execution trace:
(0,0): anon0
-MoreInduction.dfy(88,1): Error BP5003: A postcondition might not hold on this return path.
-MoreInduction.dfy(87,11): Related location: This is the postcondition that might not hold.
+MoreInduction.dfy(88,0): Error BP5003: A postcondition might not hold on this return path.
+MoreInduction.dfy(87,10): Related location: This is the postcondition that might not hold.
Execution trace:
(0,0): anon0
-MoreInduction.dfy(93,1): Error BP5003: A postcondition might not hold on this return path.
-MoreInduction.dfy(92,22): Related location: This is the postcondition that might not hold.
+MoreInduction.dfy(93,0): Error BP5003: A postcondition might not hold on this return path.
+MoreInduction.dfy(92,21): Related location: This is the postcondition that might not hold.
Execution trace:
(0,0): anon0
diff --git a/Test/dafny2/SnapshotableTrees.dfy.expect b/Test/dafny2/SnapshotableTrees.dfy.expect index 849b9e38..808fe0f9 100644 --- a/Test/dafny2/SnapshotableTrees.dfy.expect +++ b/Test/dafny2/SnapshotableTrees.dfy.expect @@ -1,5 +1,5 @@ -SnapshotableTrees.dfy(68,24): Error BP5002: A precondition for this call might not hold.
-SnapshotableTrees.dfy(648,16): Related location: This is the precondition that might not hold.
+SnapshotableTrees.dfy(68,23): Error BP5002: A precondition for this call might not hold.
+SnapshotableTrees.dfy(648,15): Related location: This is the precondition that might not hold.
Execution trace:
(0,0): anon0
(0,0): anon3_Then
diff --git a/Test/dafny4/BinarySearch.dfy.expect b/Test/dafny4/BinarySearch.dfy.expect index 944f677a..a9f834b7 100644 --- a/Test/dafny4/BinarySearch.dfy.expect +++ b/Test/dafny4/BinarySearch.dfy.expect @@ -1,4 +1,4 @@ -BinarySearch.dfy(44,20): Error: result of operation might violate newtype constraint
+BinarySearch.dfy(44,19): Error: result of operation might violate newtype constraint
Execution trace:
(0,0): anon0
BinarySearch.dfy(40,3): anon18_LoopHead
diff --git a/Test/dafny4/Bug73.dfy.expect b/Test/dafny4/Bug73.dfy.expect index 6cf5c156..8beaa18c 100644 --- a/Test/dafny4/Bug73.dfy.expect +++ b/Test/dafny4/Bug73.dfy.expect @@ -1,9 +1,9 @@ -Bug73.dfy(7,14): Error: assertion violation
+Bug73.dfy(7,13): Error: assertion violation
Execution trace:
(0,0): anon0
Bug73.dfy(7,19): anon3_Else
(0,0): anon2
-Bug73.dfy(13,14): Error: assertion violation
+Bug73.dfy(13,13): Error: assertion violation
Execution trace:
(0,0): anon0
Bug73.dfy(13,20): anon3_Else
diff --git a/Test/dafny4/SoftwareFoundations-Basics.dfy.expect b/Test/dafny4/SoftwareFoundations-Basics.dfy.expect index 0f9eb8d0..f07b068f 100644 --- a/Test/dafny4/SoftwareFoundations-Basics.dfy.expect +++ b/Test/dafny4/SoftwareFoundations-Basics.dfy.expect @@ -1,4 +1,4 @@ -SoftwareFoundations-Basics.dfy(41,12): Error: assertion violation
+SoftwareFoundations-Basics.dfy(41,11): Error: assertion violation
Execution trace:
(0,0): anon0
diff --git a/Test/hofs/Apply.dfy.expect b/Test/hofs/Apply.dfy.expect index 77d34c4c..0a923143 100644 --- a/Test/hofs/Apply.dfy.expect +++ b/Test/hofs/Apply.dfy.expect @@ -1,4 +1,4 @@ -Apply.dfy(27,16): Error: assertion violation
+Apply.dfy(27,15): Error: assertion violation
Execution trace:
(0,0): anon0
Apply.dfy(26,27): anon15_Else
diff --git a/Test/hofs/Classes.dfy.expect b/Test/hofs/Classes.dfy.expect index 1c9e31f0..a5b33522 100644 --- a/Test/hofs/Classes.dfy.expect +++ b/Test/hofs/Classes.dfy.expect @@ -1,7 +1,7 @@ -Classes.dfy(64,12): Error: assertion violation
+Classes.dfy(64,11): Error: assertion violation
Execution trace:
(0,0): anon0
-Classes.dfy(40,6): Error: possible violation of function precondition
+Classes.dfy(40,5): Error: possible violation of function precondition
Execution trace:
(0,0): anon0
(0,0): anon7_Else
diff --git a/Test/hofs/Field.dfy.expect b/Test/hofs/Field.dfy.expect index 9f6998f5..0859d83c 100644 --- a/Test/hofs/Field.dfy.expect +++ b/Test/hofs/Field.dfy.expect @@ -1,13 +1,13 @@ -Field.dfy(12,12): Error: possible violation of function precondition
+Field.dfy(12,11): Error: possible violation of function precondition
Execution trace:
(0,0): anon0
-Field.dfy(12,15): Error: assertion violation
+Field.dfy(12,14): Error: assertion violation
Execution trace:
(0,0): anon0
-Field.dfy(21,12): Error: possible violation of function precondition
+Field.dfy(21,11): Error: possible violation of function precondition
Execution trace:
(0,0): anon0
-Field.dfy(21,14): Error: assertion violation
+Field.dfy(21,13): Error: assertion violation
Execution trace:
(0,0): anon0
diff --git a/Test/hofs/FnRef.dfy.expect b/Test/hofs/FnRef.dfy.expect index 0f6f2aa9..e665c830 100644 --- a/Test/hofs/FnRef.dfy.expect +++ b/Test/hofs/FnRef.dfy.expect @@ -1,19 +1,19 @@ -FnRef.dfy(17,45): Error: possible violation of function precondition
+FnRef.dfy(17,44): Error: possible violation of function precondition
Execution trace:
(0,0): anon0
FnRef.dfy(15,12): anon5_Else
(0,0): anon6_Then
-FnRef.dfy(32,8): Error: possible violation of function precondition
+FnRef.dfy(32,7): Error: possible violation of function precondition
Execution trace:
(0,0): anon0
FnRef.dfy(26,12): anon9_Else
FnRef.dfy(28,8): anon10_Else
-FnRef.dfy(46,12): Error: assertion violation
+FnRef.dfy(46,11): Error: assertion violation
Execution trace:
(0,0): anon0
FnRef.dfy(43,12): anon7_Else
(0,0): anon9_Then
-FnRef.dfy(65,14): Error: assertion violation
+FnRef.dfy(65,13): Error: assertion violation
Execution trace:
(0,0): anon0
FnRef.dfy(56,12): anon8_Else
diff --git a/Test/hofs/Frame.dfy.expect b/Test/hofs/Frame.dfy.expect index 0ee2eadb..9964deb4 100644 --- a/Test/hofs/Frame.dfy.expect +++ b/Test/hofs/Frame.dfy.expect @@ -1,35 +1,35 @@ -Frame.dfy(23,16): Error: assertion violation
+Frame.dfy(23,15): Error: assertion violation
Execution trace:
(0,0): anon0
Frame.dfy(19,12): anon5_Else
(0,0): anon6_Then
-Frame.dfy(37,14): Error: assertion violation
+Frame.dfy(37,13): Error: assertion violation
Execution trace:
(0,0): anon0
Frame.dfy(33,12): anon3_Else
-Frame.dfy(63,23): Error: assertion violation
+Frame.dfy(63,22): Error: assertion violation
Execution trace:
(0,0): anon0
(0,0): anon13_Then
Frame.dfy(55,12): anon14_Else
(0,0): anon15_Then
(0,0): anon5
-Frame.dfy(66,19): Error: insufficient reads clause to read array element
+Frame.dfy(66,18): Error: insufficient reads clause to read array element
Execution trace:
(0,0): anon0
(0,0): anon16_Then
(0,0): anon17_Then
-Frame.dfy(68,28): Error: insufficient reads clause to read array element
+Frame.dfy(68,27): Error: insufficient reads clause to read array element
Execution trace:
(0,0): anon0
(0,0): anon16_Else
(0,0): anon18_Then
-Frame.dfy(123,14): Error: possible violation of function precondition
+Frame.dfy(123,13): Error: possible violation of function precondition
Execution trace:
(0,0): anon0
(0,0): anon5_Then
(0,0): anon6_Else
-Frame.dfy(123,19): Error: assertion violation
+Frame.dfy(123,18): Error: assertion violation
Execution trace:
(0,0): anon0
(0,0): anon5_Then
diff --git a/Test/hofs/Lambda.dfy.expect b/Test/hofs/Lambda.dfy.expect index 4fe8275f..ab57fbe0 100644 --- a/Test/hofs/Lambda.dfy.expect +++ b/Test/hofs/Lambda.dfy.expect @@ -1,4 +1,4 @@ -Lambda.dfy(24,12): Error: assertion violation
+Lambda.dfy(24,11): Error: assertion violation
Execution trace:
(0,0): anon0
Lambda.dfy(6,24): anon31_Else
diff --git a/Test/hofs/LambdaParsefail.dfy.expect b/Test/hofs/LambdaParsefail.dfy.expect index 11deb9b0..a72fc978 100644 --- a/Test/hofs/LambdaParsefail.dfy.expect +++ b/Test/hofs/LambdaParsefail.dfy.expect @@ -1,6 +1,6 @@ -LambdaParsefail.dfy(5,19): error: this symbol not expected in VarDeclStatement
-LambdaParsefail.dfy(6,19): error: this symbol not expected in VarDeclStatement
-LambdaParsefail.dfy(7,21): error: this symbol not expected in VarDeclStatement
-LambdaParsefail.dfy(8,15): error: cannot declare identifier beginning with underscore
-LambdaParsefail.dfy(9,17): error: this symbol not expected in VarDeclStatement
+LambdaParsefail.dfy(5,18): Error: this symbol not expected in VarDeclStatement
+LambdaParsefail.dfy(6,18): Error: this symbol not expected in VarDeclStatement
+LambdaParsefail.dfy(7,20): Error: this symbol not expected in VarDeclStatement
+LambdaParsefail.dfy(8,14): Error: cannot declare identifier beginning with underscore
+LambdaParsefail.dfy(9,16): Error: this symbol not expected in VarDeclStatement
5 parse errors detected in LambdaParsefail.dfy
diff --git a/Test/hofs/LambdaParsefail2.dfy.expect b/Test/hofs/LambdaParsefail2.dfy.expect index 0c9ecb83..1a6a65dc 100644 --- a/Test/hofs/LambdaParsefail2.dfy.expect +++ b/Test/hofs/LambdaParsefail2.dfy.expect @@ -1,2 +1,2 @@ -LambdaParsefail2.dfy(6,39): error: invalid LambdaArrow
+LambdaParsefail2.dfy(6,38): Error: invalid LambdaArrow
1 parse errors detected in LambdaParsefail2.dfy
diff --git a/Test/hofs/Naked.dfy.expect b/Test/hofs/Naked.dfy.expect index 514952a1..9794478d 100644 --- a/Test/hofs/Naked.dfy.expect +++ b/Test/hofs/Naked.dfy.expect @@ -1,45 +1,45 @@ -Naked.dfy(9,16): Error: cannot use naked function in recursive setting. Possible solution: eta expansion.
+Naked.dfy(9,15): Error: cannot use naked function in recursive setting. Possible solution: eta expansion.
Execution trace:
(0,0): anon0
(0,0): anon9_Else
(0,0): anon10_Else
(0,0): anon11_Then
-Naked.dfy(12,8): Error: cannot use naked function in recursive setting. Possible solution: eta expansion.
+Naked.dfy(12,7): Error: cannot use naked function in recursive setting. Possible solution: eta expansion.
Execution trace:
(0,0): anon0
(0,0): anon9_Else
(0,0): anon10_Else
(0,0): anon11_Else
-Naked.dfy(17,53): Error: cannot use naked function in recursive setting. Possible solution: eta expansion.
+Naked.dfy(17,52): Error: cannot use naked function in recursive setting. Possible solution: eta expansion.
Execution trace:
(0,0): anon0
(0,0): anon7_Else
(0,0): anon8_Else
-Naked.dfy(22,13): Error: cannot use naked function in recursive setting. Possible solution: eta expansion.
+Naked.dfy(22,12): Error: cannot use naked function in recursive setting. Possible solution: eta expansion.
Execution trace:
(0,0): anon0
-Naked.dfy(26,14): Error: cannot use naked function in recursive setting. Possible solution: eta expansion.
+Naked.dfy(26,13): Error: cannot use naked function in recursive setting. Possible solution: eta expansion.
Execution trace:
(0,0): anon0
-Naked.dfy(30,45): Error: possible violation of function precondition
-Naked.dfy(32,14): Related location
+Naked.dfy(30,44): Error: possible violation of function precondition
+Naked.dfy(32,13): Related location
Execution trace:
(0,0): anon0
(0,0): anon4_Else
-Naked.dfy(32,15): Error: cannot use naked function in recursive setting. Possible solution: eta expansion.
+Naked.dfy(32,14): Error: cannot use naked function in recursive setting. Possible solution: eta expansion.
Execution trace:
(0,0): anon0
-Naked.dfy(38,9): Error: cannot use naked function in recursive setting. Possible solution: eta expansion.
+Naked.dfy(38,8): Error: cannot use naked function in recursive setting. Possible solution: eta expansion.
Execution trace:
(0,0): anon0
-Naked.dfy(42,10): Error: cannot use naked function in recursive setting. Possible solution: eta expansion.
+Naked.dfy(42,9): Error: cannot use naked function in recursive setting. Possible solution: eta expansion.
Execution trace:
(0,0): anon0
-Naked.dfy(45,30): Error: cannot prove termination; try supplying a decreases clause
+Naked.dfy(45,29): Error: cannot prove termination; try supplying a decreases clause
Execution trace:
(0,0): anon0
(0,0): anon4_Else
-Naked.dfy(48,11): Error: cannot use naked function in recursive setting. Possible solution: eta expansion.
+Naked.dfy(48,10): Error: cannot use naked function in recursive setting. Possible solution: eta expansion.
Execution trace:
(0,0): anon0
diff --git a/Test/hofs/OneShot.dfy.expect b/Test/hofs/OneShot.dfy.expect index 91b931b8..0b4a2bb8 100644 --- a/Test/hofs/OneShot.dfy.expect +++ b/Test/hofs/OneShot.dfy.expect @@ -1,16 +1,16 @@ -OneShot.dfy(20,12): Error: possible violation of function precondition
+OneShot.dfy(20,11): Error: possible violation of function precondition
Execution trace:
(0,0): anon0
(0,0): anon5_Then
OneShot.dfy(13,8): anon5_Else
(0,0): anon6_Then
-OneShot.dfy(22,12): Error: assertion violation
+OneShot.dfy(22,11): Error: assertion violation
Execution trace:
(0,0): anon0
(0,0): anon5_Then
OneShot.dfy(13,8): anon5_Else
(0,0): anon6_Else
-OneShot.dfy(22,13): Error: possible violation of function precondition
+OneShot.dfy(22,12): Error: possible violation of function precondition
Execution trace:
(0,0): anon0
(0,0): anon5_Then
diff --git a/Test/hofs/ReadsReads.dfy.expect b/Test/hofs/ReadsReads.dfy.expect index cd013630..0a374c44 100644 --- a/Test/hofs/ReadsReads.dfy.expect +++ b/Test/hofs/ReadsReads.dfy.expect @@ -1,33 +1,33 @@ -ReadsReads.dfy(31,7): Error: insufficient reads clause to invoke function
+ReadsReads.dfy(31,6): Error: insufficient reads clause to invoke function
Execution trace:
(0,0): anon0
(0,0): anon4_Else
-ReadsReads.dfy(36,5): Error: insufficient reads clause to invoke function
+ReadsReads.dfy(36,4): Error: insufficient reads clause to invoke function
Execution trace:
(0,0): anon0
(0,0): anon4_Else
-ReadsReads.dfy(47,12): Error: insufficient reads clause to invoke function
+ReadsReads.dfy(47,11): Error: insufficient reads clause to invoke function
Execution trace:
(0,0): anon0
(0,0): anon4_Else
-ReadsReads.dfy(58,7): Error: insufficient reads clause to invoke function
+ReadsReads.dfy(58,6): Error: insufficient reads clause to invoke function
Execution trace:
(0,0): anon0
(0,0): anon4_Else
-ReadsReads.dfy(87,50): Error: assertion violation
+ReadsReads.dfy(87,49): Error: assertion violation
Execution trace:
(0,0): anon0
(0,0): anon16_Then
-ReadsReads.dfy(89,29): Error: assertion violation
+ReadsReads.dfy(89,28): Error: assertion violation
Execution trace:
(0,0): anon0
(0,0): anon18_Then
-ReadsReads.dfy(99,37): Error: assertion violation
+ReadsReads.dfy(99,36): Error: assertion violation
Execution trace:
(0,0): anon0
ReadsReads.dfy(96,14): anon15_Else
(0,0): anon19_Then
-ReadsReads.dfy(101,29): Error: assertion violation
+ReadsReads.dfy(101,28): Error: assertion violation
Execution trace:
(0,0): anon0
ReadsReads.dfy(96,14): anon15_Else
diff --git a/Test/hofs/Simple.dfy.expect b/Test/hofs/Simple.dfy.expect index e2f16ef3..c0123c80 100644 --- a/Test/hofs/Simple.dfy.expect +++ b/Test/hofs/Simple.dfy.expect @@ -1,26 +1,26 @@ -Simple.dfy(14,10): Error: possible division by zero
+Simple.dfy(14,9): Error: possible division by zero
Execution trace:
(0,0): anon0
(0,0): anon6_Else
(0,0): anon7_Then
-Simple.dfy(27,10): Error: possible division by zero
+Simple.dfy(27,9): Error: possible division by zero
Execution trace:
(0,0): anon0
(0,0): anon6_Else
(0,0): anon7_Then
-Simple.dfy(37,9): Error: possible violation of function precondition
+Simple.dfy(37,8): Error: possible violation of function precondition
Execution trace:
(0,0): anon0
Simple.dfy(35,13): anon5_Else
-Simple.dfy(49,9): Error: possible violation of function precondition
+Simple.dfy(49,8): Error: possible violation of function precondition
Execution trace:
(0,0): anon0
(0,0): anon3_Then
(0,0): anon2
-Simple.dfy(61,10): Error: possible violation of function precondition
+Simple.dfy(61,9): Error: possible violation of function precondition
Execution trace:
(0,0): anon0
-Simple.dfy(73,10): Error: assertion violation
+Simple.dfy(73,9): Error: assertion violation
Execution trace:
(0,0): anon0
Simple.dfy(72,38): anon5_Else
diff --git a/Test/hofs/Twice.dfy.expect b/Test/hofs/Twice.dfy.expect index 2476b945..0ce2450c 100644 --- a/Test/hofs/Twice.dfy.expect +++ b/Test/hofs/Twice.dfy.expect @@ -1,8 +1,8 @@ -Twice.dfy(27,22): Error: assertion violation
+Twice.dfy(27,21): Error: assertion violation
Execution trace:
(0,0): anon0
Twice.dfy(23,12): anon3_Else
-Twice.dfy(35,32): Error: possible violation of function precondition
+Twice.dfy(35,31): Error: possible violation of function precondition
Execution trace:
(0,0): anon0
(0,0): anon10_Else
diff --git a/Test/irondafny0/inheritreqs0.dfy.expect b/Test/irondafny0/inheritreqs0.dfy.expect index eaadc85a..44e33bc0 100644 --- a/Test/irondafny0/inheritreqs0.dfy.expect +++ b/Test/irondafny0/inheritreqs0.dfy.expect @@ -1,5 +1,5 @@ -inheritreqs0.dfy(19,14): Error BP5002: A precondition for this call might not hold.
-inheritreqs0.dfy[Impl](6,18): Related location: This is the precondition that might not hold.
+inheritreqs0.dfy(19,13): Error BP5002: A precondition for this call might not hold.
+inheritreqs0.dfy[Impl](6,17): Related location: This is the precondition that might not hold.
Execution trace:
(0,0): anon0
diff --git a/Test/irondafny0/inheritreqs1.dfy.expect b/Test/irondafny0/inheritreqs1.dfy.expect index 27c76fee..a07d179d 100644 --- a/Test/irondafny0/inheritreqs1.dfy.expect +++ b/Test/irondafny0/inheritreqs1.dfy.expect @@ -1,5 +1,5 @@ -inheritreqs1.dfy(20,14): Error BP5002: A precondition for this call might not hold.
-inheritreqs1.dfy(15,18): Related location: This is the precondition that might not hold.
+inheritreqs1.dfy(20,13): Error BP5002: A precondition for this call might not hold.
+inheritreqs1.dfy(15,17): Related location: This is the precondition that might not hold.
Execution trace:
(0,0): anon0
diff --git a/Test/irondafny0/xrefine1.dfy.expect b/Test/irondafny0/xrefine1.dfy.expect index ae844fc8..ec946cda 100644 --- a/Test/irondafny0/xrefine1.dfy.expect +++ b/Test/irondafny0/xrefine1.dfy.expect @@ -1,5 +1,5 @@ -xrefine1.dfy(71,13): Error BP5002: A precondition for this call might not hold.
-xrefine1.dfy[MainImpl](49,29): Related location: This is the precondition that might not hold.
+xrefine1.dfy(71,12): Error BP5002: A precondition for this call might not hold.
+xrefine1.dfy[MainImpl](49,28): Related location: This is the precondition that might not hold.
Execution trace:
(0,0): anon0
|