Merge pull request diffblue#2222 from tautschnig/attributes

C front-end: fallthrough attribute, variable aliases

Author: Daniel Kroening

regression/ansi-c/gcc_attributes12/main.c

@@ -0,0 +1,9 @@
+static const int my_ids[] = { 1, 2, 3, 4 };
+
+#ifdef __GNUC__
+extern typeof(my_ids) my_ids_table __attribute__((alias("my_ids")));
+#endif
+
+int main()
+{
+}

regression/ansi-c/gcc_attributes12/test.desc

@@ -0,0 +1,8 @@
+CORE
+main.c
+
+^EXIT=0$
+^SIGNAL=0$
+--
+^warning: ignoring
+^CONVERSION ERROR$

regression/ansi-c/gcc_attributes13/main.c

@@ -0,0 +1,20 @@
+// GCC statement attributes -- currently "fallthrough" is the only one that GCC
+// supports.
+// https://gcc.gnu.org/onlinedocs/gcc/Statement-Attributes.html
+
+int main()
+{
+  int x;
+  switch(x)
+  {
+    case 1:
+      x = 2;
+#ifdef __GNUC__
+      __attribute__((fallthrough));
+#endif
+    case 2:
+      x = 3;
+  }
+
+  return 0;
+}

regression/ansi-c/gcc_attributes13/test.desc

@@ -0,0 +1,8 @@
+CORE
+main.c
+
+^EXIT=0$
+^SIGNAL=0$
+--
+^warning: ignoring
+^CONVERSION ERROR$

src/ansi-c/c_typecheck_base.cpp

@@ -152,7 +152,7 @@ void c_typecheck_baset::typecheck_new_symbol(symbolt &symbol)
         it->set_identifier(irep_idt());
     }
   }
-  else
+  else if(!symbol.is_macro)
   {
     // check the initializer
     do_initializer(symbol);

src/ansi-c/parser.y

@@ -148,6 +148,7 @@ extern char *yyansi_ctext;
 %token TOK_GCC_ATTRIBUTE_NORETURN "noreturn"
 %token TOK_GCC_ATTRIBUTE_CONSTRUCTOR "constructor"
 %token TOK_GCC_ATTRIBUTE_DESTRUCTOR "destructor"
+%token TOK_GCC_ATTRIBUTE_FALLTHROUGH "fallthrough"
 %token TOK_GCC_LABEL   "__label__"
 %token TOK_MSC_ASM     "__asm"
 %token TOK_MSC_BASED   "__based"
@@ -2156,6 +2157,7 @@ statement:
         | msc_asm_statement
         | msc_seh_statement
         | cprover_exception_statement
+        | statement_attribute
         ;
 
 declaration_statement:
@@ -2214,6 +2216,14 @@ labeled_statement:
         }
         ;
 
+statement_attribute:
+          TOK_GCC_ATTRIBUTE '(' '(' TOK_GCC_ATTRIBUTE_FALLTHROUGH ')' ')' ';' labeled_statement
+        {
+          // attribute ignored
+          $$=$8;
+        }
+        ;
+
 compound_statement:
           compound_scope '{' '}'
         {

src/ansi-c/scanner.l

@@ -1580,6 +1580,8 @@ __decltype          { if(PARSER.cpp98 &&
 "destructor" |
 "__destructor__"   { BEGIN(GCC_ATTRIBUTE3); loc(); return TOK_GCC_ATTRIBUTE_DESTRUCTOR; }
 
+"fallthrough"       { BEGIN(GCC_ATTRIBUTE3); loc(); return TOK_GCC_ATTRIBUTE_FALLTHROUGH; }
+
 {ws}                { /* ignore */ }
 {newline}           { /* ignore */ }
 {identifier}        { BEGIN(GCC_ATTRIBUTE4); }