From d54c31d6b3f4c193a7b4cc321bf154f79eb8fbd5 Mon Sep 17 00:00:00 2001
From: karoliineh <karoliine.holter@ut.ee>
Date: Wed, 13 Sep 2023 16:55:54 +0300
Subject: [PATCH] Add test for nullpointer.dereference.refine

---
 .../16-nullpointer-dereference-refine.c       | 45 +++++++++++++++++++
 1 file changed, 45 insertions(+)
 create mode 100644 tests/regression/26-undefined_behavior/16-nullpointer-dereference-refine.c

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 <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;
+}
\ No newline at end of file