Showing error 18

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.BUG.c
Line in file: 234
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    int p6;  // condition variable
 25    int lk6; // lock variable
 26
 27    int p7;  // condition variable
 28    int lk7; // lock variable
 29
 30    int p8;  // condition variable
 31    int lk8; // lock variable
 32
 33    int p9;  // condition variable
 34    int lk9; // lock variable
 35
 36    int p10;  // condition variable
 37    int lk10; // lock variable
 38
 39    int p11;  // condition variable
 40    int lk11; // lock variable
 41
 42    int p12;  // condition variable
 43    int lk12; // lock variable
 44
 45    int p13;  // condition variable
 46    int lk13; // lock variable
 47
 48    int p14;  // condition variable
 49    int lk14; // lock variable
 50
 51    int p15;  // condition variable
 52    int lk15; // lock variable
 53
 54
 55    int cond;
 56
 57    while(1) {
 58        cond = nondet_int();
 59        if (cond == 0) {
 60            goto out;
 61        } else {}
 62        lk1 = 0; // initially lock is open
 63
 64        lk2 = 0; // initially lock is open
 65
 66        lk3 = 0; // initially lock is open
 67
 68        lk4 = 0; // initially lock is open
 69
 70        lk5 = 0; // initially lock is open
 71
 72        lk6 = 0; // initially lock is open
 73
 74        lk7 = 0; // initially lock is open
 75
 76        lk8 = 0; // initially lock is open
 77
 78        lk9 = 0; // initially lock is open
 79
 80        lk10 = 0; // initially lock is open
 81
 82        lk11 = 0; // initially lock is open
 83
 84        lk12 = 0; // initially lock is open
 85
 86        lk13 = 0; // initially lock is open
 87
 88        lk14 = 0; // initially lock is open
 89
 90        lk15 = 0; // initially lock is open
 91
 92
 93    // lock phase
 94        if (p1 != 0) {
 95            lk1 = 1; // acquire lock
 96        } else {}
 97
 98        if (p2 != 0) {
 99            lk2 = 1; // acquire lock
100        } else {}
101
102        if (p3 != 0) {
103            lk3 = 1; // acquire lock
104        } else {}
105
106        if (p4 != 0) {
107            lk4 = 1; // acquire lock
108        } else {}
109
110        if (p5 != 0) {
111            lk5 = 1; // acquire lock
112        } else {}
113
114        if (p6 != 0) {
115            lk6 = 1; // acquire lock
116        } else {}
117
118        if (p7 != 0) {
119            lk7 = 1; // acquire lock
120        } else {}
121
122        if (p8 != 0) {
123            lk8 = 1; // acquire lock
124        } else {}
125
126        if (p9 != 0) {
127            lk9 = 1; // acquire lock
128        } else {}
129
130        if (p10 != 0) {
131            lk10 = 1; // acquire lock
132        } else {}
133
134        if (p11 != 0) {
135            lk11 = 1; // acquire lock
136        } else {}
137
138        if (p12 != 0) {
139            lk12 = 1; // acquire lock
140        } else {}
141
142        if (p13 != 0) {
143            lk13 = 1; // acquire lock
144        } else {}
145
146        if (p14 != 0) {
147            lk14 = 1; // acquire lock
148        } else {}
149
150        if (p15 != 0) {
151            lk15 = 1; // acquire lock
152        } else {}
153
154
155    // unlock phase
156        if (p1 != 0) {
157            if (lk1 != 1) goto ERROR; // assertion failure
158            lk1 = 0;
159        } else {}
160
161        if (p2 != 0) {
162            if (lk2 != 1) goto ERROR; // assertion failure
163            lk2 = 0;
164        } else { goto ERROR; }
165
166        if (p3 != 0) {
167            if (lk3 != 1) goto ERROR; // assertion failure
168            lk3 = 0;
169        } else {}
170
171        if (p4 != 0) {
172            if (lk4 != 1) goto ERROR; // assertion failure
173            lk4 = 0;
174        } else {}
175
176        if (p5 != 0) {
177            if (lk5 != 1) goto ERROR; // assertion failure
178            lk5 = 0;
179        } else {}
180
181        if (p6 != 0) {
182            if (lk6 != 1) goto ERROR; // assertion failure
183            lk6 = 0;
184        } else {}
185
186        if (p7 != 0) {
187            if (lk7 != 1) goto ERROR; // assertion failure
188            lk7 = 0;
189        } else {}
190
191        if (p8 != 0) {
192            if (lk8 != 1) goto ERROR; // assertion failure
193            lk8 = 0;
194        } else {}
195
196        if (p9 != 0) {
197            if (lk9 != 1) goto ERROR; // assertion failure
198            lk9 = 0;
199        } else {}
200
201        if (p10 != 0) {
202            if (lk10 != 1) goto ERROR; // assertion failure
203            lk10 = 0;
204        } else {}
205
206        if (p11 != 0) {
207            if (lk11 != 1) goto ERROR; // assertion failure
208            lk11 = 0;
209        } else {}
210
211        if (p12 != 0) {
212            if (lk12 != 1) goto ERROR; // assertion failure
213            lk12 = 0;
214        } else {}
215
216        if (p13 != 0) {
217            if (lk13 != 1) goto ERROR; // assertion failure
218            lk13 = 0;
219        } else {}
220
221        if (p14 != 0) {
222            if (lk14 != 1) goto ERROR; // assertion failure
223            lk14 = 0;
224        } else { goto ERROR; }
225
226        if (p15 != 0) {
227            if (lk15 != 1) goto ERROR; // assertion failure
228            lk15 = 0;
229        } else {}
230
231    }
232  out:
233    return 0;
234  ERROR:
235    return 0;  
236}
237
↑