Showing error 1469

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