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 0000000000..77b5d60142 --- /dev/null +++ b/regression/cbmc/assigning_nullpointers_should_not_crash_symex/main.c @@ -0,0 +1,19 @@ +#include +#include + +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 0000000000..a78f480b98 --- /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