+
+extern pthread_t pthread_self(void)
+ /*@*/;
+extern int pthread_equal(pthread_t t1, pthread_t t2)
+ /*@*/;
+
+extern int pthread_create(/*@out@*/ pthread_t *restrict thread,
+ const pthread_attr_t *restrict attr,
+ void *(*start_routine)(void*), void *restrict arg)
+ /*@modifies *thread @*/;
+extern int pthread_join(pthread_t thread, /*@out@*/ void **value_ptr)
+ /*@modifies *value_ptr @*/;
+
+extern int pthread_setcancelstate(int state, /*@out@*/ int *oldstate)
+ /*@globals internalState @*/
+ /*@modifies *oldstate, internalState @*/;
+extern int pthread_setcanceltype(int type, /*@out@*/ int *oldtype)
+ /*@globals internalState @*/
+ /*@modifies *oldtype, internalState @*/;
+extern void pthread_testcancel(void)
+ /*@globals internalState @*/
+ /*@modifies internalState @*/;
+extern void pthread_cleanup_pop(int execute)
+ /*@globals internalState @*/
+ /*@modifies internalState @*/;
+extern void pthread_cleanup_push(void (*routine)(void*), void *arg)
+ /*@globals internalState @*/
+ /*@modifies internalState @*/;
+extern void _pthread_cleanup_pop(/*@out@*/ struct _pthread_cleanup_buffer *__buffer, int execute)
+ /*@globals internalState @*/
+ /*@modifies internalState @*/;
+extern void _pthread_cleanup_push(/*@out@*/ struct _pthread_cleanup_buffer *__buffer, void (*routine)(void*), /*@out@*/ void *arg)
+ /*@globals internalState @*/
+ /*@modifies internalState @*/;
+
+extern int pthread_mutexattr_destroy(pthread_mutexattr_t *attr)
+ /*@modifies *attr @*/;
+extern int pthread_mutexattr_init(/*@out@*/ pthread_mutexattr_t *attr)
+ /*@modifies *attr @*/;
+
+int pthread_mutexattr_gettype(const pthread_mutexattr_t *restrict attr,
+ /*@out@*/ int *restrict type)
+ /*@modifies *type @*/;
+int pthread_mutexattr_settype(pthread_mutexattr_t *attr, int type)
+ /*@modifies *attr @*/;
+
+extern int pthread_mutex_destroy(pthread_mutex_t *mutex)
+ /*@modifies *mutex @*/;
+extern int pthread_mutex_init(/*@out@*/ pthread_mutex_t *restrict mutex,
+ const pthread_mutexattr_t *restrict attr)
+ /*@modifies *mutex @*/;
+
+extern int pthread_mutex_lock(pthread_mutex_t *mutex)
+ /*@modifies *mutex @*/;
+extern int pthread_mutex_trylock(pthread_mutex_t *mutex)
+ /*@modifies *mutex @*/;
+extern int pthread_mutex_unlock(pthread_mutex_t *mutex)
+ /*@modifies *mutex @*/;
+
+extern int pthread_cond_destroy(pthread_cond_t *cond)
+ /*@modifies *cond @*/;
+extern int pthread_cond_init(/*@out@*/ pthread_cond_t *restrict cond,
+ const pthread_condattr_t *restrict attr)
+ /*@modifies *cond @*/;
+
+extern int pthread_cond_timedwait(pthread_cond_t *restrict cond,
+ pthread_mutex_t *restrict mutex,
+ const struct timespec *restrict abstime)
+ /*@modifies *cond, *mutex @*/;
+extern int pthread_cond_wait(pthread_cond_t *restrict cond,
+ pthread_mutex_t *restrict mutex)
+ /*@modifies *cond, *mutex @*/;
+extern int pthread_cond_broadcast(pthread_cond_t *cond)
+ /*@modifies *cond @*/;
+extern int pthread_cond_signal(pthread_cond_t *cond)
+ /*@modifies *cond @*/;
+