Showing error 2169

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/peterson_safe.i
Line in file: 641
Project: SV-COMP 2013
Project version: 2.6.28
Tools: Manual Work
Entered: 2013-01-17 16:57:54 UTC


Source:

611     __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1)));
612extern int pthread_barrierattr_getpshared (__const pthread_barrierattr_t *
613        __restrict __attr,
614        int *__restrict __pshared)
615     __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1, 2)));
616extern int pthread_barrierattr_setpshared (pthread_barrierattr_t *__attr,
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 flag1 = 0, flag2 = 0;
634int turn;
635int x;
636void *thr1() {
637  flag1 = 1;
638  turn = 1;
639  while (flag2==1 && turn==1) {};
640  x = 0;
641  if (!(x<=0)) ERROR: goto ERROR;;
642  flag1 = 0;
643}
644void *thr2() {
645  flag2 = 1;
646  turn = 0;
647  while (flag1==1 && turn==0) {};
648  x = 1;
649  if (!(x>=1)) ERROR: goto ERROR;;
650  flag2 = 0;
651}
Show full sources