Merge pull request #1265 from goblint/mutex-meet-tid-memsafety

Test for `mutex-meet-tid` for ValidDeref & Move `Afterconfig.run` to ensure privatizations can potentially be auto-tuned

src/autoTune.ml

@@ -224,7 +224,7 @@ 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;
   | ValidMemtrack
   | ValidMemcleanup -> (* Enable the memLeak analysis *)
     let memLeakAna = ["memLeak"] in

src/maingoblint.ml

@@ -191,10 +191,10 @@ let handle_flags () =
 
 let handle_options () =
   check_arguments ();
-  AfterConfig.run ();
   Sys.set_signal (GobSys.signal_of_string (get_string "dbg.solver-signal")) Signal_ignore; (* Ignore solver-signal before solving (e.g. MyCFG), otherwise exceptions self-signal the default, which crashes instead of printing backtrace. *)
   if AutoTune.isActivated "memsafetySpecification" && get_string "ana.specification" <> "" then
     AutoTune.focusOnMemSafetySpecification ();
+  AfterConfig.run ();
   Cilfacade.init_options ();
   handle_flags ()
 

tests/regression/74-invalid_deref/31-multithreaded.c

@@ -0,0 +1,21 @@
+//PARAM: --set ana.path_sens[+] threadflag  --set ana.activated[+] memOutOfBounds --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; //NOWARN
+  pthread_mutex_unlock(&mutex);
+  return 0;
+}