diff --git a/tests/regression/26-undefined_behavior/16-nullpointer-dereference-refine.c b/tests/regression/26-undefined_behavior/16-nullpointer-dereference-refine.c new file mode 100644 index 0000000000..97d28d99b3 --- /dev/null +++ b/tests/regression/26-undefined_behavior/16-nullpointer-dereference-refine.c @@ -0,0 +1,45 @@ +// PARAM: --enable sem.null-pointer.dereference-refine +#include + +struct person { + int age; + int height; + int* ptr; +}; + +int main(){ + int r1, r2, p; + int *a = NULL; + int *b; + + switch(r1) { + case 1: + *a = 10; // WARN + __goblint_check(0); // NOWARN (unreachable) + break; + case 2: + *a = 10; // WARN + __goblint_check(0); // NOWARN (unreachable) + break; + case 3: + *b = 10; // WARN + p = *b; // NOWARN + case 4: + if (r2) { + struct person new_person = {1,1, NULL}; + p = *(new_person.ptr); // WARN + } else { + int test = 3; + struct person non_null = {1,1, &test}; + p = *(non_null.ptr); + } + __goblint_check(p != NULL); // reachable + break; + // TODO: case 5: nullpointer in if condition + // TODO: case 6: nullpointer as a function argument + default: + // code block + break; + } + return 1; +} \ No newline at end of file