From 72f5736edb31585e33ededdd78d0eda71014fea7 Mon Sep 17 00:00:00 2001
From: Michael Tautschnig <tautschn@amazon.com>
Date: Wed, 16 Dec 2020 12:43:01 +0000
Subject: [PATCH] dump-c: when removing const-ness, also handle bit fields

We need to remove the const qualifier when the assignment is no longer
performed as part of the declaration. This worked for various types
already, but bit fields had not been considered.
---
 regression/goto-instrument/chain.sh           |  1 +
 .../goto-instrument/dump-decl-const/main.c    | 19 +++++++++++++++++++
 .../goto-instrument/dump-decl-const/test.desc | 16 ++++++++++++++++
 src/goto-instrument/goto_program2code.cpp     |  2 ++
 4 files changed, 38 insertions(+)
 create mode 100644 regression/goto-instrument/dump-decl-const/main.c
 create mode 100644 regression/goto-instrument/dump-decl-const/test.desc

diff --git a/regression/goto-instrument/chain.sh b/regression/goto-instrument/chain.sh
index cf2ed387c29..f10968f5162 100755
--- a/regression/goto-instrument/chain.sh
+++ b/regression/goto-instrument/chain.sh
@@ -38,6 +38,7 @@ elif echo $args | grep -q -- "--dump-c-type-header" ; then
   cat "${name}-mod.gb"
   mv "${name}.gb" "${name}-mod.gb"
 elif echo $args | grep -q -- "--dump-c" ; then
+  cat "${name}-mod.gb"
   mv "${name}-mod.gb" "${name}-mod.c"
 
   if [[ "${is_windows}" == "true" ]]; then
diff --git a/regression/goto-instrument/dump-decl-const/main.c b/regression/goto-instrument/dump-decl-const/main.c
new file mode 100644
index 00000000000..d00bc5d0c14
--- /dev/null
+++ b/regression/goto-instrument/dump-decl-const/main.c
@@ -0,0 +1,19 @@
+#include <assert.h>
+
+struct S
+{
+  const int x;
+  const int y : 8;
+  const int *const p;
+};
+
+int foo()
+{
+  return 1;
+}
+
+int main()
+{
+  struct S s1 = {foo(), 1, 0};
+  assert(s1.x == 1);
+}
diff --git a/regression/goto-instrument/dump-decl-const/test.desc b/regression/goto-instrument/dump-decl-const/test.desc
new file mode 100644
index 00000000000..d8746604d8d
--- /dev/null
+++ b/regression/goto-instrument/dump-decl-const/test.desc
@@ -0,0 +1,16 @@
+CORE
+main.c
+--dump-c
+signed int x
+signed int y
+const signed int \*p
+^[[:space:]]*s1 = \(struct S\)\{ .* \};
+^EXIT=0$
+^SIGNAL=0$
+--
+const signed int x
+const signed int y
+const p
+--
+This test demonstrates that the constness of struct members has been removed,
+which is necessary as the initialisation is not performed in the declaration.
diff --git a/src/goto-instrument/goto_program2code.cpp b/src/goto-instrument/goto_program2code.cpp
index f8c69289dae..a48a8cb0e6f 100644
--- a/src/goto-instrument/goto_program2code.cpp
+++ b/src/goto-instrument/goto_program2code.cpp
@@ -1591,6 +1591,8 @@ void goto_program2codet::remove_const(typet &type)
         ++it)
       remove_const(it->type());
   }
+  else if(type.id() == ID_c_bit_field)
+    to_c_bit_field_type(type).subtype().remove(ID_C_constant);
 }
 
 static bool has_labels(const codet &code)