From 109e14535e8071b13ec7e4e4f426037fe5f29943 Mon Sep 17 00:00:00 2001
From: Michael Tautschnig <tautschn@amazon.com>
Date: Tue, 9 Dec 2025 11:42:34 +0000
Subject: [PATCH] Add regression test to ascertain struct hack support

When a struct with a C90-style flexible array member (e.g., `char
data[1]`, aka "struct hack") was allocated with extra space using
`malloc(sizeof(struct Foo) + sizeof(char)*2)`, CBMC before 78839a9
incorrectly failed assertions when accessing elements beyond the
declared array size.

Co-authored-by: Kiro autonomous agent

Fixes: #5213
---
 .../cbmc/gh_issue_8617_structhack/main.c      | 28 +++++++++++++++++
 .../cbmc/gh_issue_8617_structhack/test.desc   | 30 +++++++++++++++++++
 2 files changed, 58 insertions(+)
 create mode 100644 regression/cbmc/gh_issue_8617_structhack/main.c
 create mode 100644 regression/cbmc/gh_issue_8617_structhack/test.desc

diff --git a/regression/cbmc/gh_issue_8617_structhack/main.c b/regression/cbmc/gh_issue_8617_structhack/main.c
new file mode 100644
index 00000000000..e986b529d47
--- /dev/null
+++ b/regression/cbmc/gh_issue_8617_structhack/main.c
@@ -0,0 +1,28 @@
+#include <assert.h>
+#include <stdlib.h>
+
+// Reproduction case for struct hack bug reported for CBMC 5.12
+// Bug: When a struct with a flexible array member is allocated with extra
+// space, CBMC incorrectly fails assertions when accessing elements beyond
+// the declared size.
+
+struct Foo
+{
+  int i;
+  char data[1];
+};
+
+int main()
+{
+  struct Foo *foo = malloc(sizeof(struct Foo) + sizeof(char) * 2);
+  assert(foo);
+  foo->data[0] = 'a';
+  assert(foo->data[0] == 'a'); // always succeeds
+  foo->data[1] = 'b';          // set data[1]
+  assert(foo->data[1] == 'b'); // check data[1] -- should succeed
+  foo->data[2] = 'c';          // set data[2]
+  assert(
+    foo->data[1] == 'b'); // check data[1] again - this used to fail in 5.12
+
+  return 0;
+}
diff --git a/regression/cbmc/gh_issue_8617_structhack/test.desc b/regression/cbmc/gh_issue_8617_structhack/test.desc
new file mode 100644
index 00000000000..258bc6aec1f
--- /dev/null
+++ b/regression/cbmc/gh_issue_8617_structhack/test.desc
@@ -0,0 +1,30 @@
+CORE
+main.c
+--no-malloc-may-fail
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring
+--
+Regression test for GitHub issue #8617.
+Exact reproduction of the struct hack bug reported for CBMC 5.12.
+
+In the original bug report, when a struct with a flexible array member
+(char data[1]) was allocated with extra space via
+malloc(sizeof(struct Foo) + sizeof(char)*2), CBMC would incorrectly fail
+the assertion assert(foo->data[1]=='b') after setting foo->data[2]='c'.
+
+This was caused by incorrect handling of byte_extract operations for
+flexible array members. Array operations may fall back to byte_extract
+expressions, and without proper simplification, accesses to dynamically
+allocated extra memory beyond the declared struct size would fail.
+
+Fixed in CBMC 6.7.0 by commit 78839a978c which improved simplification
+of byte_extract operations to handle multiple-of-element size accesses
+to arrays correctly, converting them to index expressions when the offset
+is known to be a multiple of the array-element size.
+
+Note: C90 did not have flexible arrays, and using arrays of size 1 was
+common practice (the "struct hack"). While this is technically undefined
+behavior in C99+, CBMC now handles this pattern correctly.