Merge pull request #1720 from goblint/issue_1719

`IsMultiple` in `MallocWrapper`: Check uniqueness of allocating(!) thread

Author: michael-schwarz

src/analyses/wrapperFunctionAnalysis.ml

@@ -171,7 +171,10 @@ module MallocWrapper : MCPSpec = struct
       NodeVarinfoMap.mem_varinfo v
     | Q.IsMultiple v ->
       begin match NodeVarinfoMap.from_varinfo v with
-        | Some (_, _, c) -> UniqueCount.is_top c || not (man.ask Q.MustBeUniqueThread)
+        | Some (t, _, c) -> UniqueCount.is_top c ||
+                            (match t with
+                             | `Lifted tid -> not (Thread.is_unique tid)
+                             | _ -> true)
         | None -> false
       end
     | _ -> Queries.Result.top q

tests/regression/11-heap/17-unique-mt.c

@@ -0,0 +1,26 @@
+// PARAM: --set ana.malloc.unique_address_count 3
+#include<pthread.h>
+static int iRThreads = 1;
+static int data1Value = 0;
+pthread_mutex_t *data1Lock;
+
+void *funcA(void *param) {
+    pthread_mutex_lock(data1Lock);
+    data1Value = 1; //NORACE
+    pthread_mutex_unlock(data1Lock);
+}
+
+int main(int argc, char *argv[]) {
+    data1Lock = (pthread_mutex_t *) malloc(sizeof(pthread_mutex_t));
+
+    pthread_t one;
+    pthread_t other[3];
+
+    pthread_create(&one, ((void *)0), &funcA, ((void *)0));
+
+    for (int i = 0; i < 3; i++) {
+      pthread_create(&other[i], ((void *)0), &funcA, ((void *)0));
+    }
+
+    return 0;
+}