Merge pull request #584 from goblint/preprocessor_exclude_stdlib

Preprocessor directives to disable Goblint includes

Author: michael-schwarz

includes/pthread.c

@@ -1,3 +1,4 @@
+#ifndef GOBLINT_NO_PTHREAD_ONCE
 #include <pthread.h>
 
 int pthread_once(pthread_once_t *once_control,void (*init_routine)(void)) __attribute__((goblint_stub));
@@ -7,3 +8,4 @@ int pthread_once(pthread_once_t *once_control,void (*init_routine)(void)) {
   init_routine();
   return top;
 }
+#endif

includes/stdlib.c

@@ -1,5 +1,8 @@
+#if !defined(GOBLINT_NO_QSORT) || !defined(GOBLINT_NO_BSEARCH)
 #include <stddef.h>
+#endif
 
+#ifndef GOBLINT_NO_QSORT
 void qsort(void *ptr, size_t count, size_t size, int (*comp)(const void*, const void*)) __attribute__((goblint_stub));
 void qsort(void *ptr, size_t count, size_t size, int (*comp)(const void*, const void*)) {
   // call all possible compares first, before invalidating array elements
@@ -28,8 +31,9 @@ void qsort(void *ptr, size_t count, size_t size, int (*comp)(const void*, const
 
   // array isn't actually sorted! just pretend calls for Goblint
 }
+#endif
 
-
+#ifndef GOBLINT_NO_BSEARCH
 void* bsearch(const void *key, const void *ptr, size_t count, size_t size, int (*comp)(const void*, const void*))  __attribute__((goblint_stub));
 void* bsearch(const void *key, const void *ptr, size_t count, size_t size, int (*comp)(const void*, const void*)) {
   // linear search for simplicity
@@ -42,3 +46,4 @@ void* bsearch(const void *key, const void *ptr, size_t count, size_t size, int (
 
   return NULL;
 }
+#endif

tests/regression/41-stdlib/03-noqsort.c

@@ -0,0 +1,10 @@
+// PARAM: --set cppflags[+] -DGOBLINT_NO_QSORT
+#include<stddef.h>
+
+// There should be no CIL warning about multiple definitions here
+void qsort(void *ptr, size_t count, size_t size, int (*comp)(const void*, const void*), int more) {
+}
+
+int main() {
+
+}