Showing error 1460

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_13_safe.c
Line in file: 201
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    int p10 = __VERIFIER_nondet_int();  // condition variable
 32    int lk10; // lock variable
 33
 34    int p11 = __VERIFIER_nondet_int();  // condition variable
 35    int lk11; // lock variable
 36
 37    int p12 = __VERIFIER_nondet_int();  // condition variable
 38    int lk12; // lock variable
 39
 40    int p13 = __VERIFIER_nondet_int();  // condition variable
 41    int lk13; // lock variable
 42
 43
 44    int cond;
 45
 46    while(1) {
 47        cond = __VERIFIER_nondet_int();
 48        if (cond == 0) {
 49            goto out;
 50        } else {}
 51        lk1 = 0; // initially lock is open
 52
 53        lk2 = 0; // initially lock is open
 54
 55        lk3 = 0; // initially lock is open
 56
 57        lk4 = 0; // initially lock is open
 58
 59        lk5 = 0; // initially lock is open
 60
 61        lk6 = 0; // initially lock is open
 62
 63        lk7 = 0; // initially lock is open
 64
 65        lk8 = 0; // initially lock is open
 66
 67        lk9 = 0; // initially lock is open
 68
 69        lk10 = 0; // initially lock is open
 70
 71        lk11 = 0; // initially lock is open
 72
 73        lk12 = 0; // initially lock is open
 74
 75        lk13 = 0; // initially lock is open
 76
 77
 78    // lock phase
 79        if (p1 != 0) {
 80            lk1 = 1; // acquire lock
 81        } else {}
 82
 83        if (p2 != 0) {
 84            lk2 = 1; // acquire lock
 85        } else {}
 86
 87        if (p3 != 0) {
 88            lk3 = 1; // acquire lock
 89        } else {}
 90
 91        if (p4 != 0) {
 92            lk4 = 1; // acquire lock
 93        } else {}
 94
 95        if (p5 != 0) {
 96            lk5 = 1; // acquire lock
 97        } else {}
 98
 99        if (p6 != 0) {
100            lk6 = 1; // acquire lock
101        } else {}
102
103        if (p7 != 0) {
104            lk7 = 1; // acquire lock
105        } else {}
106
107        if (p8 != 0) {
108            lk8 = 1; // acquire lock
109        } else {}
110
111        if (p9 != 0) {
112            lk9 = 1; // acquire lock
113        } else {}
114
115        if (p10 != 0) {
116            lk10 = 1; // acquire lock
117        } else {}
118
119        if (p11 != 0) {
120            lk11 = 1; // acquire lock
121        } else {}
122
123        if (p12 != 0) {
124            lk12 = 1; // acquire lock
125        } else {}
126
127        if (p13 != 0) {
128            lk13 = 1; // acquire lock
129        } else {}
130
131
132    // unlock phase
133        if (p1 != 0) {
134            if (lk1 != 1) goto ERROR; // assertion failure
135            lk1 = 0;
136        } else {}
137
138        if (p2 != 0) {
139            if (lk2 != 1) goto ERROR; // assertion failure
140            lk2 = 0;
141        } else {}
142
143        if (p3 != 0) {
144            if (lk3 != 1) goto ERROR; // assertion failure
145            lk3 = 0;
146        } else {}
147
148        if (p4 != 0) {
149            if (lk4 != 1) goto ERROR; // assertion failure
150            lk4 = 0;
151        } else {}
152
153        if (p5 != 0) {
154            if (lk5 != 1) goto ERROR; // assertion failure
155            lk5 = 0;
156        } else {}
157
158        if (p6 != 0) {
159            if (lk6 != 1) goto ERROR; // assertion failure
160            lk6 = 0;
161        } else {}
162
163        if (p7 != 0) {
164            if (lk7 != 1) goto ERROR; // assertion failure
165            lk7 = 0;
166        } else {}
167
168        if (p8 != 0) {
169            if (lk8 != 1) goto ERROR; // assertion failure
170            lk8 = 0;
171        } else {}
172
173        if (p9 != 0) {
174            if (lk9 != 1) goto ERROR; // assertion failure
175            lk9 = 0;
176        } else {}
177
178        if (p10 != 0) {
179            if (lk10 != 1) goto ERROR; // assertion failure
180            lk10 = 0;
181        } else {}
182
183        if (p11 != 0) {
184            if (lk11 != 1) goto ERROR; // assertion failure
185            lk11 = 0;
186        } else {}
187
188        if (p12 != 0) {
189            if (lk12 != 1) goto ERROR; // assertion failure
190            lk12 = 0;
191        } else {}
192
193        if (p13 != 0) {
194            if (lk13 != 1) goto ERROR; // assertion failure
195            lk13 = 0;
196        } else {}
197
198    }
199  out:
200    return 0;
201  ERROR:
202    return 0;  
203}
204
↑