Showing error 245

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