Showing error 2289

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