Add test for nullpointer.dereference.refine

tests/regression/26-undefined_behavior/16-nullpointer-dereference-refine.c

@@ -0,0 +1,45 @@
+// PARAM: --enable sem.null-pointer.dereference-refine
+#include <stdio.h>
+
+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;
+}