Showing error 20

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

Source: 

 1int get_exit_nondet()
 2{
 3    int retval;
 4    return (retval);
 5}
 6
 7int main()
 8{
 9    int p1;  // condition variable
10    int lk1; // lock variable
11
12    int p2;  // condition variable
13    int lk2; // lock variable
14
15    int p3;  // condition variable
16    int lk3; // lock variable
17
18    int p4;  // condition variable
19    int lk4; // lock variable
20
21    int p5;  // condition variable
22    int lk5; // lock variable
23
24
25    int cond;
26
27    while(1) {
28        cond = get_exit_nondet();
29        if (cond == 0) {
30            goto out;
31        } else {}
32        lk1 = 0; // initially lock is open
33
34        lk2 = 0; // initially lock is open
35
36        lk3 = 0; // initially lock is open
37
38        lk4 = 0; // initially lock is open
39
40        lk5 = 0; // initially lock is open
41
42
43    // lock phase
44        if (p1 != 0) {
45            lk1 = 1; // acquire lock
46        } else {}
47
48        if (p2 != 0) {
49            lk2 = 1; // acquire lock
50        } else {}
51
52        if (p3 != 0) {
53            lk3 = 1; // acquire lock
54        } else {}
55
56        if (p4 != 0) {
57            lk4 = 1; // acquire lock
58        } else {}
59
60        if (p5 != 0) {
61            lk5 = 1; // acquire lock
62        } else {}
63
64
65    // unlock phase
66        if (p1 != 0) {
67            if (lk1 != 1) goto ERROR; // assertion failure
68            lk1 = 0;
69        } else {}
70
71        if (p2 != 0) {
72            if (lk2 != 1) goto ERROR; // assertion failure
73            lk2 = 0;
74        } else {}
75
76        if (p3 != 0) {
77            if (lk3 != 1) goto ERROR; // assertion failure
78            lk3 = 0;
79        } else {}
80
81        if (p4 != 0) {
82            if (lk4 != 1) goto ERROR; // assertion failure
83            lk4 = 0;
84        } else {}
85
86        if (p5 != 0) {
87            if (lk5 != 1) goto ERROR; // assertion failure
88            lk5 = 0;
89        } else {}
90
91    }
92  out:
93    return 0;
94  ERROR:
95    return 0;  
96}
97
↑