Merge pull request #3277 from tautschnig/nested-labels

C front-end: cleanup label statement type checking

Author: tautschnig

regression/cbmc/nested_label1/main.c

@@ -0,0 +1,13 @@
+#include <assert.h>
+
+int main()
+{
+  goto label2;
+  goto out;
+label1:
+label2:
+label3:
+  assert(0);
+out:
+  return 0;
+}

regression/cbmc/nested_label1/test.desc

@@ -0,0 +1,12 @@
+CORE
+main.c
+
+^EXIT=10$
+^SIGNAL=0$
+^VERIFICATION FAILED$
+--
+^warning: ignoring
+--
+This test checks that the assertion is reachable despite being wrapped in a
+nested list of labels, and that jumping to a label in the middle of that list is
+handled correctly.

scripts/delete_failing_smt2_solver_tests

@@ -262,6 +262,7 @@ rm memory_allocation1/test.desc
 rm memset1/test.desc
 rm memset3/test.desc
 rm mm_io1/test.desc
+rm nested_label1/test.desc
 rm no_nondet_static/test.desc
 rm null1/test.desc
 rm null2/test.desc

src/ansi-c/c_typecheck_code.cpp

@@ -193,26 +193,8 @@ void c_typecheck_baset::typecheck_block(code_blockt &code)
 
   for(auto &code_op : code.statements())
   {
-    if(code_op.is_nil())
-      continue;
-
-    if(code_op.get_statement()==ID_label)
-    {
-      // these may be nested
-      codet *code_ptr=&code_op;
-
-      while(code_ptr->get_statement()==ID_label)
-      {
-        assert(code_ptr->operands().size()==1);
-        code_ptr=&to_code(code_ptr->op0());
-      }
-
-      // codet &label_op=*code_ptr;
-
-      new_ops.move(code_op);
-    }
-    else
-      new_ops.move(code_op);
+    if(code_op.is_not_nil())
+      new_ops.add(std::move(code_op));
   }
 
   code.statements().swap(new_ops.statements());