Showing error 238

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

Source: 

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