diff options
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
|