#include <pthread.h>
#include <errno.h>

Include dependency graph for pthread_lib.c:

Macros
#define	__CPROVER_PTHREAD_H_INCLUDED

#define	__CPROVER_mutex_t_defined

#define	__CPROVER_ERRNO_H_INCLUDED

Typedefs
typedef signed char	__CPROVER_mutex_t

Functions
int	__VERIFIER_nondet_int (void)

int	pthread_mutexattr_settype (pthread_mutexattr_t *attr, int type)

int	pthread_cancel (pthread_t thread)

int	pthread_mutex_init (pthread_mutex_t mutex, const pthread_mutexattr_t mutexattr)

int	pthread_mutex_lock (pthread_mutex_t *mutex)

int	pthread_mutex_trylock (pthread_mutex_t *mutex)

int	pthread_mutex_unlock (pthread_mutex_t *mutex)

int	pthread_mutex_destroy (pthread_mutex_t *mutex)

void	pthread_exit (void *value_ptr)

int	pthread_join (pthread_t thread, void **value_ptr)

int	pthread_rwlock_destroy (pthread_rwlock_t *lock)

int	pthread_rwlock_init (pthread_rwlock_t lock, const pthread_rwlockattr_t attr)

int	pthread_rwlock_rdlock (pthread_rwlock_t *lock)

int	pthread_rwlock_tryrdlock (pthread_rwlock_t *lock)

int	pthread_rwlock_trywrlock (pthread_rwlock_t *lock)

int	pthread_rwlock_unlock (pthread_rwlock_t *lock)

int	pthread_rwlock_wrlock (pthread_rwlock_t *lock)

void	__spawned_thread (unsigned long this_thread_id, unsigned long next_thread_key, void (start_routine)(void ), void arg)

int	pthread_create (pthread_t thread, const pthread_attr_t attr, void (start_routine)(void ), void arg)

int	pthread_cond_init (pthread_cond_t cond, const pthread_condattr_t attr)

int	pthread_cond_signal (pthread_cond_t *cond)

int	pthread_cond_broadcast (pthread_cond_t *cond)

int	pthread_cond_wait (pthread_cond_t cond, pthread_mutex_t mutex)

int	pthread_spin_lock (pthread_spinlock_t *lock)

int	pthread_spin_unlock (pthread_spinlock_t *lock)

int	pthread_spin_trylock (pthread_spinlock_t *lock)

int	pthread_barrier_init (pthread_barrier_t restrict barrier, const pthread_barrierattr_t restrict attr, unsigned count)

int	pthread_barrier_destroy (pthread_barrier_t *barrier)

int	pthread_barrier_wait (pthread_barrier_t *barrier)

int	pthread_key_create (pthread_key_t key, void(destructor)(void *))

int	pthread_key_delete (pthread_key_t key)

void *	pthread_getspecific (pthread_key_t key)

int	pthread_setspecific (pthread_key_t key, const void *value)

Variables
__CPROVER_bool	__CPROVER_threads_exited [__CPROVER_constant_infinity_uint]

__CPROVER_thread_local unsigned long	__CPROVER_thread_id = 0

unsigned long	__CPROVER_next_thread_id = 0

__CPROVER_thread_local unsigned long	__CPROVER_next_thread_key = 0

__CPROVER_thread_local const void *	__CPROVER_thread_keys [__CPROVER_constant_infinity_uint]

Macro Definition Documentation

◆ __CPROVER_ERRNO_H_INCLUDED

#define __CPROVER_ERRNO_H_INCLUDED

Definition at line 337 of file pthread_lib.c.

◆ __CPROVER_mutex_t_defined

#define __CPROVER_mutex_t_defined

Definition at line 57 of file pthread_lib.c.

◆ __CPROVER_PTHREAD_H_INCLUDED

#define __CPROVER_PTHREAD_H_INCLUDED

Definition at line 5 of file pthread_lib.c.

Typedef Documentation

◆ __CPROVER_mutex_t

typedef signed char __CPROVER_mutex_t

Definition at line 62 of file pthread_lib.c.

Function Documentation

◆ __spawned_thread()

void __spawned_thread	(	unsigned long	this_thread_id,
		unsigned long	next_thread_key,
		void ()(void *)	start_routine,
		void *	arg
	)

Definition at line 561 of file pthread_lib.c.

◆ __VERIFIER_nondet_int()

int __VERIFIER_nondet_int ( void )

◆ pthread_barrier_destroy()

int pthread_barrier_destroy ( pthread_barrier_t * barrier )

Definition at line 900 of file pthread_lib.c.

◆ pthread_barrier_init()

int pthread_barrier_init	(	pthread_barrier_t *restrict	barrier,
		const pthread_barrierattr_t *restrict	attr,
		unsigned	count
	)

Definition at line 847 of file pthread_lib.c.

◆ pthread_barrier_wait()

int pthread_barrier_wait ( pthread_barrier_t * barrier )

Definition at line 930 of file pthread_lib.c.

◆ pthread_cancel()

int pthread_cancel ( pthread_t thread )

Definition at line 35 of file pthread_lib.c.

◆ pthread_cond_broadcast()

int pthread_cond_broadcast ( pthread_cond_t * cond )

Definition at line 716 of file pthread_lib.c.

◆ pthread_cond_init()

int pthread_cond_init	(	pthread_cond_t *	cond,
		const pthread_condattr_t *	attr
	)

Definition at line 687 of file pthread_lib.c.

◆ pthread_cond_signal()

int pthread_cond_signal ( pthread_cond_t * cond )

Definition at line 701 of file pthread_lib.c.

◆ pthread_cond_wait()

int pthread_cond_wait	(	pthread_cond_t *	cond,
		pthread_mutex_t *	mutex
	)

Definition at line 731 of file pthread_lib.c.

◆ pthread_create()

int pthread_create	(	pthread_t *	thread,
		const pthread_attr_t *	attr,
		void ()(void *)	start_routine,
		void *	arg
	)

Definition at line 637 of file pthread_lib.c.

◆ pthread_exit()

void pthread_exit ( void * value_ptr )

Definition at line 306 of file pthread_lib.c.

◆ pthread_getspecific()

void* pthread_getspecific ( pthread_key_t key )

Definition at line 1007 of file pthread_lib.c.

◆ pthread_join()

int pthread_join	(	pthread_t	thread,
		void **	value_ptr
	)

Definition at line 346 of file pthread_lib.c.

◆ pthread_key_create()

int pthread_key_create	(	pthread_key_t *	key,
		void()(void )	destructor
	)

Definition at line 965 of file pthread_lib.c.

◆ pthread_key_delete()

int pthread_key_delete ( pthread_key_t key )

Definition at line 990 of file pthread_lib.c.

◆ pthread_mutex_destroy()

int pthread_mutex_destroy ( pthread_mutex_t * mutex )

Definition at line 260 of file pthread_lib.c.

◆ pthread_mutex_init()

int pthread_mutex_init	(	pthread_mutex_t *	mutex,
		const pthread_mutexattr_t *	mutexattr
	)

Definition at line 76 of file pthread_lib.c.

◆ pthread_mutex_lock()

int pthread_mutex_lock ( pthread_mutex_t * mutex )

Definition at line 112 of file pthread_lib.c.

◆ pthread_mutex_trylock()

int pthread_mutex_trylock ( pthread_mutex_t * mutex )

Definition at line 161 of file pthread_lib.c.

◆ pthread_mutex_unlock()

int pthread_mutex_unlock ( pthread_mutex_t * mutex )

Definition at line 212 of file pthread_lib.c.

◆ pthread_mutexattr_settype()

int pthread_mutexattr_settype	(	pthread_mutexattr_t *	attr,
		int	type
	)

Definition at line 10 of file pthread_lib.c.

◆ pthread_rwlock_destroy()

int pthread_rwlock_destroy ( pthread_rwlock_t * lock )

Definition at line 411 of file pthread_lib.c.

◆ pthread_rwlock_init()

int pthread_rwlock_init	(	pthread_rwlock_t *	lock,
		const pthread_rwlockattr_t *	attr
	)

Definition at line 441 of file pthread_lib.c.

◆ pthread_rwlock_rdlock()

int pthread_rwlock_rdlock ( pthread_rwlock_t * lock )

Definition at line 463 of file pthread_lib.c.

◆ pthread_rwlock_tryrdlock()

int pthread_rwlock_tryrdlock ( pthread_rwlock_t * lock )

Definition at line 482 of file pthread_lib.c.

◆ pthread_rwlock_trywrlock()

int pthread_rwlock_trywrlock ( pthread_rwlock_t * lock )

Definition at line 499 of file pthread_lib.c.

◆ pthread_rwlock_unlock()

int pthread_rwlock_unlock ( pthread_rwlock_t * lock )

Definition at line 516 of file pthread_lib.c.

◆ pthread_rwlock_wrlock()

int pthread_rwlock_wrlock ( pthread_rwlock_t * lock )

Definition at line 533 of file pthread_lib.c.

◆ pthread_setspecific()

int pthread_setspecific	(	pthread_key_t	key,
		const void *	value
	)

Definition at line 1023 of file pthread_lib.c.

◆ pthread_spin_lock()

int pthread_spin_lock ( pthread_spinlock_t * lock )

Definition at line 766 of file pthread_lib.c.

◆ pthread_spin_trylock()

int pthread_spin_trylock ( pthread_spinlock_t * lock )

Definition at line 815 of file pthread_lib.c.

◆ pthread_spin_unlock()

int pthread_spin_unlock ( pthread_spinlock_t * lock )

Definition at line 789 of file pthread_lib.c.

Variable Documentation

◆ __CPROVER_next_thread_id

unsigned long __CPROVER_next_thread_id = 0

Definition at line 344 of file pthread_lib.c.

◆ __CPROVER_next_thread_key

__CPROVER_thread_local unsigned long __CPROVER_next_thread_key = 0

Definition at line 559 of file pthread_lib.c.

◆ __CPROVER_thread_id

__CPROVER_thread_local unsigned long __CPROVER_thread_id = 0

Definition at line 295 of file pthread_lib.c.

◆ __CPROVER_thread_keys

__CPROVER_thread_local const void * __CPROVER_thread_keys

Definition at line 956 of file pthread_lib.c.

◆ __CPROVER_threads_exited

__CPROVER_bool __CPROVER_threads_exited

Definition at line 294 of file pthread_lib.c.

Macros

Typedefs

Functions

Variables