Showing error 2322

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