C library: define exactly one function per comment block

Functions from the model library are loaded upon request, and their
definitions are found as labelled by comment blocks. When adding all
these functions to a single, common symbol table we were by chance able
to also find functions other than those explicitly referenced by those
comment labels. Moving forward, however, we might not actually use a
single symbol table anymore.

Author: tautschnig

src/ansi-c/library/pthread_lib.c

@@ -531,16 +531,10 @@ inline int pthread_rwlock_wrlock(pthread_rwlock_t *lock)
   return 0; // we never fail
 }
 
-/* FUNCTION: pthread_create */
-
-#ifndef __CPROVER_PTHREAD_H_INCLUDED
-#include <pthread.h>
-#define __CPROVER_PTHREAD_H_INCLUDED
-#endif
+/* FUNCTION: __spawned_thread */
 
 extern __CPROVER_bool __CPROVER_threads_exited[];
 extern __CPROVER_thread_local unsigned long __CPROVER_thread_id;
-extern unsigned long __CPROVER_next_thread_id;
 
 extern __CPROVER_thread_local const void *__CPROVER_thread_keys[];
 extern __CPROVER_thread_local void (*__CPROVER_thread_key_dtors[])(void *);
@@ -595,6 +589,26 @@ __CPROVER_HIDE:;
   __CPROVER_threads_exited[this_thread_id] = 1;
 }
 
+/* FUNCTION: pthread_create */
+
+#ifndef __CPROVER_PTHREAD_H_INCLUDED
+#  include <pthread.h>
+#  define __CPROVER_PTHREAD_H_INCLUDED
+#endif
+
+extern unsigned long __CPROVER_next_thread_id;
+
+void __spawned_thread(
+  unsigned long this_thread_id,
+#if 0
+  // Destructor support is disabled as it is too expensive due to its extensive
+  // use of shared variables.
+  void (**thread_key_dtors)(void *),
+#endif
+  unsigned long next_thread_key,
+  void *(*start_routine)(void *),
+  void *arg);
+
 inline int pthread_create(
   pthread_t *thread, // must not be null
   const pthread_attr_t *attr, // may be null