Fix: Unify column numbers in Dafny's errors

Dafny counts from 0, but Boogie counts from 1. Tokens are 1-based. Thus when we
print tokens, we need to decrement the column number. This was done for resolver
errors, but not for verification or parsing errors. In addition, parsing errors
were inconsistent with resolution errors case-wise.

Unfortunately, the fix affects the output of many tests.

1 files changed, 23 insertions, 23 deletions

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