Showing error 1467

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_7_safe.c
Line in file: 117
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    int p7 = __VERIFIER_nondet_int();  // condition variable
 23    int lk7; // lock variable
 24
 25
 26    int cond;
 27
 28    while(1) {
 29        cond = __VERIFIER_nondet_int();
 30        if (cond == 0) {
 31            goto out;
 32        } else {}
 33        lk1 = 0; // initially lock is open
 34
 35        lk2 = 0; // initially lock is open
 36
 37        lk3 = 0; // initially lock is open
 38
 39        lk4 = 0; // initially lock is open
 40
 41        lk5 = 0; // initially lock is open
 42
 43        lk6 = 0; // initially lock is open
 44
 45        lk7 = 0; // initially lock is open
 46
 47
 48    // lock phase
 49        if (p1 != 0) {
 50            lk1 = 1; // acquire lock
 51        } else {}
 52
 53        if (p2 != 0) {
 54            lk2 = 1; // acquire lock
 55        } else {}
 56
 57        if (p3 != 0) {
 58            lk3 = 1; // acquire lock
 59        } else {}
 60
 61        if (p4 != 0) {
 62            lk4 = 1; // acquire lock
 63        } else {}
 64
 65        if (p5 != 0) {
 66            lk5 = 1; // acquire lock
 67        } else {}
 68
 69        if (p6 != 0) {
 70            lk6 = 1; // acquire lock
 71        } else {}
 72
 73        if (p7 != 0) {
 74            lk7 = 1; // acquire lock
 75        } else {}
 76
 77
 78    // unlock phase
 79        if (p1 != 0) {
 80            if (lk1 != 1) goto ERROR; // assertion failure
 81            lk1 = 0;
 82        } else {}
 83
 84        if (p2 != 0) {
 85            if (lk2 != 1) goto ERROR; // assertion failure
 86            lk2 = 0;
 87        } else {}
 88
 89        if (p3 != 0) {
 90            if (lk3 != 1) goto ERROR; // assertion failure
 91            lk3 = 0;
 92        } else {}
 93
 94        if (p4 != 0) {
 95            if (lk4 != 1) goto ERROR; // assertion failure
 96            lk4 = 0;
 97        } else {}
 98
 99        if (p5 != 0) {
100            if (lk5 != 1) goto ERROR; // assertion failure
101            lk5 = 0;
102        } else {}
103
104        if (p6 != 0) {
105            if (lk6 != 1) goto ERROR; // assertion failure
106            lk6 = 0;
107        } else {}
108
109        if (p7 != 0) {
110            if (lk7 != 1) goto ERROR; // assertion failure
111            lk7 = 0;
112        } else {}
113
114    }
115  out:
116    return 0;
117  ERROR:
118    return 0;  
119}
120
↑