semaphore_lib.c File Reference

#include <semaphore.h>
#include <limits.h>
#include <pthread.h>

Include dependency graph for semaphore_lib.c:

Macros
#define	__ESBMC_sem_lock_field(a)
#define	__ESBMC_sem_count_field(a)
#define	__ESBMC_sem_init_field(a)
#define	__ESBMC_sem_waiters(a)

Functions
void	__ESBMC_release_blocked_threads (unsigned int waiters)
int	sem_init (sem_t *__sem, int __pshared, unsigned int __value)
static int	sem_init_check (sem_t *__sem)
int	sem_wait_check (sem_t *__sem)
int	sem_wait_nocheck (sem_t *__sem)
int	sem_post (sem_t *__sem)
int	sem_destroy (sem_t *__sem)

Variables
unsigned short int	__ESBMC_num_threads_running
unsigned short int	__ESBMC_blocked_threads_count

Macro Definition Documentation

__ESBMC_sem_count_field

#define __ESBMC_sem_count_field

(

a

)

Value:

((a).__count)

__ESBMC_sem_init_field

#define __ESBMC_sem_init_field

(

a

)

Value:

((a).__init)

__ESBMC_sem_lock_field

#define __ESBMC_sem_lock_field

(

a

)

Value:

((a).__lock)

__ESBMC_sem_waiters

#define __ESBMC_sem_waiters

(

a

)

Value:

((a).__waiters)

Function Documentation

__ESBMC_release_blocked_threads()

void __ESBMC_release_blocked_threads ( unsigned int waiters )

extern

sem_destroy()

int sem_destroy

(

sem_t *

__sem

)

sem_init()

int sem_init	(	sem_t *	__sem,
		int	__pshared,
		unsigned int	__value )

sem_init_check()

int sem_init_check ( sem_t * __sem )

static

sem_post()

int sem_post

(

sem_t *

__sem

)

sem_wait_check()

int sem_wait_check

(

sem_t *

__sem

)

sem_wait_nocheck()

int sem_wait_nocheck

(

sem_t *

__sem

)

Variable Documentation

__ESBMC_blocked_threads_count

unsigned short int __ESBMC_blocked_threads_count

extern

__ESBMC_num_threads_running

unsigned short int __ESBMC_num_threads_running

extern