C front-end: labelled declarations are only supported by Visual Studio

In order to support GCC's label attributes even when the semicolon is
omitted, distinguish GCC and Visual Studio modes when parsing labelled
statements. See
https://github.com/gcc-mirror/gcc/blob/master/gcc/c/c-parser.c#L5553 for
GCC's limitation, which we now mimic. (We already supported attributes
followed by a semicolon, which GCC's documentation mandates, but the
Linux kernel doesn't always follow this rule.) Fixed regression tests
that had declarations immediately following a label.

Author: tautschnig

regression/ansi-c/label1/main.c

@@ -0,0 +1,14 @@
+extern void foo(int *, unsigned int);
+
+int main()
+{
+#ifdef _MSC_VER
+label:
+  int x;
+#elif defined(__GNUC__)
+  int *p;
+  unsigned int u;
+label:
+  __attribute__((unused)) foo(p, u);
+#endif
+}

regression/ansi-c/label1/test.desc

@@ -0,0 +1,15 @@
+CORE
+main.c
+
+^EXIT=0$
+^SIGNAL=0$
+--
+^warning: ignoring
+^CONVERSION ERROR$
+--
+GCC does not permit labelling declarations as they are not considered
+statements, and would result in ambiguity in case of label attributes. We used
+to run into this problem, treating the function call in this test as a KnR
+function declaration.
+
+Visual Studio, on the other hand, happily accepts labelled declarations.

regression/cbmc/destructors/main.c

@@ -6,7 +6,7 @@ int main(int argc, char **argv) {
 
   const float *pc = (const float []){1e0, 1e1, 1e2};
 
-start:
+start:;
   test newAlloc0 = {0};
   if(argv[0])
   {
@@ -20,7 +20,7 @@ int main(int argc, char **argv) {
     if (argv[2])
     {
       test newAlloc3 = {3};
-nested_if:
+    nested_if:;
       test newAlloc5 = {5};
       if (argv[3])
       {

regression/cbmc/symex_should_exclude_null_pointers/main.c

@@ -38,15 +38,15 @@ int main(int argc, char **argv) {
   int *ptr4 = maybe_null;
   goto check;
 
-deref:
+deref:;
   int deref4 = *ptr4;
   goto end_test4;
 
 check:
   __CPROVER_assume(ptr4 != 0);
   goto deref;
 
-end_test4:
+end_test4:;
 
   // Should be judged unsafe by LSPA and safe by value-set filtering
   // (guarded by confluence):

regression/cbmc/symex_should_filter_value_sets/main.c

@@ -61,28 +61,28 @@ int main(int argc, char **argv)
   int *p7 = ptr_to_a_or_b;
   goto check7;
 
-divide7:
+divide7:;
   int c7 = *p7;
   goto end_test7;
 
 check7:
   __CPROVER_assume(p7 != &a);
   goto divide7;
 
-end_test7:
+end_test7:;
 
   int *p8 = ptr_to_a_or_b;
   goto check8;
 
-divide8:
+divide8:;
   int c8 = *p8;
   goto end_test8;
 
 check8:
   __CPROVER_assume(*p8 != 2);
   goto divide8;
 
-end_test8:
+end_test8:;
 
   // Should work (value-set filtered by confluence of if and else):
   int *p9 = ptr_to_a_or_b;

regression/cbmc/unwind_counters2/main.c

@@ -1,8 +1,9 @@
 int main()
 {
   l2: goto l1;
-  l1: int x=5;
-  goto l2;
+  l1:;
+    int x = 5;
+    goto l2;
 
-  return 0;
+    return 0;
 }

regression/cbmc/unwind_counters3/main.c

@@ -2,8 +2,9 @@ int main()
 {
   int i=0;
   l2: if(i==1) int y=0;
-  l1: int x=5;
-  goto l2;
+  l1:;
+    int x = 5;
+    goto l2;
 
-  return 0;
+    return 0;
 }

regression/cbmc/unwind_counters4/main.c

@@ -8,7 +8,7 @@ int main()
     y = 10;
     goto label;
     x = 1; // dead code, makes sure the above goto is not removed
-  label:
+  label: ;
     _Bool nondet;
     if(nondet)
       __CPROVER_assert(y != 10, "violated via first loop");

regression/goto-instrument/safe-dereferences/main.c

@@ -30,15 +30,15 @@ int main(int argc, char **argv) {
   int *ptr4 = &x;
   goto check;
 
-deref:
+deref:;
   int deref4 = *ptr4;
   goto end_test4;
 
 check:
   __CPROVER_assume(ptr4 != 0);
   goto deref;
 
-end_test4:
+end_test4:;
 
   // Shouldn't work yet despite being safe (guarded by confluence):
   int *ptr5 = &x;

src/ansi-c/parser.y

@@ -118,7 +118,8 @@ extern char *yyansi_ctext;
 
 /*** scanner parsed tokens (these have a value!) ***/
 
-%token TOK_IDENTIFIER
+%token TOK_GCC_IDENTIFIER
+%token TOK_MSC_IDENTIFIER
 %token TOK_TYPEDEFNAME
 %token TOK_INTEGER
 %token TOK_FLOATING
@@ -291,7 +292,8 @@ grammar:
 /*** Token with values **************************************************/
 
 identifier:
-          TOK_IDENTIFIER
+          TOK_GCC_IDENTIFIER
+        | TOK_MSC_IDENTIFIER
         | TOK_CPROVER_ID TOK_STRING
         {
           $$=$1;
@@ -1377,7 +1379,7 @@ atomic_type_specifier:
         ;
 
 msc_decl_identifier:
-          TOK_IDENTIFIER
+          TOK_MSC_IDENTIFIER
         {
           parser_stack($$).id(parser_stack($$).get(ID_identifier));
         }
@@ -2300,9 +2302,14 @@ designator:
 /*** Statements *********************************************************/
 
 statement:
+          declaration_statement
+        | statement_attribute
+        | stmt_not_decl_or_attr
+        ;
+
+stmt_not_decl_or_attr:
           labeled_statement
         | compound_statement
-        | declaration_statement
         | expression_statement
         | selection_statement
         | iteration_statement
@@ -2312,7 +2319,6 @@ statement:
         | msc_asm_statement
         | msc_seh_statement
         | cprover_exception_statement
-        | statement_attribute
         ;
 
 declaration_statement:
@@ -2324,8 +2330,30 @@ declaration_statement:
         }
         ;
 
+gcc_attribute_specifier_opt:
+          /* empty */
+        {
+          init($$);
+        }
+        | gcc_attribute_specifier
+        ;
+
+msc_label_identifier:
+          TOK_MSC_IDENTIFIER
+        | TOK_TYPEDEFNAME
+        ;
+
 labeled_statement:
-        identifier_or_typedef_name ':' statement
+          TOK_GCC_IDENTIFIER ':' gcc_attribute_specifier_opt stmt_not_decl_or_attr
+        {
+          // we ignore the GCC attribute
+          $$=$2;
+          statement($$, ID_label);
+          irep_idt identifier=PARSER.lookup_label(parser_stack($1).get(ID_C_base_name));
+          parser_stack($$).set(ID_label, identifier);
+          mto($$, $4);
+        }
+        | msc_label_identifier ':' statement
         {
           $$=$2;
           statement($$, ID_label);