summaryrefslogtreecommitdiff
path: root/Test
diff options
context:
space:
mode:
authorGravatar Rustan Leino <leino@microsoft.com>2011-04-22 17:47:21 -0700
committerGravatar Rustan Leino <leino@microsoft.com>2011-04-22 17:47:21 -0700
commite6609f4aa8c29d32a3b590bf2b4337148a686bf5 (patch)
treec2b07e66cd30f973085e884a6df907818ae4f6d6 /Test
parent0b243363d2e1d4cb6118cc7bb87e76b52a954e69 (diff)
parentb0ef6b3fc9c25b22cd490b9df714f3962969c538 (diff)
Merge with 1038
Diffstat (limited to 'Test')
-rw-r--r--Test/test0/Answer11
-rw-r--r--Test/test0/BadLabels1.bpl10
2 files changed, 8 insertions, 13 deletions
diff --git a/Test/test0/Answer b/Test/test0/Answer
index 9e60f623..0441b69b 100644
--- a/Test/test0/Answer
+++ b/Test/test0/Answer
@@ -109,20 +109,15 @@ WhereResolution.bpl(32,30): Error: old expressions allowed only in two-state con
BadLabels0.bpl(4,2): Error: more than one declaration of block name: X
BadLabels0.bpl(11,4): Error: more than one declaration of block name: Y
2 name resolution errors detected in BadLabels0.bpl
-BadLabels1.bpl(4,3): error: Error: goto label 'X' is undefined or out of reach
-BadLabels1.bpl(5,3): error: Error: goto label 'Y' is undefined or out of reach
-BadLabels1.bpl(10,3): error: Error: goto label 'X' is undefined or out of reach
-BadLabels1.bpl(24,5): error: Error: goto label 'K' is undefined or out of reach
-BadLabels1.bpl(30,5): error: Error: goto label 'A' is undefined or out of reach
-BadLabels1.bpl(38,7): error: Error: goto label 'M' is undefined or out of reach
-BadLabels1.bpl(41,3): error: Error: goto label 'B' is undefined or out of reach
+BadLabels1.bpl(4,3): error: Error: goto label 'X' is undefined
+BadLabels1.bpl(5,3): error: Error: goto label 'Y' is undefined
BadLabels1.bpl(47,3): error: Error: break statement is not inside a loop
BadLabels1.bpl(49,5): error: Error: break statement is not inside a loop
BadLabels1.bpl(60,5): error: Error: break label 'B' must designate an enclosing statement
BadLabels1.bpl(63,5): error: Error: break label 'A' must designate an enclosing statement
BadLabels1.bpl(64,5): error: Error: break label 'C' must designate an enclosing statement
BadLabels1.bpl(65,8): error: Error: break label 'F' must designate an enclosing statement
-13 parse errors detected in BadLabels1.bpl
+8 parse errors detected in BadLabels1.bpl
LineParse.bpl(1,0): error: Malformed (#line num [filename]) pragma: #line
LineParse.bpl(2,0): error: Malformed (#line num [filename]) pragma: #line
LineParse.bpl(1,0): error: Unrecognized pragma: #dontknow what this is No, I don't well, it's an error is what it is
diff --git a/Test/test0/BadLabels1.bpl b/Test/test0/BadLabels1.bpl
index b4bb6948..28fb47b8 100644
--- a/Test/test0/BadLabels1.bpl
+++ b/Test/test0/BadLabels1.bpl
@@ -7,7 +7,7 @@ procedure P0()
procedure P1(y: int)
{
- goto X; // error: label out of reach
+ goto X;
while (y < 100)
{
X:
@@ -21,13 +21,13 @@ procedure P1(y: int)
B:
} else {
C:
- goto K; // error: label out of reach
+ goto K;
}
while (y < 1000)
{
K:
- goto A; // error: label out of reach
+ goto A;
if (y % 2 == 0) {
goto L;
M:
@@ -35,10 +35,10 @@ procedure P1(y: int)
goto K, L;
L:
if (*) {
- goto M; // error: label out of reach
+ goto M;
}
}
- goto B; // error: label out of reach
+ goto B;
}