Merge pull request #8801 from tautschnig/fix-5213-structhack

Add regression test to ascertain struct hack support

Author: tautschnig

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;
+}

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.