Showing error 1464

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