diff --git a/src/analyses/threadJoins.ml b/src/analyses/threadJoins.ml index 2c48fbd75a..da6333aa91 100644 --- a/src/analyses/threadJoins.ml +++ b/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 diff --git a/tests/regression/51-threadjoins/06-ctxinsens.c b/tests/regression/51-threadjoins/06-ctxinsens.c new file mode 100644 index 0000000000..f09656d7fc --- /dev/null +++ b/tests/regression/51-threadjoins/06-ctxinsens.c @@ -0,0 +1,28 @@ +//PARAM: --set ana.activated[+] threadJoins --set ana.ctx_insens[+] threadJoins +#include + +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; +}