Merge pull request #1721 from goblint/issue_1719_followup

Fallback for malloc uniqueness for when threading analyses are disabled

Author: michael-schwarz

src/analyses/wrapperFunctionAnalysis.ml

@@ -174,7 +174,10 @@ module MallocWrapper : MCPSpec = struct
         | Some (t, _, c) -> UniqueCount.is_top c ||
                             (match t with
                              | `Lifted tid -> not (Thread.is_unique tid)
-                             | _ -> true)
+                             | _ ->
+                               (* The thread analysis may be completely disabled; in this case we fall back on checking whether the program has been single threaded since start *)
+                               not (man.ask (Q.MustBeSingleThreaded {since_start = true}))
+                            )
         | None -> false
       end
     | _ -> Queries.Result.top q

tests/regression/11-heap/18-unique-st.c

@@ -0,0 +1,13 @@
+// PARAM: --set ana.malloc.unique_address_count 1 --set ana.autotune.activated '["reduceAnalyses"]' --enable ana.autotune.enabled
+#include<pthread.h>
+#include<goblint.h>
+
+int main(int argc, char *argv[]) {
+    int* ptr = (int*)malloc(sizeof(int));
+    *ptr = 8;
+    *ptr = 5;
+
+    __goblint_check(*ptr ==5);
+
+    return 0;
+}