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.

13 files changed, 56 insertions, 56 deletions

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