Merge pull request #4053 from nanolith/openbsd_compatibility

OpenBSD compatibility

Author: tautschnig

src/ansi-c/c_preprocess.cpp

@@ -589,19 +589,39 @@ bool c_preprocess_gcc_clang(
     switch(config.cpp.cpp_standard)
     {
     case configt::cppt::cpp_standardt::CPP98:
-      argv.push_back("-std=gnu++98");
+#if defined(__OpenBSD__)
+      if(preprocessor == configt::ansi_ct::preprocessort::CLANG)
+        argv.push_back("-std=c++98");
+      else
+#endif
+        argv.push_back("-std=gnu++98");
       break;
 
     case configt::cppt::cpp_standardt::CPP03:
-      argv.push_back("-std=gnu++03");
+#if defined(__OpenBSD__)
+      if(preprocessor == configt::ansi_ct::preprocessort::CLANG)
+        argv.push_back("-std=c++03");
+      else
+#endif
+        argv.push_back("-std=gnu++03");
       break;
 
     case configt::cppt::cpp_standardt::CPP11:
-      argv.push_back("-std=gnu++11");
+#if defined(__OpenBSD__)
+      if(preprocessor == configt::ansi_ct::preprocessort::CLANG)
+        argv.push_back("-std=c++11");
+      else
+#endif
+        argv.push_back("-std=gnu++11");
       break;
 
     case configt::cppt::cpp_standardt::CPP14:
-      argv.push_back("-std=gnu++14");
+#if defined(__OpenBSD__)
+      if(preprocessor == configt::ansi_ct::preprocessort::CLANG)
+        argv.push_back("-std=c++14");
+      else
+#endif
+        argv.push_back("-std=gnu++14");
       break;
     }
   }
@@ -610,15 +630,30 @@ bool c_preprocess_gcc_clang(
     switch(config.ansi_c.c_standard)
     {
     case configt::ansi_ct::c_standardt::C89:
-      argv.push_back("-std=gnu89");
+#if defined(__OpenBSD__)
+      if(preprocessor == configt::ansi_ct::preprocessort::CLANG)
+        argv.push_back("-std=c89");
+      else
+#endif
+        argv.push_back("-std=gnu89");
       break;
 
     case configt::ansi_ct::c_standardt::C99:
-      argv.push_back("-std=gnu99");
+#if defined(__OpenBSD__)
+      if(preprocessor == configt::ansi_ct::preprocessort::CLANG)
+        argv.push_back("-std=c99");
+      else
+#endif
+        argv.push_back("-std=gnu99");
       break;
 
     case configt::ansi_ct::c_standardt::C11:
-      argv.push_back("-std=gnu11");
+#if defined(__OpenBSD__)
+      if(preprocessor == configt::ansi_ct::preprocessort::CLANG)
+        argv.push_back("-std=c11");
+      else
+#endif
+        argv.push_back("-std=gnu11");
       break;
     }
   }

src/ansi-c/library/pthread_lib.c

@@ -731,7 +731,8 @@ int pthread_spin_trylock(pthread_spinlock_t *lock)
 int __VERIFIER_nondet_int();
 
 // no pthread_barrier_t on the Mac
-#ifndef __APPLE__
+// slightly different declaration on OpenBSD
+#if !defined(__APPLE__) && !defined(__OpenBSD__)
 inline int pthread_barrier_init(
   pthread_barrier_t *restrict barrier,
   const pthread_barrierattr_t *restrict attr, unsigned count)
@@ -751,6 +752,28 @@ inline int pthread_barrier_init(
 }
 #endif
 
+// pthread_barrier_init has a slightly different decl on OpenBSD
+#if defined(__OpenBSD__)
+inline int pthread_barrier_init(
+  pthread_barrier_t *restrict barrier,
+  pthread_barrierattr_t *restrict attr,
+  unsigned count)
+{
+__CPROVER_HIDE:;
+  (void)barrier;
+  (void)attr;
+  (void)count;
+
+#ifdef __CPROVER_CUSTOM_BITVECTOR_ANALYSIS
+  __CPROVER_set_must(barrier, "barrier-init");
+  __CPROVER_clear_may(barrier, "barrier-destroyed");
+#endif
+
+  int result = __VERIFIER_nondet_int();
+  return result;
+}
+#endif
+
 /* FUNCTION: pthread_barrier_destroy */
 
 #ifndef __CPROVER_PTHREAD_H_INCLUDED

src/ansi-c/library/stdio.c

@@ -6,6 +6,16 @@
 #define __CPROVER_STDIO_H_INCLUDED
 #endif
 
+/* undefine macros in OpenBSD's stdio.h that are problematic to the checker. */
+#if defined(__OpenBSD__)
+#undef getchar
+#undef putchar
+#undef getc
+#undef feof
+#undef ferror
+#undef fileno
+#endif
+
 __CPROVER_bool __VERIFIER_nondet___CPROVER_bool();
 
 inline int putchar(int c)

src/util/config.cpp

@@ -674,16 +674,17 @@ void configt::ansi_ct::set_arch_spec_sh4()
 
 configt::ansi_ct::c_standardt configt::ansi_ct::default_c_standard()
 {
-  #if defined(__APPLE__)
+#if defined(__APPLE__)
   // By default, clang on the Mac builds C code in GNU C11
   return c_standardt::C11;
-  #elif defined(__FreeBSD__)
+#elif defined(__FreeBSD__) || defined(__OpenBSD__)
   // By default, clang on FreeBSD builds C code in GNU C99
+  // By default, clang on OpenBSD builds C code in C99
   return c_standardt::C99;
-  #else
+#else
   // By default, gcc 5.4 or higher use gnu11; older versions use gnu89
   return c_standardt::C11;
-  #endif
+#endif
 }
 
 configt::cppt::cpp_standardt configt::cppt::default_cpp_standard()