diff options
Diffstat (limited to 'Test/test0/BadLabels1.bpl')
-rw-r--r-- | Test/test0/BadLabels1.bpl | 166 |
1 files changed, 83 insertions, 83 deletions
diff --git a/Test/test0/BadLabels1.bpl b/Test/test0/BadLabels1.bpl index d0b4e396..dca59b57 100644 --- a/Test/test0/BadLabels1.bpl +++ b/Test/test0/BadLabels1.bpl @@ -1,83 +1,83 @@ -// RUN: %boogie -noVerify "%s" > "%t"
-// RUN: %diff "%s.expect" "%t"
-procedure P0()
-{
- // these labels don't exist at all
- goto X; // error: undefined label
- goto Y; // error: undefined label
-}
-
-procedure P1(y: int)
-{
- goto X;
- while (y < 100)
- {
- X:
- }
-
- Q:
- if (y == 102) {
- A:
- goto Q;
- } else if (y == 104) {
- B:
- } else {
- C:
- goto K;
- }
-
- while (y < 1000)
- {
- K:
- goto A;
- if (y mod 2 == 0) {
- goto L;
- M:
- }
- goto K, L;
- L:
- if (*) {
- goto M;
- }
- }
- goto B;
-}
-
-
-procedure Break(n: int)
-{
- break; // error: break not inside a loop
- if (*) {
- break; // error: label-less break not inside a loop
- }
-
- A:
- if (*) {
- break A; // this is fine, since the break statement uses a label
- }
-
- B:
- assert 2 <= n;
- while (*) {
- break B; // error: B does not label a loop
- break;
- C: while (*) { assert n < 100; }
- break A; // error: A does not label a loop
- break C; // error: A does not label an enclosing loop
- F: break F; // error: F does not label an enclosing loop
- }
-
- D:
- while (*) {
- E:
- while (*) {
- if (*) {
- break;
- } else if (*) {
- if (*) { break E; }
- } else {
- break D;
- }
- }
- }
-}
+// RUN: %boogie -noVerify "%s" > "%t" +// RUN: %diff "%s.expect" "%t" +procedure P0() +{ + // these labels don't exist at all + goto X; // error: undefined label + goto Y; // error: undefined label +} + +procedure P1(y: int) +{ + goto X; + while (y < 100) + { + X: + } + + Q: + if (y == 102) { + A: + goto Q; + } else if (y == 104) { + B: + } else { + C: + goto K; + } + + while (y < 1000) + { + K: + goto A; + if (y mod 2 == 0) { + goto L; + M: + } + goto K, L; + L: + if (*) { + goto M; + } + } + goto B; +} + + +procedure Break(n: int) +{ + break; // error: break not inside a loop + if (*) { + break; // error: label-less break not inside a loop + } + + A: + if (*) { + break A; // this is fine, since the break statement uses a label + } + + B: + assert 2 <= n; + while (*) { + break B; // error: B does not label a loop + break; + C: while (*) { assert n < 100; } + break A; // error: A does not label a loop + break C; // error: A does not label an enclosing loop + F: break F; // error: F does not label an enclosing loop + } + + D: + while (*) { + E: + while (*) { + if (*) { + break; + } else if (*) { + if (*) { break E; } + } else { + break D; + } + } + } +} |