summaryrefslogtreecommitdiff
path: root/Test/dafny0/ControlStructures.dfy.expect
diff options
context:
space:
mode:
authorGravatar Clément Pit--Claudel <clement.pitclaudel@live.com>2015-07-23 11:57:19 -0700
committerGravatar Clément Pit--Claudel <clement.pitclaudel@live.com>2015-07-23 11:57:19 -0700
commit3f886d1789d50400ffba2befdc2ae0e8d5c79cbe (patch)
tree70b54a2e8b21c82dbd06ed46c716a281dc8efa26 /Test/dafny0/ControlStructures.dfy.expect
parent1763ad8e4d6b631fe966b394ae2dbafa7d803627 (diff)
Fix: Unify column numbers in Dafny's errors
Dafny counts from 0, but Boogie counts from 1. Tokens are 1-based. Thus when we print tokens, we need to decrement the column number. This was done for resolver errors, but not for verification or parsing errors. In addition, parsing errors were inconsistent with resolution errors case-wise. Unfortunately, the fix affects the output of many tests.
Diffstat (limited to 'Test/dafny0/ControlStructures.dfy.expect')
-rw-r--r--Test/dafny0/ControlStructures.dfy.expect20
1 files changed, 10 insertions, 10 deletions
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