Skip to content

Commit

Permalink
Merge pull request #1307 from goblint/issue-1260
Browse files Browse the repository at this point in the history
Suppress thread-unsafe library function calls in single-threaded mode
  • Loading branch information
sim642 authored Dec 28, 2023
2 parents ea1bf23 + ecd0bc5 commit 3f4a6bc
Show file tree
Hide file tree
Showing 4 changed files with 22 additions and 6 deletions.
2 changes: 1 addition & 1 deletion src/analyses/raceAnalysis.ml
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down
Original file line number Diff line number Diff line change
@@ -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;
}
Original file line number Diff line number Diff line change
@@ -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
5 changes: 0 additions & 5 deletions tests/regression/29-svcomp/32-no-ov.t
Original file line number Diff line number Diff line change
Expand Up @@ -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

0 comments on commit 3f4a6bc

Please sign in to comment.