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

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/labels1/main.c

@@ -24,8 +24,9 @@ int main()
     x = 42;
 label_four:
   assert(foo() == 1);
+  fptr_t fp;
 label_five:
-  fptr_t fp = foo;
+  fp = foo;
   assert(fp() == 1);
 label_six:
   return *p;

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
@@ -293,7 +294,8 @@ grammar:
 /*** Token with values **************************************************/
 
 identifier:
-          TOK_IDENTIFIER
+          TOK_GCC_IDENTIFIER
+        | TOK_MSC_IDENTIFIER
         | TOK_CPROVER_ID TOK_STRING
         {
           // construct an identifier from a string that would otherwise not be a
@@ -1362,7 +1364,7 @@ atomic_type_specifier:
         ;
 
 msc_decl_identifier:
-          TOK_IDENTIFIER
+          TOK_MSC_IDENTIFIER
         {
           parser_stack($$).id(parser_stack($$).get(ID_identifier));
         }
@@ -2285,9 +2287,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
@@ -2297,7 +2304,6 @@ statement:
         | msc_asm_statement
         | msc_seh_statement
         | cprover_exception_statement
-        | statement_attribute
         ;
 
 declaration_statement:
@@ -2309,8 +2315,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);

src/ansi-c/scanner.l

@@ -86,7 +86,8 @@ int make_identifier()
   {
     parser_stack(yyansi_clval).id(ID_symbol);
     parser_stack(yyansi_clval).set(ID_C_base_name, final_base_name);
-    return TOK_IDENTIFIER;
+    return PARSER.mode == configt::ansi_ct::flavourt::VISUAL_STUDIO ?
+      TOK_MSC_IDENTIFIER : TOK_GCC_IDENTIFIER;
   }
   else
   {
@@ -112,7 +113,8 @@ int make_identifier()
     else
     {
       parser_stack(yyansi_clval).id(ID_symbol);
-      return TOK_IDENTIFIER;
+      return PARSER.mode == configt::ansi_ct::flavourt::VISUAL_STUDIO ?
+        TOK_MSC_IDENTIFIER : TOK_GCC_IDENTIFIER;
     }
   }
 }