Showing error 2182

User: Jiri Slaby
Error type: Reachable Error Location
Error type description: A specified error location is reachable in some program path
File location: pthread-atomic/time_var_mutex_safe.i
Line in file: 647
Project: SV-COMP 2013
Project version: 2.6.28
Tools: Manual Work
Entered: 2013-01-17 16:57:54 UTC


Source:

617        int __pshared)
618     __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1)));
619extern int pthread_key_create (pthread_key_t *__key,
620          void (*__destr_function) (void *))
621     __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1)));
622extern int pthread_key_delete (pthread_key_t __key) __attribute__ ((__nothrow__ , __leaf__));
623extern void *pthread_getspecific (pthread_key_t __key) __attribute__ ((__nothrow__ , __leaf__));
624extern int pthread_setspecific (pthread_key_t __key,
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);
Show full sources