Merge pull request #1307 from goblint/issue-1260

Suppress thread-unsafe library function calls in single-threaded mode

Author: sim642

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

tests/regression/00-sanity/52-thread-unsafe-libfuns-single-thread.c

@@ -0,0 +1,16 @@
+// PARAM: --enable allglobs --set ana.activated[+] threadJoins
+#include <stdlib.h>
+#include <pthread.h>
+
+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;
+}

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

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