Showing error 1467

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_7_safe.c
Line in file: 117
Project: SV-COMP 2013
Project version: 2.6.28
Tools: Manual Work
Entered: 2013-01-17 16:57:54 UTC

Source: 

 87        } else {}
 88
 89        if (p3 != 0) {
 90            if (lk3 != 1) goto ERROR; // assertion failure
 91            lk3 = 0;
 92        } else {}
 93
 94        if (p4 != 0) {
 95            if (lk4 != 1) goto ERROR; // assertion failure
 96            lk4 = 0;
 97        } else {}
 98
 99        if (p5 != 0) {
100            if (lk5 != 1) goto ERROR; // assertion failure
101            lk5 = 0;
102        } else {}
103
104        if (p6 != 0) {
105            if (lk6 != 1) goto ERROR; // assertion failure
106            lk6 = 0;
107        } else {}
108
109        if (p7 != 0) {
110            if (lk7 != 1) goto ERROR; // assertion failure
111            lk7 = 0;
112        } else {}
113
114    }
115  out:
116    return 0;
117  ERROR:
118    return 0;  
119}
120
Show full sources
↑