From 22e60dcf969a26c8d7c6f94ec2d7b36bf768f2b7 Mon Sep 17 00:00:00 2001
From: martin <martin@michael>
Date: Wed, 21 Jul 2021 21:45:37 +0100
Subject: [PATCH] A simplified example that triggers issue 6230, from
 @SaswatPadhi

---
 regression/cbmc/array-bug-6230/main.c    | 19 +++++++++++++++++++
 regression/cbmc/array-bug-6230/test.desc |  8 ++++++++
 2 files changed, 27 insertions(+)
 create mode 100644 regression/cbmc/array-bug-6230/main.c
 create mode 100644 regression/cbmc/array-bug-6230/test.desc

diff --git a/regression/cbmc/array-bug-6230/main.c b/regression/cbmc/array-bug-6230/main.c
new file mode 100644
index 00000000000..5dc539954b7
--- /dev/null
+++ b/regression/cbmc/array-bug-6230/main.c
@@ -0,0 +1,19 @@
+#include <stdint.h>
+#include <stdlib.h>
+
+struct inner
+{
+  uint32_t exts[32]; // 32 is the minimum to crash
+};
+
+struct outer
+{
+  struct inner ctx; // Nesting is necessary
+};
+
+int main()
+{
+  struct outer *s = malloc(sizeof(struct outer));
+  if(s != NULL)
+    s->ctx.exts[0] = 0;
+}
diff --git a/regression/cbmc/array-bug-6230/test.desc b/regression/cbmc/array-bug-6230/test.desc
new file mode 100644
index 00000000000..dc07bc8a3f3
--- /dev/null
+++ b/regression/cbmc/array-bug-6230/test.desc
@@ -0,0 +1,8 @@
+CORE
+main.c
+--malloc-may-fail --malloc-fail-null --pointer-check
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+A simplified test case that triggers issue #6230