Remove workaround for #547

michael-schwarz · michael-schwarz · commit 85b2380b07be · 2025-01-27T10:50:52.000+01:00
diff --git a/conf/bench-yaml-validate.json b/conf/bench-yaml-validate.json
@@ -71,7 +71,6 @@
   },
   "pre": {
     "cppflags": [
-      "-DGOBLINT_NO_PTHREAD_ONCE",
       "-DGOBLINT_NO_QSORT",
       "-DGOBLINT_NO_BSEARCH"
     ]
diff --git a/conf/bench-yaml.json b/conf/bench-yaml.json
@@ -67,7 +67,6 @@
   },
   "pre": {
     "cppflags": [
-      "-DGOBLINT_NO_PTHREAD_ONCE",
       "-DGOBLINT_NO_QSORT",
       "-DGOBLINT_NO_BSEARCH"
     ]
diff --git a/conf/ldv-races.json b/conf/ldv-races.json
@@ -1,7 +1,6 @@
 {
   "pre": {
     "cppflags": [
-      "-DGOBLINT_NO_PTHREAD_ONCE",
       "-DGOBLINT_NO_QSORT",
       "-DGOBLINT_NO_BSEARCH"
     ]
diff --git a/conf/traces-rel.json b/conf/traces-rel.json
@@ -83,7 +83,6 @@
   },
   "pre": {
     "cppflags": [
-      "-DGOBLINT_NO_PTHREAD_ONCE",
       "-DGOBLINT_NO_QSORT",
       "-DGOBLINT_NO_BSEARCH"
     ]
diff --git a/lib/libc/stub/src/pthread.c b/lib/libc/stub/src/pthread.c
diff --git a/scripts/sv-comp/archive.sh b/scripts/sv-comp/archive.sh
@@ -37,7 +37,6 @@ zip goblint/scripts/sv-comp/goblint.zip \
     goblint/lib/libc/stub/include/assert.h \
     goblint/lib/goblint/runtime/include/goblint.h \
     goblint/lib/libc/stub/src/stdlib.c \
-    goblint/lib/libc/stub/src/pthread.c \
     goblint/lib/sv-comp/stub/src/sv-comp.c \
     goblint/README.md \
     goblint/LICENSE
diff --git a/src/maingoblint.ml b/src/maingoblint.ml
@@ -418,9 +418,6 @@ let preprocess_files () =
   if List.mem "c" (get_string_list "lib.activated") then
     extra_files := find_custom_include (Fpath.v "stdlib.c") :: !extra_files;
 
-  if List.mem "pthread" (get_string_list "lib.activated") then
-    extra_files := find_custom_include (Fpath.v "pthread.c") :: !extra_files;
-
   if List.mem "sv-comp" (get_string_list "lib.activated") then
     extra_files := find_custom_include (Fpath.v "sv-comp.c") :: !extra_files;
 
diff --git a/tests/regression/03-practical/35-base-mutex-macos.t b/tests/regression/03-practical/35-base-mutex-macos.t
@@ -1,4 +1,4 @@
-  $ goblint --enable witness.yaml.enabled --disable witness.invariant.accessed --set pre.cppflags[+] -DGOBLINT_NO_PTHREAD_ONCE 35-base-mutex-macos.c
+  $ goblint --enable witness.yaml.enabled --disable witness.invariant.accessed --set pre.cppflags[+]
   [Info][Deadcode] Logical lines of code (LLoC) summary:
     live: 2
     dead: 0
diff --git a/tests/regression/71-doublelocking/07-rec-dyn-osx.c b/tests/regression/71-doublelocking/07-rec-dyn-osx.c
@@ -1,6 +1,5 @@
-// PARAM: --set ana.activated[+] 'maylocks' --set ana.activated[+] 'pthreadMutexType' --set pre.cppflags[+] "-DGOBLINT_NO_PTHREAD_ONCE"
+// PARAM: --set ana.activated[+] 'maylocks' --set ana.activated[+] 'pthreadMutexType'
 // Here, we do not include pthread.h, so MutexAttr.recursive_int remains at `2`, emulating the behavior of OS X.
-#define GOBLINT_NO_PTHREAD_ONCE 1
 typedef signed char __int8_t;
 typedef unsigned char __uint8_t;
 typedef short __int16_t;
diff --git a/tests/regression/71-doublelocking/20-default-init-osx.c b/tests/regression/71-doublelocking/20-default-init-osx.c
@@ -1,4 +1,4 @@
-// PARAM: --set ana.activated[+] 'maylocks' --set ana.activated[+] 'pthreadMutexType' --set pre.cppflags[+] "-DGOBLINT_NO_PTHREAD_ONCE"
+// PARAM: --set ana.activated[+] 'maylocks' --set ana.activated[+] 'pthreadMutexType'
 // Here, we do not include pthread.h, to emulate the behavior of OS X.
 #define NULL ((void *)0)
 typedef signed char __int8_t;
diff --git a/tests/regression/83-once/01-sanity.c b/tests/regression/83-once/01-sanity.c
@@ -1,4 +1,4 @@
-// PARAM: --set pre.cppflags[+] "-DGOBLINT_NO_PTHREAD_ONCE" --set ana.activated[+] pthreadOnce
+// PARAM: --set ana.activated[+] pthreadOnce
 #include <pthread.h>
 #include <stdio.h>
 
diff --git a/tests/regression/83-once/02-normal.c b/tests/regression/83-once/02-normal.c
@@ -1,4 +1,4 @@
-// PARAM: --set pre.cppflags[+] "-DGOBLINT_NO_PTHREAD_ONCE" --set ana.activated[+] pthreadOnce
+// PARAM: --set ana.activated[+] pthreadOnce
 #include <pthread.h>
 #include <stdio.h>
 
diff --git a/tests/regression/83-once/03-unknown.c b/tests/regression/83-once/03-unknown.c
@@ -1,4 +1,4 @@
-// PARAM: --set pre.cppflags[+] "-DGOBLINT_NO_PTHREAD_ONCE" --set ana.activated[+] pthreadOnce
+// PARAM: --set ana.activated[+] pthreadOnce
 #include <pthread.h>
 #include <stdio.h>
 
diff --git a/tests/regression/83-once/04-thread.c b/tests/regression/83-once/04-thread.c
@@ -1,4 +1,4 @@
-// PARAM: --set pre.cppflags[+] "-DGOBLINT_NO_PTHREAD_ONCE" --set ana.activated[+] pthreadOnce
+// PARAM: --set ana.activated[+] pthreadOnce
 #include <pthread.h>
 #include <stdio.h>
 

Original file line number	Diff line number	Diff line change
`@@ -71,7 +71,6 @@`
`71`	`71`	`},`
`72`	`72`	`"pre": {`
`73`	`73`	`"cppflags": [`
`74`		`- "-DGOBLINT_NO_PTHREAD_ONCE",`
`75`	`74`	`"-DGOBLINT_NO_QSORT",`
`76`	`75`	`"-DGOBLINT_NO_BSEARCH"`
`77`	`76`	`]`
Original file line number	Diff line number	Diff line change
`@@ -67,7 +67,6 @@`
`67`	`67`	`},`
`68`	`68`	`"pre": {`
`69`	`69`	`"cppflags": [`
`70`		`- "-DGOBLINT_NO_PTHREAD_ONCE",`
`71`	`70`	`"-DGOBLINT_NO_QSORT",`
`72`	`71`	`"-DGOBLINT_NO_BSEARCH"`
`73`	`72`	`]`
Original file line number	Diff line number	Diff line change
`@@ -1,7 +1,6 @@`
`1`	`1`	`{`
`2`	`2`	`"pre": {`
`3`	`3`	`"cppflags": [`
`4`		`- "-DGOBLINT_NO_PTHREAD_ONCE",`
`5`	`4`	`"-DGOBLINT_NO_QSORT",`
`6`	`5`	`"-DGOBLINT_NO_BSEARCH"`
`7`	`6`	`]`
Original file line number	Diff line number	Diff line change
`@@ -83,7 +83,6 @@`
`83`	`83`	`},`
`84`	`84`	`"pre": {`
`85`	`85`	`"cppflags": [`
`86`		`- "-DGOBLINT_NO_PTHREAD_ONCE",`
`87`	`86`	`"-DGOBLINT_NO_QSORT",`
`88`	`87`	`"-DGOBLINT_NO_BSEARCH"`
`89`	`88`	`]`
Original file line number	Diff line number	Diff line change
`@@ -1,4 +1,4 @@`
`1`		`- $ goblint --enable witness.yaml.enabled --disable witness.invariant.accessed --set pre.cppflags[+] -DGOBLINT_NO_PTHREAD_ONCE 35-base-mutex-macos.c`
	`1`	`+ $ goblint --enable witness.yaml.enabled --disable witness.invariant.accessed --set pre.cppflags[+]`
`2`	`2`	`[Info][Deadcode] Logical lines of code (LLoC) summary:`
`3`	`3`	`live: 2`
`4`	`4`	`dead: 0`
Original file line number	Diff line number	Diff line change
`@@ -1,4 +1,4 @@`
`1`		`-// PARAM: --set ana.activated[+] 'maylocks' --set ana.activated[+] 'pthreadMutexType' --set pre.cppflags[+] "-DGOBLINT_NO_PTHREAD_ONCE"`
	`1`	`+// PARAM: --set ana.activated[+] 'maylocks' --set ana.activated[+] 'pthreadMutexType'`
`2`	`2`	`// Here, we do not include pthread.h, to emulate the behavior of OS X.`
`3`	`3`	`#define NULL ((void *)0)`
`4`	`4`	`typedef signed char __int8_t;`
Original file line number	Diff line number	Diff line change
`@@ -1,4 +1,4 @@`
`1`		`-// PARAM: --set pre.cppflags[+] "-DGOBLINT_NO_PTHREAD_ONCE" --set ana.activated[+] pthreadOnce`
	`1`	`+// PARAM: --set ana.activated[+] pthreadOnce`
`2`	`2`	`#include <pthread.h>`
`3`	`3`	`#include <stdio.h>`
`4`	`4`