diff --git a/src/analyses/threadFlag.ml b/src/analyses/threadFlag.ml index e1efcaaba5..022fb72f29 100644 --- a/src/analyses/threadFlag.ml +++ b/src/analyses/threadFlag.ml @@ -54,13 +54,15 @@ struct module A = struct - include BoolDomain.Bool - let name () = "multi" - let may_race m1 m2 = m1 && m2 (* kill access when single threaded *) - let should_print m = not m + include Flag + let name () = "flag" + let may_race f1 f2 = + (* TODO: no longer accounts for MustBeSingleThreaded from other analyses via is_currently_multi *) + Flag.is_multi f1 && Flag.is_multi f2 && (* both must be multi-threaded *) + (Flag.is_not_main f1 || Flag.is_not_main f2) (* at least one must be non-main *) + let should_print f = not (Flag.is_multi f) end - let access ctx _ = - is_currently_multi (Analyses.ask_of_ctx ctx) + let access ctx _ = ctx.local let threadenter ctx ~multiple lval f args = if not (has_ever_been_multi (Analyses.ask_of_ctx ctx)) then diff --git a/tests/regression/10-synch/29-threadflag-main.c b/tests/regression/10-synch/29-threadflag-main.c new file mode 100644 index 0000000000..34ce75b92b --- /dev/null +++ b/tests/regression/10-synch/29-threadflag-main.c @@ -0,0 +1,18 @@ +// PARAM: --set ana.activated[-] threadid +// Deactivate threadid to rely on threadflag only. +#include +#include + +int myglobal; + +void *t_fun(void *arg) { + return NULL; +} + +int main(void) { + pthread_t id; + pthread_create(&id, NULL, t_fun, NULL); + myglobal=myglobal+1; // NORACE + pthread_join (id, NULL); + return 0; +} diff --git a/tests/regression/13-privatized/63-access-threadspawn-lval.t b/tests/regression/13-privatized/63-access-threadspawn-lval.t index 313459637c..18ea93968a 100644 --- a/tests/regression/13-privatized/63-access-threadspawn-lval.t +++ b/tests/regression/13-privatized/63-access-threadspawn-lval.t @@ -12,7 +12,7 @@ Should have (safe) write accesses to id1 and id2: dead: 0 total lines: 13 [Success][Race] Memory location id1 (safe): (63-access-threadspawn-lval.c:4:11-4:14) - write with [multi:false, thread:[main]] (conf. 110) (exp: & *((pthread_t * __restrict )(& id1))) (63-access-threadspawn-lval.c:27:3-27:37) + write with [flag:Singlethreaded, thread:[main]] (conf. 110) (exp: & *((pthread_t * __restrict )(& id1))) (63-access-threadspawn-lval.c:27:3-27:37) [Success][Race] Memory location id2 (safe): (63-access-threadspawn-lval.c:5:11-5:14) write with [mhp:{created={[main, f@63-access-threadspawn-lval.c:27:3-27:37]}}, thread:[main]] (conf. 110) (exp: (pthread_t * __restrict )(& id2)) (63-access-threadspawn-lval.c:28:3-28:37) write with [mhp:{created={[main, f@63-access-threadspawn-lval.c:27:3-27:37]}}, thread:[main]] (conf. 110) (exp: & *((pthread_t * __restrict )(& id2))) (63-access-threadspawn-lval.c:28:3-28:37) diff --git a/tests/regression/13-privatized/64-access-invalidate.t b/tests/regression/13-privatized/64-access-invalidate.t index 28227ec475..2d719ec89c 100644 --- a/tests/regression/13-privatized/64-access-invalidate.t +++ b/tests/regression/13-privatized/64-access-invalidate.t @@ -12,7 +12,7 @@ Should have (safe) write access to id1 and magic2 invalidate to A: dead: 0 total lines: 10 [Success][Race] Memory location id (safe): (64-access-invalidate.c:4:11-4:13) - write with [multi:false, thread:[main]] (conf. 110) (exp: & *((pthread_t * __restrict )(& id))) (64-access-invalidate.c:21:3-21:36) + write with [flag:Singlethreaded, thread:[main]] (conf. 110) (exp: & *((pthread_t * __restrict )(& id))) (64-access-invalidate.c:21:3-21:36) [Info][Race] Memory locations race summary: safe: 1 vulnerable: 0