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: 

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
Show full sources
↑