From 820fd3559adb4513658f94483db97b184c42e9ca Mon Sep 17 00:00:00 2001
From: Hannes Steffenhagen <hannes.steffenhagen@diffblue.com>
Date: Wed, 13 Feb 2019 11:19:26 +0000
Subject: [PATCH] Add KNOWNBUG regression test for GH issue #4168

---
 .../main.c                                    | 19 +++++++++++++++++++
 .../test.desc                                 | 10 ++++++++++
 2 files changed, 29 insertions(+)
 create mode 100644 regression/cbmc/assigning_nullpointers_should_not_crash_symex/main.c
 create mode 100644 regression/cbmc/assigning_nullpointers_should_not_crash_symex/test.desc

diff --git a/regression/cbmc/assigning_nullpointers_should_not_crash_symex/main.c b/regression/cbmc/assigning_nullpointers_should_not_crash_symex/main.c
new file mode 100644
index 00000000000..77b5d60142f
--- /dev/null
+++ b/regression/cbmc/assigning_nullpointers_should_not_crash_symex/main.c
@@ -0,0 +1,19 @@
+#include <assert.h>
+#include <stddef.h>
+
+struct linked_list
+{
+  struct linked_list *next;
+};
+
+int main(void)
+{
+  size_t list_sz = 8ul;
+  assert(list_sz == sizeof(struct linked_list));
+  struct linked_list *list = malloc(list_sz);
+  // this line makes symex crash for some reason
+  // last known to work on 9cf2bfb3e458d419d842a0e1fd26fb1748451851
+  // (no bisection has been done yet to narrow down the source of the error)
+  list->next = (struct linked_list *)0;
+  assert(!list->next);
+}
diff --git a/regression/cbmc/assigning_nullpointers_should_not_crash_symex/test.desc b/regression/cbmc/assigning_nullpointers_should_not_crash_symex/test.desc
new file mode 100644
index 00000000000..a78f480b980
--- /dev/null
+++ b/regression/cbmc/assigning_nullpointers_should_not_crash_symex/test.desc
@@ -0,0 +1,10 @@
+KNOWNBUG
+main.c
+
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring
+--
+This tests for the regression described in https://github.com/diffblue/cbmc/issues/4168