From d6d0a49b203b463166186186e848fdb726fea6df Mon Sep 17 00:00:00 2001
From: Michael Tautschnig <tautschn@amazon.com>
Date: Tue, 22 May 2018 12:38:38 +0000
Subject: [PATCH 1/2] C front-end: support alias attributes on variables

GCC only documents those for functions, but the Linux kernel code uses aliases
when building kernel modules. These result from the expansion of the following
macro defined in mdoule.h:

 #define MODULE_DEVICE_TABLE(type, name)         \
 extern typeof(name) __mod_##type##__##name##_device_table   \
   __attribute__ ((unused, alias(__stringify(name))))
---
 regression/ansi-c/gcc_attributes12/main.c    | 9 +++++++++
 regression/ansi-c/gcc_attributes12/test.desc | 8 ++++++++
 src/ansi-c/c_typecheck_base.cpp              | 2 +-
 3 files changed, 18 insertions(+), 1 deletion(-)
 create mode 100644 regression/ansi-c/gcc_attributes12/main.c
 create mode 100644 regression/ansi-c/gcc_attributes12/test.desc

diff --git a/regression/ansi-c/gcc_attributes12/main.c b/regression/ansi-c/gcc_attributes12/main.c
new file mode 100644
index 00000000000..34b9bbbcc98
--- /dev/null
+++ b/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()
+{
+}
diff --git a/regression/ansi-c/gcc_attributes12/test.desc b/regression/ansi-c/gcc_attributes12/test.desc
new file mode 100644
index 00000000000..466da18b2b5
--- /dev/null
+++ b/regression/ansi-c/gcc_attributes12/test.desc
@@ -0,0 +1,8 @@
+CORE
+main.c
+
+^EXIT=0$
+^SIGNAL=0$
+--
+^warning: ignoring
+^CONVERSION ERROR$
diff --git a/src/ansi-c/c_typecheck_base.cpp b/src/ansi-c/c_typecheck_base.cpp
index 890815fcc86..fc8fc87c9b1 100644
--- a/src/ansi-c/c_typecheck_base.cpp
+++ b/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);

From e1b906ae4c4ebdc2f62878981ea16bee31e9fdb2 Mon Sep 17 00:00:00 2001
From: Michael Tautschnig <tautschn@amazon.com>
Date: Tue, 22 May 2018 12:41:28 +0000
Subject: [PATCH 2/2] Support GCC's fallthrough attribute

---
 regression/ansi-c/gcc_attributes13/main.c    | 20 ++++++++++++++++++++
 regression/ansi-c/gcc_attributes13/test.desc |  8 ++++++++
 src/ansi-c/parser.y                          | 10 ++++++++++
 src/ansi-c/scanner.l                         |  2 ++
 4 files changed, 40 insertions(+)
 create mode 100644 regression/ansi-c/gcc_attributes13/main.c
 create mode 100644 regression/ansi-c/gcc_attributes13/test.desc

diff --git a/regression/ansi-c/gcc_attributes13/main.c b/regression/ansi-c/gcc_attributes13/main.c
new file mode 100644
index 00000000000..64230094d9d
--- /dev/null
+++ b/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;
+}
diff --git a/regression/ansi-c/gcc_attributes13/test.desc b/regression/ansi-c/gcc_attributes13/test.desc
new file mode 100644
index 00000000000..466da18b2b5
--- /dev/null
+++ b/regression/ansi-c/gcc_attributes13/test.desc
@@ -0,0 +1,8 @@
+CORE
+main.c
+
+^EXIT=0$
+^SIGNAL=0$
+--
+^warning: ignoring
+^CONVERSION ERROR$
diff --git a/src/ansi-c/parser.y b/src/ansi-c/parser.y
index 7f590e90e2d..a6612f2337c 100644
--- a/src/ansi-c/parser.y
+++ b/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 '{' '}'
         {
diff --git a/src/ansi-c/scanner.l b/src/ansi-c/scanner.l
index 9151ea2263f..45508450351 100644
--- a/src/ansi-c/scanner.l
+++ b/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); }