Showing error 248

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