diff --git a/src/analyses/raceAnalysis.ml b/src/analyses/raceAnalysis.ml index f35e6756a1..6b7217147e 100644 --- a/src/analyses/raceAnalysis.ml +++ b/src/analyses/raceAnalysis.ml @@ -369,7 +369,7 @@ struct let special ctx (lvalOpt: lval option) (f:varinfo) (arglist:exp list) : D.t = (* perform shallow and deep invalidate according to Library descriptors *) let desc = LibraryFunctions.find f in - if List.mem LibraryDesc.ThreadUnsafe desc.attrs then ( + if List.mem LibraryDesc.ThreadUnsafe desc.attrs && ThreadFlag.is_currently_multi (Analyses.ask_of_ctx ctx) then ( let exp = Lval (Var f, NoOffset) in let conf = 110 in let kind = AccessKind.Call in diff --git a/tests/regression/00-sanity/52-thread-unsafe-libfuns-single-thread.c b/tests/regression/00-sanity/52-thread-unsafe-libfuns-single-thread.c new file mode 100644 index 0000000000..94c0f3efeb --- /dev/null +++ b/tests/regression/00-sanity/52-thread-unsafe-libfuns-single-thread.c @@ -0,0 +1,16 @@ +// PARAM: --enable allglobs --set ana.activated[+] threadJoins +#include +#include + +void *t_benign(void *arg) { + return NULL; +} + +int main() { + rand(); + pthread_t id; + pthread_create(&id, NULL, t_benign, NULL); + pthread_join(id, NULL); + rand(); + return 0; +} \ No newline at end of file diff --git a/tests/regression/00-sanity/52-thread-unsafe-libfuns-single-thread.t b/tests/regression/00-sanity/52-thread-unsafe-libfuns-single-thread.t new file mode 100644 index 0000000000..64413bae36 --- /dev/null +++ b/tests/regression/00-sanity/52-thread-unsafe-libfuns-single-thread.t @@ -0,0 +1,5 @@ + $ goblint --enable allglobs --set ana.activated[+] threadJoins 52-thread-unsafe-libfuns-single-thread.c + [Info][Deadcode] Logical lines of code (LLoC) summary: + live: 8 + dead: 0 + total lines: 8 diff --git a/tests/regression/29-svcomp/32-no-ov.t b/tests/regression/29-svcomp/32-no-ov.t index 85eb90c185..1dc22ed89e 100644 --- a/tests/regression/29-svcomp/32-no-ov.t +++ b/tests/regression/29-svcomp/32-no-ov.t @@ -9,8 +9,3 @@ dead: 0 total lines: 3 SV-COMP result: true - [Info][Race] Memory locations race summary: - safe: 1 - vulnerable: 0 - unsafe: 0 - total memory locations: 1