Showing error 1466

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

Source: 

  1extern int __VERIFIER_nondet_int();
  2int main()
  3{
  4    int p1 = __VERIFIER_nondet_int();  // condition variable
  5    int lk1; // lock variable
  6
  7    int p2 = __VERIFIER_nondet_int();  // condition variable
  8    int lk2; // lock variable
  9
 10    int p3 = __VERIFIER_nondet_int();  // condition variable
 11    int lk3; // lock variable
 12
 13    int p4 = __VERIFIER_nondet_int();  // condition variable
 14    int lk4; // lock variable
 15
 16    int p5 = __VERIFIER_nondet_int();  // condition variable
 17    int lk5; // lock variable
 18
 19    int p6 = __VERIFIER_nondet_int();  // condition variable
 20    int lk6; // lock variable
 21
 22
 23    int cond;
 24
 25    while(1) {
 26        cond = __VERIFIER_nondet_int();
 27        if (cond == 0) {
 28            goto out;
 29        } else {}
 30        lk1 = 0; // initially lock is open
 31
 32        lk2 = 0; // initially lock is open
 33
 34        lk3 = 0; // initially lock is open
 35
 36        lk4 = 0; // initially lock is open
 37
 38        lk5 = 0; // initially lock is open
 39
 40        lk6 = 0; // initially lock is open
 41
 42
 43    // lock phase
 44        if (p1 != 0) {
 45            lk1 = 1; // acquire lock
 46        } else {}
 47
 48        if (p2 != 0) {
 49            lk2 = 1; // acquire lock
 50        } else {}
 51
 52        if (p3 != 0) {
 53            lk3 = 1; // acquire lock
 54        } else {}
 55
 56        if (p4 != 0) {
 57            lk4 = 1; // acquire lock
 58        } else {}
 59
 60        if (p5 != 0) {
 61            lk5 = 1; // acquire lock
 62        } else {}
 63
 64        if (p6 != 0) {
 65            lk6 = 1; // acquire lock
 66        } else {}
 67
 68
 69    // unlock phase
 70        if (p1 != 0) {
 71            if (lk1 != 1) goto ERROR; // assertion failure
 72            lk1 = 0;
 73        } else {}
 74
 75        if (p2 != 0) {
 76            if (lk2 != 1) goto ERROR; // assertion failure
 77            lk2 = 0;
 78        } else {}
 79
 80        if (p3 != 0) {
 81            if (lk3 != 1) goto ERROR; // assertion failure
 82            lk3 = 0;
 83        } else {}
 84
 85        if (p4 != 0) {
 86            if (lk4 != 1) goto ERROR; // assertion failure
 87            lk4 = 0;
 88        } else {}
 89
 90        if (p5 != 0) {
 91            if (lk5 != 1) goto ERROR; // assertion failure
 92            lk5 = 0;
 93        } else {}
 94
 95        if (p6 != 0) {
 96            if (lk6 != 1) goto ERROR; // assertion failure
 97            lk6 = 0;
 98        } else {}
 99
100    }
101  out:
102    return 0;
103  ERROR:
104    return 0;  
105}
106
↑