Showing error 18

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.BUG.c
Line in file: 234
Project: SV-COMP 2012
Tools: Manual Work
Entered: 2012-11-19 13:47:39 UTC


Source:

204        } else {}
205
206        if (p11 != 0) {
207            if (lk11 != 1) goto ERROR; // assertion failure
208            lk11 = 0;
209        } else {}
210
211        if (p12 != 0) {
212            if (lk12 != 1) goto ERROR; // assertion failure
213            lk12 = 0;
214        } else {}
215
216        if (p13 != 0) {
217            if (lk13 != 1) goto ERROR; // assertion failure
218            lk13 = 0;
219        } else {}
220
221        if (p14 != 0) {
222            if (lk14 != 1) goto ERROR; // assertion failure
223            lk14 = 0;
224        } else { goto ERROR; }
225
226        if (p15 != 0) {
227            if (lk15 != 1) goto ERROR; // assertion failure
228            lk15 = 0;
229        } else {}
230
231    }
232  out:
233    return 0;
234  ERROR:
235    return 0;  
236}
237
Show full sources