Merge pull request #4174 from hannes-steffenhagen-diffblue/regression-add_nullpointer_regression_test

Add KNOWNBUG regression test for GH issue #4168

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

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