Showing error 270

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