Merge pull request #982 from goblint/issue-968

Improve `threadJoins` when it is used context-insensitively

src/analyses/threadJoins.ml

@@ -87,6 +87,9 @@ struct
     | Queries.MustJoinedThreads -> (ctx.local:ConcDomain.MustThreadSet.t) (* type annotation needed to avoid "would escape the scope of its equation" *)
     | _ ->  Queries.Result.top q
 
+  let combine ctx (lval:lval option) fexp (f:fundec) (args:exp list) fc au =
+    D.union ctx.local au
+
   let startstate v = D.top ()
   let exitstate  v = D.top ()
 end

tests/regression/51-threadjoins/06-ctxinsens.c

@@ -0,0 +1,28 @@
+//PARAM: --set ana.activated[+] threadJoins --set ana.ctx_insens[+] threadJoins
+#include <pthread.h>
+
+int g = 10;
+
+void *t_fun(void *arg) {
+  g++; //NORACE
+  return NULL;
+}
+
+void benign() { 
+  // Causes must-joined set to be empty here!
+}
+
+int main(void) {
+  int t;
+
+  pthread_t id;
+  pthread_create(&id, NULL, t_fun, NULL);
+
+  benign();
+  pthread_join(id, NULL);
+  benign();
+  g++; //NORACE
+
+
+  return 0;
+}