diff options
author | Rustan Leino <leino@microsoft.com> | 2011-04-22 17:47:21 -0700 |
---|---|---|
committer | Rustan Leino <leino@microsoft.com> | 2011-04-22 17:47:21 -0700 |
commit | e6609f4aa8c29d32a3b590bf2b4337148a686bf5 (patch) | |
tree | c2b07e66cd30f973085e884a6df907818ae4f6d6 /Test | |
parent | 0b243363d2e1d4cb6118cc7bb87e76b52a954e69 (diff) | |
parent | b0ef6b3fc9c25b22cd490b9df714f3962969c538 (diff) |
Merge with 1038
Diffstat (limited to 'Test')
-rw-r--r-- | Test/test0/Answer | 11 | ||||
-rw-r--r-- | Test/test0/BadLabels1.bpl | 10 |
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;
}
|