From 186f49b4a66f1dc2e2554923016cab5e3f305253 Mon Sep 17 00:00:00 2001
From: Michael Tautschnig <tautschn@amazon.com>
Date: Thu, 28 Apr 2016 14:13:03 +0000
Subject: [PATCH] Maintain alignment annotation when extracting from
 already-typechecked

---
 regression/ansi-c/gcc_attributes8/main.c    | 23 +++++++++++++++++++++
 regression/ansi-c/gcc_attributes8/test.desc |  8 +++++++
 src/ansi-c/c_typecheck_type.cpp             |  5 +++++
 3 files changed, 36 insertions(+)
 create mode 100644 regression/ansi-c/gcc_attributes8/main.c
 create mode 100644 regression/ansi-c/gcc_attributes8/test.desc

diff --git a/regression/ansi-c/gcc_attributes8/main.c b/regression/ansi-c/gcc_attributes8/main.c
new file mode 100644
index 00000000000..7cb7a0964a1
--- /dev/null
+++ b/regression/ansi-c/gcc_attributes8/main.c
@@ -0,0 +1,23 @@
+#define STATIC_ASSERT(condition) \
+  int some_array[(condition) ? 1 : -1];
+
+#ifdef __GNUC__
+
+struct s
+{
+  char x;
+
+  // struct-typed member with alignment
+  struct inner
+  {
+    int a;
+  } inner __attribute__((aligned(64)));
+};
+
+STATIC_ASSERT(sizeof(struct s)==128);
+
+#endif
+
+int main()
+{
+}
diff --git a/regression/ansi-c/gcc_attributes8/test.desc b/regression/ansi-c/gcc_attributes8/test.desc
new file mode 100644
index 00000000000..466da18b2b5
--- /dev/null
+++ b/regression/ansi-c/gcc_attributes8/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_type.cpp b/src/ansi-c/c_typecheck_type.cpp
index f1420925c99..7890b2a1c8d 100644
--- a/src/ansi-c/c_typecheck_type.cpp
+++ b/src/ansi-c/c_typecheck_type.cpp
@@ -51,9 +51,14 @@ void c_typecheck_baset::typecheck_type(typet &type)
     c_qualifierst c_qualifiers(type);
     c_qualifiers+=c_qualifierst(type.subtype());
     bool packed=type.get_bool(ID_C_packed);
+    exprt alignment=static_cast<const exprt &>(type.find(ID_C_alignment));
+
     type.swap(type.subtype());
+
     c_qualifiers.write(type);
     if(packed) type.set(ID_C_packed, true);
+    if(alignment.is_not_nil()) type.add(ID_C_alignment, alignment);
+
     return; // done
   }