Add tests for library function races via NULL

tests/regression/05-lval_ls/20-race-null-void.c

@@ -0,0 +1,54 @@
+#include <pthread.h>
+#include <stdio.h>
+
+void *t_fun(void *arg) {
+  void **top;
+  free(top); // RACE
+  return NULL;
+}
+
+int main(void) {
+  pthread_t id;
+  pthread_create(&id, NULL, t_fun, NULL);
+
+  int r; // rand
+  int zero = 0; // IntDomain zero
+  void *null;
+  __goblint_assume(null == NULL); // AddressDomain NULL
+  int one = 1; // IntDomain one
+  void *unknown;
+  __goblint_assume(unknown != NULL); // AddressDomain unknown
+  void *top;
+  switch (r) {
+    case 0:
+      pthread_join(id, NULL); // NORACE
+      break;
+    case 1:
+      pthread_join(id, 0); // NORACE
+      break;
+    case 2:
+      pthread_join(id, zero); // NORACE
+      break;
+    case 3:
+      pthread_join(id, 1); // RACE
+      break;
+    case 4:
+      pthread_join(id, one); // RACE
+      break;
+    case 5:
+      pthread_join(id, r); // RACE
+      break;
+    case 6:
+      pthread_join(id, null); // NORACE
+      break;
+    case 7:
+      pthread_join(id, unknown); // RACE
+      break;
+    case 8:
+      pthread_join(id, top); // RACE
+      break;
+    default:
+      break;
+  }
+  return 0;
+}

tests/regression/05-lval_ls/21-race-null-type.c

@@ -0,0 +1,55 @@
+// PARAM: --enable ana.race.direct-arithmetic
+#include <pthread.h>
+#include <stdio.h>
+
+void *t_fun(void *arg) {
+  void *top;
+  time(top); // RACE
+  return NULL;
+}
+
+int main(void) {
+  pthread_t id;
+  pthread_create(&id, NULL, t_fun, NULL);
+
+  int r; // rand
+  int zero = 0; // IntDomain zero
+  void *null;
+  __goblint_assume(null == NULL); // AddressDomain NULL
+  int one = 1; // IntDomain one
+  void *unknown;
+  __goblint_assume(unknown != NULL); // AddressDomain unknown
+  void *top;
+  switch (r) {
+    case 0:
+      time(NULL); // NORACE
+      break;
+    case 1:
+      time(0); // NORACE
+      break;
+    case 2:
+      time(zero); // NORACE
+      break;
+    case 3:
+      time(1); // RACE
+      break;
+    case 4:
+      time(one); // RACE
+      break;
+    case 5:
+      time(r); // RACE
+      break;
+    case 6:
+      time(null); // NORACE
+      break;
+    case 7:
+      time(unknown); // RACE
+      break;
+    case 8:
+      time(top); // RACE
+      break;
+    default:
+      break;
+  }
+  return 0;
+}

tests/regression/05-lval_ls/22-race-null-void-deep.c

@@ -0,0 +1,56 @@
+#include <pthread.h>
+#include <stdio.h>
+
+pthread_key_t key;
+
+void *t_fun(void *arg) {
+  void *top;
+  pthread_setspecific(key, top); // RACE
+  return NULL;
+}
+
+int main(void) {
+  pthread_t id;
+  pthread_create(&id, NULL, t_fun, NULL);
+
+  int r; // rand
+  int zero = 0; // IntDomain zero
+  void *null;
+  __goblint_assume(null == NULL); // AddressDomain NULL
+  int one = 1; // IntDomain one
+  void *unknown;
+  __goblint_assume(unknown != NULL); // AddressDomain unknown
+  void *top;
+  switch (r) {
+    case 0:
+      pthread_setspecific(key, NULL); // NORACE
+      break;
+    case 1:
+      pthread_setspecific(key, 0); // NORACE
+      break;
+    case 2:
+      pthread_setspecific(key, zero); // NORACE
+      break;
+    case 3:
+      pthread_setspecific(key, 1); // RACE
+      break;
+    case 4:
+      pthread_setspecific(key, one); // RACE
+      break;
+    case 5:
+      pthread_setspecific(key, r); // RACE
+      break;
+    case 6:
+      pthread_setspecific(key, null); // NORACE
+      break;
+    case 7:
+      pthread_setspecific(key, unknown); // RACE
+      break;
+    case 8:
+      pthread_setspecific(key, top); // RACE
+      break;
+    default:
+      break;
+  }
+  return 0;
+}

tests/regression/05-lval_ls/23-race-null-type-deep.c

@@ -0,0 +1,54 @@
+#include <pthread.h>
+#include <stdio.h>
+
+void *t_fun(void *arg) {
+  void *top;
+  fclose(top); // RACE
+  return NULL;
+}
+
+int main(void) {
+  pthread_t id;
+  pthread_create(&id, NULL, t_fun, NULL);
+
+  int r; // rand
+  int zero = 0; // IntDomain zero
+  void *null;
+  __goblint_assume(null == NULL); // AddressDomain NULL
+  int one = 1; // IntDomain one
+  void *unknown;
+  __goblint_assume(unknown != NULL); // AddressDomain unknown
+  void *top;
+  switch (r) {
+    case 0:
+      feof(NULL); // NORACE
+      break;
+    case 1:
+      feof(0); // NORACE
+      break;
+    case 2:
+      feof(zero); // NORACE
+      break;
+    case 3:
+      feof(1); // RACE
+      break;
+    case 4:
+      feof(one); // RACE
+      break;
+    case 5:
+      feof(r); // RACE
+      break;
+    case 6:
+      feof(null); // NORACE
+      break;
+    case 7:
+      feof(unknown); // RACE
+      break;
+    case 8:
+      feof(top); // RACE
+      break;
+    default:
+      break;
+  }
+  return 0;
+}