Enable mutex-meet-tid for ValidDeref

goblint · Nov 22, 2023 · 17ebe80 · 17ebe80
1 parent 9c808c9
commit 17ebe80
Show file tree

Hide file tree

Showing 2 changed files with 26 additions and 1 deletion.
diff --git a/src/autoTune.ml b/src/autoTune.ml
@@ -222,7 +222,11 @@ let focusOnMemSafetySpecification (spec: Svcomp.Specification.t) =
     print_endline "Setting \"cil.addNestedScopeAttr\" to true";
     set_bool "cil.addNestedScopeAttr" true;
     print_endline @@ "Specification: ValidDeref -> enabling memOutOfBounds analysis \"" ^ (String.concat ", " memOobAna) ^ "\"";
-    enableAnalyses memOobAna
+    enableAnalyses memOobAna;
+    (* Set privatization to mutex-meet-tid *)
+    set_string "ana.base.privatization" "mutex-meet-tid";
+    (* Required for mutex-meet-tid privatization *)
+    GobConfig.set_auto "ana.path_sens[+]" "threadflag";
   | ValidMemtrack
   | ValidMemcleanup -> (* Enable the memLeak analysis *)
     let memLeakAna = ["memLeak"] in

diff --git a/tests/regression/74-invalid_deref/31-multithreaded.c b/tests/regression/74-invalid_deref/31-multithreaded.c
@@ -0,0 +1,21 @@
+//PARAM: --set ana.activated[+] useAfterFree --set ana.activated[+] threadJoins --set ana.path_sens[+] threadflag  --set ana.activated[+] memOutOfBounds --enable ana.int.interval --set ana.base.arrays.domain partitioned --set ana.base.privatization mutex-meet-tid
+#include <pthread.h>
+
+int data;
+int *p = &data, *q;
+pthread_mutex_t mutex;
+void *t_fun(void *arg) {
+  pthread_mutex_lock(&mutex);
+  *p = 8;
+  pthread_mutex_unlock(&mutex);
+  return ((void *)0);
+}
+int main() {
+  pthread_t id;
+  pthread_create(&id, ((void *)0), t_fun, ((void *)0));
+  q = p;
+  pthread_mutex_lock(&mutex);
+  *q = 8;
+  pthread_mutex_unlock(&mutex);
+  return 0;
+}