Merge pull request #1172 from goblint/races_sjlj

Add some `setjump/longjump` tests for race detection

tests/regression/68-longjmp/52-races.c

@@ -0,0 +1,35 @@
+// PARAM: --enable ana.int.interval
+#include <stdio.h>
+#include <stdlib.h>
+#include <setjmp.h>
+#include <pthread.h>
+
+jmp_buf env_buffer;
+int global = 0;
+pthread_mutex_t mutex1 = PTHREAD_MUTEX_INITIALIZER;
+
+void *t_fun(void *arg) {
+  pthread_mutex_lock(&mutex1);
+  global = 3; // NORACE
+  pthread_mutex_unlock(&mutex1);
+  return NULL;
+}
+
+int bar() {
+   pthread_mutex_lock(&mutex1);
+   longjmp(env_buffer, 2);
+   pthread_mutex_unlock(&mutex1);
+   return 8;
+}
+
+int main() {
+   pthread_t id;
+   pthread_create(&id, NULL, t_fun, NULL);
+
+   if(!setjmp( env_buffer )) {
+      bar();
+   }
+
+   global = 5; // NORACE
+   pthread_mutex_unlock(&mutex1);
+}

tests/regression/68-longjmp/53-races-no.c

@@ -0,0 +1,36 @@
+// PARAM: --enable ana.int.interval
+#include <stdio.h>
+#include <stdlib.h>
+#include <setjmp.h>
+#include <pthread.h>
+
+jmp_buf env_buffer;
+int global = 0;
+pthread_mutex_t mutex1 = PTHREAD_MUTEX_INITIALIZER;
+
+void *t_fun(void *arg) {
+  pthread_mutex_lock(&mutex1);
+  global = 3; // NORACE
+  pthread_mutex_unlock(&mutex1);
+  return NULL;
+}
+
+int bar() {
+   pthread_mutex_lock(&mutex1);
+   if(global ==3) {
+      longjmp(env_buffer, 2);
+   }
+   return 8;
+}
+
+int main() {
+   pthread_t id;
+   pthread_create(&id, NULL, t_fun, NULL);
+
+   if(!setjmp( env_buffer )) {
+      bar();
+   }
+
+   global = 5; // NORACE
+   pthread_mutex_unlock(&mutex1);
+}

tests/regression/68-longjmp/54-races-actually.c

@@ -0,0 +1,50 @@
+// PARAM: --enable ana.int.interval
+#include <stdio.h>
+#include <stdlib.h>
+#include <setjmp.h>
+#include <pthread.h>
+
+jmp_buf env_buffer;
+int global = 0;
+pthread_mutex_t mutex1 = PTHREAD_MUTEX_INITIALIZER;
+
+void *t_fun(void *arg) {
+  pthread_mutex_lock(&mutex1);
+  global = 3; // RACE
+  pthread_mutex_unlock(&mutex1);
+  return NULL;
+}
+
+int bar() {
+   pthread_mutex_lock(&mutex1);
+   if(global == 3) {
+      longjmp(env_buffer, 2);
+   } else {
+      longjmp(env_buffer, 4);
+   }
+   return 8;
+}
+
+int main() {
+   pthread_t id;
+   pthread_create(&id, NULL, t_fun, NULL);
+   int n = 0;
+
+   switch(setjmp( env_buffer )) {
+      case 0:
+         bar();
+         break;
+      case 2:
+         n=1;
+         pthread_mutex_unlock(&mutex1);
+         break;
+      default:
+         break;
+   }
+
+   global = 5; //RACE
+
+   if(n == 0) {
+      pthread_mutex_unlock(&mutex1);
+   }
+}

tests/regression/68-longjmp/55-races-no-return.c

@@ -0,0 +1,50 @@
+// PARAM: --enable ana.int.interval
+#include <stdio.h>
+#include <stdlib.h>
+#include <setjmp.h>
+#include <pthread.h>
+
+jmp_buf env_buffer;
+int global = 0;
+pthread_mutex_t mutex1 = PTHREAD_MUTEX_INITIALIZER;
+
+void *t_fun(void *arg) {
+  pthread_mutex_lock(&mutex1);
+  global = 3; //NORACE
+  pthread_mutex_unlock(&mutex1);
+  return NULL;
+}
+
+int bar() {
+   pthread_mutex_lock(&mutex1);
+   if(global == 7) {
+      longjmp(env_buffer, 2);
+   } else {
+      longjmp(env_buffer, 4);
+   }
+   return 8;
+}
+
+int main() {
+   pthread_t id;
+   pthread_create(&id, NULL, t_fun, NULL);
+   int n = 0;
+
+   switch(setjmp( env_buffer )) {
+      case 0:
+         bar();
+         break;
+      case 2:
+         n=1;
+         pthread_mutex_unlock(&mutex1);
+         break;
+      default:
+         break;
+   }
+
+   global = 5; //NORACE
+
+   if(n == 0) {
+      pthread_mutex_unlock(&mutex1);
+   }
+}