Showing error 2167

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


Source:

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 x, y;
634int b1, b2;
635int X;
636void *thr1() {
637  while (1) {
638    b1 = 1;
639    x = 1;
640    if (y != 0) {
641      b1 = 0;
642      while (y != 0) {};
643      continue;
644    }
645    y = 1;
646    if (x != 1) {
647      b1 = 0;
648      while (b2 >= 1) {};
649      if (y != 1) {
650 while (y != 0) {};
651 continue;
652      }
653    }
654    break;
655  }
656  X = 0;
657  if (!(X <= 0)) ERROR: goto ERROR;;
658  y = 0;
659  b1 = 0;
660}
661void *thr2() {
662  while (1) {
663    b2 = 1;
664    x = 2;
665    if (y != 0) {
666      b2 = 0;
667      while (y != 0) {};
Show full sources