Showing error 269

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