Showing error 1505

User: Jiri Slaby
Error type: Reachable Error Location
Error type description: A specified error location is reachable in some program path
File location: loops/pc_sfifo_2_unsafe.i
Line in file: 7
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();
  2void error(void)
  3{
  4
  5  {
  6  goto ERROR;
  7  ERROR: ;
  8  return;
  9}
 10}
 11
 12int q_buf_0 ;
 13int q_free ;
 14int q_read_ev ;
 15int q_write_ev ;
 16int q_req_up ;
 17int q_ev ;
 18void update_fifo_q(void)
 19{
 20
 21  {
 22  if ((int )q_free == 0) {
 23    q_write_ev = 0;
 24  } else {
 25
 26  }
 27  if ((int )q_free == 1) {
 28    q_read_ev = 0;
 29  } else {
 30
 31  }
 32  q_ev = 0;
 33  q_req_up = 0;
 34
 35  return;
 36}
 37}
 38int p_num_write ;
 39int p_last_write ;
 40int p_dw_st ;
 41int p_dw_pc ;
 42int p_dw_i ;
 43int c_num_read ;
 44int c_last_read ;
 45int c_dr_st ;
 46int c_dr_pc ;
 47int c_dr_i ;
 48int is_do_write_p_triggered(void)
 49{ int __retres1 ;
 50
 51  {
 52  if ((int )p_dw_pc == 1) {
 53    if ((int )q_read_ev == 1) {
 54      __retres1 = 1;
 55      goto return_label;
 56    } else {
 57
 58    }
 59  } else {
 60
 61  }
 62  __retres1 = 0;
 63  return_label:
 64  return (__retres1);
 65}
 66}
 67int is_do_read_c_triggered(void)
 68{ int __retres1 ;
 69
 70  {
 71  if ((int )c_dr_pc == 1) {
 72    if ((int )q_write_ev == 1) {
 73      __retres1 = 1;
 74      goto return_label;
 75    } else {
 76
 77    }
 78  } else {
 79
 80  }
 81  __retres1 = 0;
 82  return_label:
 83  return (__retres1);
 84}
 85}
 86void immediate_notify_threads(void)
 87{ int tmp ;
 88  int tmp___0 ;
 89
 90  {
 91  {
 92  tmp = is_do_write_p_triggered();
 93  }
 94  if (tmp) {
 95    p_dw_st = 0;
 96  } else {
 97
 98  }
 99  {
100  tmp___0 = is_do_read_c_triggered();
101  }
102  if (tmp___0) {
103    c_dr_st = 0;
104  } else {
105
106  }
107
108  return;
109}
110}
111void do_write_p(void)
112{
113
114
115  {
116  if ((int )p_dw_pc == 0) {
117    goto DW_ENTRY;
118  } else {
119    if ((int )p_dw_pc == 1) {
120      goto DW_WAIT_READ;
121    } else {
122
123    }
124  }
125  DW_ENTRY:
126  {
127  while (1) {
128    while_0_continue: ;
129    if ((int )q_free == 0) {
130      p_dw_st = 2;
131      p_dw_pc = 1;
132
133      goto return_label;
134      DW_WAIT_READ: ;
135    } else {
136
137    }
138    {
139      q_buf_0 = __VERIFIER_nondet_int();
140    p_last_write = q_buf_0;
141    p_num_write += 1;
142    q_free = 0;
143    q_req_up = 1;
144    }
145  }
146  while_0_break: ;
147  }
148  return_label:
149  return;
150}
151}
152static int a_t ;
153void do_read_c(void)
154{ int a ;
155
156  {
157  if ((int )c_dr_pc == 0) {
158    goto DR_ENTRY;
159  } else {
160    if ((int )c_dr_pc == 1) {
161      goto DR_WAIT_WRITE;
162    } else {
163
164    }
165  }
166  DR_ENTRY:
167  {
168  while (1) {
169    while_1_continue: ;
170    if ((int )q_free == 1) {
171      c_dr_st = 2;
172      c_dr_pc = 1;
173      a_t = a;
174
175      goto return_label;
176      DR_WAIT_WRITE:
177      a = a_t;
178    } else {
179
180    }
181    a = q_buf_0;
182    c_last_read = a;
183    c_num_read += 1;
184    q_free = 1;
185    q_req_up = 1;
186    if (p_last_write == c_last_read) {
187      if (p_num_write == c_num_read) {
188
189      } else {
190        {
191        error();
192        }
193      }
194    } else {
195      {
196      error();
197      }
198    }
199  }
200  while_1_break: ;
201  }
202  return_label:
203  return;
204}
205}
206void update_channels(void)
207{
208
209  {
210  if ((int )q_req_up == 1) {
211    {
212    update_fifo_q();
213    }
214  } else {
215
216  }
217
218  return;
219}
220}
221void init_threads(void)
222{
223
224  {
225  if ((int )p_dw_i == 1) {
226    p_dw_st = 0;
227  } else {
228    p_dw_st = 2;
229  }
230  if ((int )c_dr_i == 1) {
231    c_dr_st = 0;
232  } else {
233    c_dr_st = 2;
234  }
235
236  return;
237}
238}
239int exists_runnable_thread(void)
240{ int __retres1 ;
241
242  {
243  if ((int )p_dw_st == 0) {
244    __retres1 = 1;
245    goto return_label;
246  } else {
247    if ((int )c_dr_st == 0) {
248      __retres1 = 1;
249      goto return_label;
250    } else {
251
252    }
253  }
254  __retres1 = 0;
255  return_label:
256  return (__retres1);
257}
258}
259void fire_delta_events(void)
260{
261
262  {
263  if ((int )q_read_ev == 0) {
264    q_read_ev = 1;
265  } else {
266
267  }
268  if ((int )q_write_ev == 0) {
269    q_write_ev = 1;
270  } else {
271
272  }
273
274  return;
275}
276}
277void reset_delta_events(void)
278{
279
280  {
281  if ((int )q_read_ev == 1) {
282    q_read_ev = 2;
283  } else {
284
285  }
286  if ((int )q_write_ev == 1) {
287    q_write_ev = 2;
288  } else {
289
290  }
291
292  return;
293}
294}
295void activate_threads(void)
296{ int tmp ;
297  int tmp___0 ;
298
299  {
300  {
301  tmp = is_do_write_p_triggered();
302  }
303  if (tmp) {
304    p_dw_st = 0;
305  } else {
306
307  }
308  {
309  tmp___0 = is_do_read_c_triggered();
310  }
311  if (tmp___0) {
312    c_dr_st = 0;
313  } else {
314
315  }
316
317  return;
318}
319}
320void eval(void)
321{ int tmp ;
322  int tmp___0 ;
323  int tmp___1 ;
324
325
326  {
327  {
328  while (1) {
329    while_2_continue: ;
330    {
331    tmp___1 = exists_runnable_thread();
332    }
333    if (tmp___1) {
334
335    } else {
336      goto while_2_break;
337    }
338    if ((int )p_dw_st == 0) {
339      {
340 tmp = __VERIFIER_nondet_int();
341      }
342      if (tmp) {
343        {
344        p_dw_st = 1;
345        do_write_p();
346        }
347      } else {
348 error();
349      }
350    } else {
351
352    }
353    if ((int )c_dr_st == 0) {
354      {
355 tmp___0 = __VERIFIER_nondet_int();
356      }
357      if (tmp___0) {
358        {
359        c_dr_st = 1;
360        do_read_c();
361        }
362      } else {
363
364      }
365    } else {
366
367    }
368  }
369  while_2_break: ;
370  }
371
372  return;
373}
374}
375int stop_simulation(void)
376{ int tmp ;
377  int __retres2 ;
378
379  {
380  {
381  tmp = exists_runnable_thread();
382  }
383  if (tmp) {
384    __retres2 = 0;
385    goto return_label;
386  } else {
387
388  }
389  __retres2 = 1;
390  return_label:
391  return (__retres2);
392}
393}
394void start_simulation(void)
395{ int kernel_st ;
396  int tmp ;
397
398  {
399  {
400  kernel_st = 0;
401  update_channels();
402  init_threads();
403  fire_delta_events();
404  activate_threads();
405  reset_delta_events();
406  }
407  {
408  while (1) {
409    while_3_continue: ;
410    {
411    kernel_st = 1;
412    eval();
413    }
414    {
415    kernel_st = 2;
416    update_channels();
417    }
418    {
419    kernel_st = 3;
420    fire_delta_events();
421    activate_threads();
422    reset_delta_events();
423    tmp = stop_simulation();
424    }
425    if (tmp) {
426      goto while_3_break;
427    } else {
428
429    }
430  }
431  while_3_break: ;
432  }
433
434  return;
435}
436}
437void init_model(void)
438{
439
440  {
441  q_free = 1;
442  q_write_ev = 2;
443  q_read_ev = q_write_ev;
444  p_num_write = 0;
445  p_dw_pc = 0;
446  p_dw_i = 1;
447  c_num_read = 0;
448  c_dr_pc = 0;
449  c_dr_i = 1;
450
451  return;
452}
453}
454int main(void)
455{ int __retres1 ;
456
457  {
458  {
459  init_model();
460  start_simulation();
461  }
462  __retres1 = 0;
463  return (__retres1);
464}
465}
↑