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: 

 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
20    int cond;
21
22    while(1) {
23        cond = __VERIFIER_nondet_int();
24        if (cond == 0) {
25            goto out;
26        } else {}
27        lk1 = 0; // initially lock is open
28
29        lk2 = 0; // initially lock is open
30
31        lk3 = 0; // initially lock is open
32
33        lk4 = 0; // initially lock is open
34
35        lk5 = 0; // initially lock is open
36
37
38    // lock phase
39        if (p1 != 0) {
40            lk1 = 1; // acquire lock
41        } else {}
42
43        if (p2 != 0) {
44            lk2 = 1; // acquire lock
45        } else {}
46
47        if (p3 != 0) {
48            lk3 = 1; // acquire lock
49        } else {}
50
51        if (p4 != 0) {
52            lk4 = 1; // acquire lock
53        } else {}
54
55        if (p5 != 0) {
56            lk5 = 1; // acquire lock
57        } else {}
58
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
↑