OpenBSD compatibility

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,27 @@ 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

@@ -2,7 +2,13 @@
 /* FUNCTION: putchar */
 
 #ifndef __CPROVER_STDIO_H_INCLUDED
+# if !defined(__OpenBSD__)
 #include <stdio.h>
+# else
+// on OpenBSD, there are some definitions that the checker does not like.
+#include <stdio_openbsd_compat.h>
+# endif
+
 #define __CPROVER_STDIO_H_INCLUDED
 #endif
 

src/ansi-c/library/stdio_openbsd_compat.h

@@ -0,0 +1,54 @@
+/*-
+ * Portions of this file were lifted from OpenBSD's stdio.h.
+ *
+ * Copyright (c) 1990 The Regents of the University of California.
+ * All rights reserved.
+ *
+ * This code is derived from software contributed to Berkeley by
+ * Chris Torek.
+ *
+ * Redistribution and use in source and binary forms, with or without
+ * modification, are permitted provided that the following conditions
+ * are met:
+ * 1. Redistributions of source code must retain the above copyright
+ *    notice, this list of conditions and the following disclaimer.
+ * 2. Redistributions in binary form must reproduce the above copyright
+ *    notice, this list of conditions and the following disclaimer in the
+ *    documentation and/or other materials provided with the distribution.
+ * 3. Neither the name of the University nor the names of its contributors
+ *    may be used to endorse or promote products derived from this software
+ *    without specific prior written permission.
+ *
+ * THIS SOFTWARE IS PROVIDED BY THE REGENTS AND CONTRIBUTORS ``AS IS'' AND
+ * ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE
+ * IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE
+ * ARE DISCLAIMED.  IN NO EVENT SHALL THE REGENTS OR CONTRIBUTORS BE LIABLE
+ * FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL
+ * DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS
+ * OR SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION)
+ * HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT
+ * LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY
+ * OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF
+ * SUCH DAMAGE.
+ */
+#ifndef	_STDIO_H_
+#define	_STDIO_H_
+
+#include <stdarg.h>
+
+typedef	struct __sFILE {
+    int dummy;
+} FILE;
+
+extern FILE __sF[3];
+
+#define	stdin	(&__sF[0])
+#define	stdout	(&__sF[1])
+#define	stderr	(&__sF[2])
+
+int	 printf(const char *, ...);
+int	 vfscanf(FILE *, const char *, va_list);
+int	 vsscanf(const char *, const char *, va_list);
+int	 vfprintf(FILE *, const char *, va_list);
+
+#endif /* _STDIO_H_ */

src/ansi-c/library_check.sh

@@ -10,7 +10,7 @@ for f in "$@"; do
     perl -p -i -e 's/(_mm_.fence)/s$1/' __libcheck.c
     perl -p -i -e 's/(__sync_)/s$1/' __libcheck.c
     perl -p -i -e 's/(__noop)/s$1/' __libcheck.c
-    $CC -std=gnu99 -E -include library/cprover.h -D__CPROVER_bool=_Bool -D__CPROVER_thread_local=__thread -DLIBRARY_CHECK -o __libcheck.i __libcheck.c
+    $CC -std=gnu99 -E -include library/cprover.h -I library -D__CPROVER_bool=_Bool -D__CPROVER_thread_local=__thread -DLIBRARY_CHECK -o __libcheck.i __libcheck.c
     $CC -S -Wall -Werror -pedantic -Wextra -std=gnu99 __libcheck.i -o __libcheck.s -Wno-unused-label
     ec="${?}"
     rm __libcheck.s __libcheck.i __libcheck.c