Merge pull request #1230 from goblint/issue_1223

`threadAnalysis`: Only add to set of must-joined threads if argument to `pthread_join` evaluates to a singleton

src/analyses/threadAnalysis.ml

@@ -61,7 +61,8 @@ struct
            s
        in
        match TS.elements (ctx.ask (Queries.EvalThread id)) with
-       | threads -> List.fold_left join_thread ctx.local threads
+       | [t] -> join_thread ctx.local t (* single thread *)
+       | _ -> ctx.local (* if several possible threads are may-joined, none are must-joined *)
        | exception SetDomain.Unsupported _ -> ctx.local)
     | _ -> ctx.local
 

tests/regression/10-synch/28-join-array.c

@@ -0,0 +1,25 @@
+// PARAM: --set ana.activated[+] thread
+#include <pthread.h>
+
+int data = 0;
+pthread_mutex_t data_mutex;
+
+void *thread(void *arg) {
+  pthread_mutex_lock(&data_mutex);
+  data = 3; // RACE!
+  pthread_mutex_unlock(&data_mutex);
+  return NULL;
+}
+
+int main() {
+  pthread_t tids[2];
+
+  pthread_create(&tids[0], NULL, &thread, NULL);
+  pthread_create(&tids[1], NULL, &thread, NULL);
+
+  pthread_join(tids[0], NULL);
+
+  data = 1; //RACE!
+
+  return 1;
+}