Showing error 1465

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

Source: 

59
60    // unlock phase
61        if (p1 != 0) {
62            if (lk1 != 1) goto ERROR; // assertion failure
63            lk1 = 0;
64        } else {}
65
66        if (p2 != 0) {
67            if (lk2 != 1) goto ERROR; // assertion failure
68            lk2 = 0;
69        } else {}
70
71        if (p3 != 0) {
72            if (lk3 != 1) goto ERROR; // assertion failure
73            lk3 = 0;
74        } else {}
75
76        if (p4 != 0) {
77            if (lk4 != 1) goto ERROR; // assertion failure
78            lk4 = 0;
79        } else {}
80
81        if (p5 != 0) {
82            if (lk5 != 1) goto ERROR; // assertion failure
83            lk5 = 0;
84        } else {}
85
86    }
87  out:
88    return 0;
89  ERROR:
90    return 0;  
91}
92
Show full sources
↑