C library: add __builtin_unreachable to functions that do not return

These calls are wrapped in #ifdef LIBRARY_CHECK and exist for the sole
purpose of making library_check.sh not warn about `noreturn` functions
seemingly returning.

Author: tautschnig

src/ansi-c/library/pthread_lib.c

@@ -314,6 +314,9 @@ inline void pthread_exit(void *value_ptr)
 #endif
   __CPROVER_threads_exited[__CPROVER_thread_id]=1;
   __CPROVER_assume(0);
+#ifdef LIBRARY_CHECK
+  __builtin_unreachable();
+#endif
 }
 
 /* FUNCTION: pthread_join */

src/ansi-c/library/setjmp.c

@@ -13,6 +13,9 @@ inline void longjmp(jmp_buf env, int val)
   (void)val;
   __CPROVER_assert(0, "longjmp requires instrumentation");
   __CPROVER_assume(0);
+#ifdef LIBRARY_CHECK
+  __builtin_unreachable();
+#endif
 }
 
 /* FUNCTION: _longjmp */
@@ -29,6 +32,9 @@ inline void _longjmp(jmp_buf env, int val)
   (void)val;
   __CPROVER_assert(0, "_longjmp requires instrumentation");
   __CPROVER_assume(0);
+#ifdef LIBRARY_CHECK
+  __builtin_unreachable();
+#endif
 }
 
 /* FUNCTION: siglongjmp */
@@ -47,6 +53,9 @@ inline void siglongjmp(sigjmp_buf env, int val)
   (void)val;
   __CPROVER_assert(0, "siglongjmp requires instrumentation");
   __CPROVER_assume(0);
+#ifdef LIBRARY_CHECK
+  __builtin_unreachable();
+#endif
 }
 
 #endif

src/ansi-c/library/stdlib.c

@@ -36,6 +36,9 @@ inline void exit(int status)
 {
   (void)status;
   __CPROVER_assume(0);
+#ifdef LIBRARY_CHECK
+  __builtin_unreachable();
+#endif
 }
 
 /* FUNCTION: _Exit */
@@ -46,6 +49,9 @@ inline void _Exit(int status)
 {
   (void)status;
   __CPROVER_assume(0);
+#ifdef LIBRARY_CHECK
+  __builtin_unreachable();
+#endif
 }
 
 /* FUNCTION: abort */
@@ -55,6 +61,9 @@ inline void _Exit(int status)
 inline void abort(void)
 {
   __CPROVER_assume(0);
+#ifdef LIBRARY_CHECK
+  __builtin_unreachable();
+#endif
 }
 
 /* FUNCTION: calloc */

src/ansi-c/library_check.sh

@@ -7,6 +7,7 @@ for f in "$@"; do
     echo "Checking ${f}"
     cp "${f}" __libcheck.c
     perl -p -i -e 's/(__builtin_[^v])/s$1/' __libcheck.c
+    perl -p -i -e 's/s(__builtin_unreachable)/$1/' __libcheck.c
     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/(__atomic_)/s$1/' __libcheck.c