Showing error 271

User: Jiri Slaby
Error type: Reachable Error Location
Error type description: A specified error location is reachable in some program path
File location: systemc/toy2_BUG.cil.c
Line in file: 18
Project: SV-COMP 2012
Tools: Manual Work
Entered: 2012-11-19 13:47:39 UTC

Source: 

  1/* Generated by CIL v. 1.3.6 */
  2/* print_CIL_Input is true */
  3
  4/*int nondet(void)
  5{
  6  int x;
  7  {
  8    return (x);
  9  }
 10  }*/
 11
 12
 13void error(void) 
 14{ 
 15
 16  {
 17  goto ERROR;
 18  ERROR: ;
 19  return;
 20}
 21}
 22
 23int c  ;
 24int c_t  ;
 25int c_req_up  ;
 26int p_in  ;
 27int p_out  ;
 28int wl_st  ;
 29int c1_st  ;
 30int c2_st  ;
 31int wb_st  ;
 32int r_st  ;
 33int wl_i  ;
 34int c1_i  ;
 35int c2_i  ;
 36int wb_i  ;
 37int r_i  ;
 38int wl_pc  ;
 39int c1_pc  ;
 40int c2_pc  ;
 41int wb_pc  ;
 42int e_e  ;
 43int e_f  ;
 44int e_g  ;
 45int e_c  ;
 46int e_p_in  ;
 47int e_wl  ;
 48void write_loop(void) ;
 49void compute1(void) ;
 50void compute2(void) ;
 51void write_back(void) ;
 52void read(void) ;
 53int d  ;
 54int data  ;
 55int processed  ;
 56static int t_b  ;
 57void write_loop(void) 
 58{ int t ;
 59
 60  {
 61  if ((int )wl_pc == 0) {
 62    goto WL_ENTRY_LOC;
 63  } else {
 64    if ((int )wl_pc == 2) {
 65      goto WL_WAIT_2_LOC;
 66    } else {
 67      if ((int )wl_pc == 1) {
 68        goto WL_WAIT_1_LOC;
 69      } else {
 70
 71      }
 72    }
 73  }
 74  WL_ENTRY_LOC: 
 75  wl_st = 2;
 76  wl_pc = 1;
 77  e_wl = 0;
 78
 79  goto return_label;
 80  WL_WAIT_1_LOC: 
 81  {
 82  while (1) {
 83    while_0_continue: /* CIL Label */ ;
 84    t = d;
 85    data = d;
 86    processed = 0;
 87    e_f = 1;
 88    if ((int )c1_pc == 1) {
 89      if ((int )e_f == 1) {
 90        c1_st = 0;
 91      } else {
 92
 93      }
 94    } else {
 95
 96    }
 97    if ((int )c2_pc == 1) {
 98      if ((int )e_f == 1) {
 99        c2_st = 0;
100      } else {
101
102      }
103    } else {
104
105    }
106    e_f = 2;
107    wl_st = 2;
108    wl_pc = 2;
109    t_b = t;
110
111    goto return_label;
112    WL_WAIT_2_LOC: 
113    t = t_b;
114    if (d == t + 1) {
115
116    } else {
117      {
118        error();
119      }
120    }
121  }
122  while_0_break: /* CIL Label */ ;
123  }
124  return_label: /* CIL Label */ 
125  return;
126}
127}
128void compute1(void) 
129{ 
130
131  {
132  if ((int )c1_pc == 0) {
133    goto C1_ENTRY_LOC;
134  } else {
135    if ((int )c1_pc == 1) {
136      goto C1_WAIT_LOC;
137    } else {
138
139    }
140  }
141  C1_ENTRY_LOC: 
142  {
143  while (1) {
144    while_1_continue: /* CIL Label */ ;
145    c1_st = 2;
146    c1_pc = 1;
147
148    goto return_label;
149    C1_WAIT_LOC: 
150    if (! processed) {
151      data += 1;
152      e_g = 1;
153      if ((int )wb_pc == 1) {
154        if ((int )e_g == 1) {
155          wb_st = 0;
156        } else {
157
158        }
159      } else {
160
161      }
162      e_g = 2;
163    } else {
164
165    }
166  }
167  while_1_break: /* CIL Label */ ;
168  }
169  return_label: /* CIL Label */ 
170  return;
171}
172}
173void compute2(void) 
174{ 
175
176  {
177  if ((int )c2_pc == 0) {
178    goto C2_ENTRY_LOC;
179  } else {
180    if ((int )c2_pc == 1) {
181      goto C2_WAIT_LOC;
182    } else {
183
184    }
185  }
186  C2_ENTRY_LOC: 
187  {
188  while (1) {
189    while_2_continue: /* CIL Label */ ;
190    c2_st = 2;
191    c2_pc = 1;
192
193    goto return_label;
194    C2_WAIT_LOC: 
195    if (! processed) {
196      data += 1;
197      e_g = 1;
198      if ((int )wb_pc == 1) {
199        if ((int )e_g == 1) {
200          wb_st = 0;
201        } else {
202
203        }
204      } else {
205
206      }
207      e_g = 2;
208    } else {
209
210    }
211  }
212  while_2_break: /* CIL Label */ ;
213  }
214  return_label: /* CIL Label */ 
215  return;
216}
217}
218void write_back(void) 
219{ 
220
221  {
222  if ((int )wb_pc == 0) {
223    goto WB_ENTRY_LOC;
224  } else {
225    if ((int )wb_pc == 1) {
226      goto WB_WAIT_LOC;
227    } else {
228
229    }
230  }
231  WB_ENTRY_LOC: 
232  {
233  while (1) {
234    while_3_continue: /* CIL Label */ ;
235    wb_st = 2;
236    wb_pc = 1;
237
238    goto return_label;
239    WB_WAIT_LOC: 
240    c_t = data;
241    c_req_up = 1;
242    processed = 1;
243  }
244  while_3_break: /* CIL Label */ ;
245  }
246  return_label: /* CIL Label */ 
247  return;
248}
249}
250void read(void) 
251{ 
252
253  {
254  d = c;
255  e_e = 1;
256  if ((int )wl_pc == 1) {
257    if ((int )e_wl == 1) {
258      wl_st = 0;
259    } else {
260      goto _L;
261    }
262  } else {
263    _L: /* CIL Label */ 
264    if ((int )wl_pc == 2) {
265      if ((int )e_e == 1) {
266        wl_st = 0;
267      } else {
268
269      }
270    } else {
271
272    }
273  }
274  e_e = 2;
275  r_st = 2;
276
277  return;
278}
279}
280void eval(void) 
281{ int tmp ;
282  int tmp___0 ;
283  int tmp___1 ;
284  int tmp___2 ;
285  int tmp___3 ;
286//  int __VERIFIER_nondet_int(); 
287
288  {
289  {
290  while (1) {
291    while_4_continue: /* CIL Label */ ;
292    if ((int )wl_st == 0) {
293
294    } else {
295      if ((int )c1_st == 0) {
296
297      } else {
298        if ((int )c2_st == 0) {
299
300        } else {
301          if ((int )wb_st == 0) {
302
303          } else {
304            if ((int )r_st == 0) {
305
306            } else {
307              goto while_4_break;
308            }
309          }
310        }
311      }
312    }
313    if ((int )wl_st == 0) {
314      {
315        tmp =  __VERIFIER_nondet_int(); 
316      }
317      if (tmp) {
318        {
319        wl_st = 1;
320        write_loop();
321        }
322      } else {
323
324      }
325    } else {
326
327    }
328    if ((int )c1_st == 0) {
329      {
330        tmp___0 =  __VERIFIER_nondet_int(); 
331      }
332      if (tmp___0) {
333        {
334        c1_st = 1;
335        compute1();
336        }
337      } else {
338
339      }
340    } else {
341
342    }
343    if ((int )c2_st == 0) {
344      {
345        tmp___1 =  __VERIFIER_nondet_int(); 
346      }
347      if (tmp___1) {
348        {
349        c2_st = 1;
350        compute2();
351        }
352      } else {
353
354      }
355    } else {
356
357    }
358    if ((int )wb_st == 0) {
359      {
360        tmp___2 =  __VERIFIER_nondet_int(); 
361      }
362      if (tmp___2) {
363        {
364        wb_st = 1;
365        write_back();
366        }
367      } else {
368
369      }
370    } else {
371
372    }
373    if ((int )r_st == 0) {
374      {
375        tmp___3 = __VERIFIER_nondet_int();
376      }
377      if (tmp___3) {
378        {
379        r_st = 1;
380        read();
381        }
382      } else {
383
384      }
385    } else {
386
387    }
388  }
389  while_4_break: /* CIL Label */ ;
390  }
391
392  return;
393}
394}
395void start_simulation(void) 
396{ int kernel_st ;
397
398  {
399  kernel_st = 0;
400  if ((int )c_req_up == 1) {
401    if (c != c_t) {
402      c = c_t;
403      e_c = 0;
404    } else {
405
406    }
407    c_req_up = 0;
408  } else {
409
410  }
411  if ((int )wl_i == 1) {
412    wl_st = 0;
413  } else {
414    wl_st = 2;
415  }
416  if ((int )c1_i == 1) {
417    c1_st = 0;
418  } else {
419    c1_st = 2;
420  }
421  if ((int )c2_i == 1) {
422    c2_st = 0;
423  } else {
424    c2_st = 2;
425  }
426  if ((int )wb_i == 1) {
427    wb_st = 0;
428  } else {
429    wb_st = 2;
430  }
431  if ((int )r_i == 1) {
432    r_st = 0;
433  } else {
434    r_st = 2;
435  }
436  if ((int )e_f == 0) {
437    e_f = 1;
438  } else {
439
440  }
441  if ((int )e_g == 0) {
442    e_g = 1;
443  } else {
444
445  }
446  if ((int )e_e == 0) {
447    e_e = 1;
448  } else {
449
450  }
451  if ((int )e_c == 0) {
452    e_c = 1;
453  } else {
454
455  }
456  if ((int )e_wl == 0) {
457    e_wl = 1;
458  } else {
459
460  }
461  if ((int )wl_pc == 1) {
462    if ((int )e_wl == 1) {
463      wl_st = 0;
464    } else {
465      goto _L;
466    }
467  } else {
468    _L: /* CIL Label */ 
469    if ((int )wl_pc == 2) {
470      if ((int )e_e == 1) {
471        wl_st = 0;
472      } else {
473
474      }
475    } else {
476
477    }
478  }
479  if ((int )c1_pc == 1) {
480    if ((int )e_f == 1) {
481      c1_st = 0;
482    } else {
483
484    }
485  } else {
486
487  }
488  if ((int )c2_pc == 1) {
489    if ((int )e_f == 1) {
490      c2_st = 0;
491    } else {
492
493    }
494  } else {
495
496  }
497  if ((int )wb_pc == 1) {
498    if ((int )e_g == 1) {
499      wb_st = 0;
500    } else {
501
502    }
503  } else {
504
505  }
506  if ((int )e_c == 1) {
507    r_st = 0;
508  } else {
509
510  }
511  if ((int )e_e == 1) {
512    e_e = 2;
513  } else {
514
515  }
516  if ((int )e_f == 1) {
517    e_f = 2;
518  } else {
519
520  }
521  if ((int )e_g == 1) {
522    e_g = 2;
523  } else {
524
525  }
526  if ((int )e_c == 1) {
527    e_c = 2;
528  } else {
529
530  }
531  if ((int )e_wl == 1) {
532    e_wl = 2;
533  } else {
534
535  }
536  {
537  while (1) {
538    while_5_continue: /* CIL Label */ ;
539    {
540    kernel_st = 1;
541    eval();
542    }
543    kernel_st = 2;
544    if ((int )c_req_up == 1) {
545      if (c != c_t) {
546        c = c_t;
547        e_c = 0;
548      } else {
549
550      }
551      c_req_up = 0;
552    } else {
553
554    }
555    kernel_st = 3;
556    if ((int )e_f == 0) {
557      e_f = 1;
558    } else {
559
560    }
561    if ((int )e_g == 0) {
562      e_g = 1;
563    } else {
564
565    }
566    if ((int )e_e == 0) {
567      e_e = 1;
568    } else {
569
570    }
571    if ((int )e_c == 0) {
572      e_c = 1;
573    } else {
574
575    }
576    if ((int )e_wl == 0) {
577      e_wl = 1;
578    } else {
579
580    }
581    if ((int )wl_pc == 1) {
582      if ((int )e_wl == 1) {
583        wl_st = 0;
584      } else {
585        goto _L___0;
586      }
587    } else {
588      _L___0: /* CIL Label */ 
589      if ((int )wl_pc == 2) {
590        if ((int )e_e == 1) {
591          wl_st = 0;
592        } else {
593
594        }
595      } else {
596
597      }
598    }
599    if ((int )c1_pc == 1) {
600      if ((int )e_f == 1) {
601        c1_st = 0;
602      } else {
603
604      }
605    } else {
606
607    }
608    if ((int )c2_pc == 1) {
609      if ((int )e_f == 1) {
610        c2_st = 0;
611      } else {
612
613      }
614    } else {
615
616    }
617    if ((int )wb_pc == 1) {
618      if ((int )e_g == 1) {
619        wb_st = 0;
620      } else {
621
622      }
623    } else {
624
625    }
626    if ((int )e_c == 1) {
627      r_st = 0;
628    } else {
629
630    }
631    if ((int )e_e == 1) {
632      e_e = 2;
633    } else {
634
635    }
636    if ((int )e_f == 1) {
637      e_f = 2;
638    } else {
639
640    }
641    if ((int )e_g == 1) {
642      e_g = 2;
643    } else {
644
645    }
646    if ((int )e_c == 1) {
647      e_c = 2;
648    } else {
649
650    }
651    if ((int )e_wl == 1) {
652      e_wl = 2;
653    } else {
654
655    }
656    if ((int )wl_st == 0) {
657
658    } else {
659      if ((int )c1_st == 0) {
660
661      } else {
662        if ((int )c2_st == 0) {
663
664        } else {
665          if ((int )wb_st == 0) {
666
667          } else {
668            if ((int )r_st == 0) {
669
670            } else {
671              goto while_5_break;
672            }
673          }
674        }
675      }
676    }
677  }
678  while_5_break: /* CIL Label */ ;
679  }
680
681  return;
682}
683}
684int main(void) 
685{ int __retres1 ;
686
687  {
688  {
689  e_wl = 2;
690  e_c = e_wl;
691  e_g = e_c;
692  e_f = e_g;
693  e_e = e_f;
694  wl_pc = 0;
695  c1_pc = 0;
696  c2_pc = 0;
697  wb_pc = 0;
698  wb_i = 1;
699  c2_i = wb_i;
700  c1_i = c2_i;
701  wl_i = c1_i;
702  r_i = 0;
703  c_req_up = 0;
704  d = 0;
705  c = 0;
706  start_simulation();
707  }
708  __retres1 = 0;
709  return (__retres1);
710}
711}
↑