Changed label checking for goto targets in StmtList so that they can be any label in the current implementation.

1 files changed, 5 insertions, 5 deletions

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;  

 }