diff --git a/src/analyses/wrapperFunctionAnalysis.ml b/src/analyses/wrapperFunctionAnalysis.ml index 1228a809ab..929d9e2b0b 100644 --- a/src/analyses/wrapperFunctionAnalysis.ml +++ b/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 diff --git a/tests/regression/11-heap/18-unique-st.c b/tests/regression/11-heap/18-unique-st.c new file mode 100644 index 0000000000..01f52cd35f --- /dev/null +++ b/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 +#include + +int main(int argc, char *argv[]) { + int* ptr = (int*)malloc(sizeof(int)); + *ptr = 8; + *ptr = 5; + + __goblint_check(*ptr ==5); + + return 0; +}