Merge pull request #547 from goblint/pthread_once

Add implementation for `pthread_once`

Author: michael-schwarz

includes/dune

@@ -4,6 +4,7 @@
   (files
     assert.h
     stdlib.c
+    pthread.c
     linuxlight.h
     sv-comp.c
     (linux/goblint_preconf.h as linux/goblint_preconf.h) ; must repeat directory, otherwise gets stripped from target

includes/pthread.c

@@ -0,0 +1,9 @@
+#include <pthread.h>
+
+int pthread_once(pthread_once_t *once_control,void (*init_routine)(void)) __attribute__((goblint_stub));
+int pthread_once(pthread_once_t *once_control,void (*init_routine)(void)) {
+  // Not actually once, just call it
+  int top;
+  init_routine();
+  return top;
+}

src/maingoblint.ml

@@ -280,7 +280,7 @@ let preprocess_files () =
 
   let extra_arg_files = ref [] in
 
-  extra_arg_files := find_custom_include "stdlib.c" :: !extra_arg_files;
+  extra_arg_files := find_custom_include "stdlib.c" :: find_custom_include "pthread.c" :: !extra_arg_files;
 
   if get_bool "ana.sv-comp.functions" then
     extra_arg_files := find_custom_include "sv-comp.c" :: !extra_arg_files;

sv-comp/archive.sh

@@ -14,6 +14,7 @@ zip goblint/sv-comp/goblint.zip \
     goblint/goblint \
     goblint/conf/svcomp22.json \
     goblint/includes/stdlib.c \
+    goblint/includes/pthread.c \
     goblint/includes/sv-comp.c \
     goblint/README.md \
     goblint/LICENSE

tests/regression/02-base/10-init_allfuns.c

@@ -1,5 +1,4 @@
 // PARAM: --enable allfuns --set ana.activated "['base','threadid','threadflag','escape','mutex','access','mallocWrapper']"
-
 int glob1 = 5;
 int glob2 = 7;
 

tests/regression/02-base/71-pthread-once.c

@@ -0,0 +1,16 @@
+//PARAM: --disable sem.unknown_function.spawn
+#include <pthread.h>
+#include <assert.h>
+
+int g;
+pthread_once_t once = PTHREAD_ONCE_INIT;
+
+void t_fun() {
+  assert(1); // reachable!
+  return NULL;
+}
+
+int main() {
+  pthread_once(&once,t_fun);
+  return 0;
+}

tests/regression/07-uninit/14-struct_in_struct.c

@@ -43,6 +43,7 @@ int main(){
 
 	mod_S1(&tt1.s); //NOWARN
 	mod_S2(&tt2.s); //NOWARN
+	
 	mod_S31(&tt3.s); //NOWARN
 	mod_S32(&tt3.s); //NOWARN