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, 49 insertions, 49 deletions

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