625 __const void *__pointer) __attribute__ ((__nothrow__ , __leaf__)) ;
626extern int pthread_getcpuclockid (pthread_t __thread_id,
627 __clockid_t *__clock_id)
628 __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (2)));
629extern int pthread_atfork (void (*__prepare) (void),
630 void (*__parent) (void),
631 void (*__child) (void)) __attribute__ ((__nothrow__ , __leaf__));
632
633int block;
634int busy;
635int inode;
636pthread_mutex_t m_inode;
637pthread_mutex_t m_busy;
638void *allocator(){
639 pthread_mutex_lock(&m_inode);
640 if(inode == 0){
641 pthread_mutex_lock(&m_busy);
642 busy = 1;
643 pthread_mutex_unlock(&m_busy);
644 inode = 1;
645 }
646 block = 1;
647 if (!(block == 1)) ERROR: goto ERROR;;
648 pthread_mutex_unlock(&m_inode);
649 return ((void *)0);
650}
651void *de_allocator(){
652 pthread_mutex_lock(&m_busy);
653 if(busy == 0){
654 block = 0;
655 if (!(block == 0)) ERROR: goto ERROR;;
656 }
657 pthread_mutex_unlock(&m_busy);
658 return ((void *)0);
659}
660int main() {
661 pthread_t t1, t2;
662 __VERIFIER_assume(inode == busy);
663 pthread_mutex_init(&m_inode, 0);
664 pthread_mutex_init(&m_busy, 0);
665 pthread_create(&t1, 0, allocator, 0);