Showing error 250

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.05.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 t5_pc  =    0;
 19int m_st  ;
 20int t1_st  ;
 21int t2_st  ;
 22int t3_st  ;
 23int t4_st  ;
 24int t5_st  ;
 25int m_i  ;
 26int t1_i  ;
 27int t2_i  ;
 28int t3_i  ;
 29int t4_i  ;
 30int t5_i  ;
 31int M_E  =    2;
 32int T1_E  =    2;
 33int T2_E  =    2;
 34int T3_E  =    2;
 35int T4_E  =    2;
 36int T5_E  =    2;
 37int E_M  =    2;
 38int E_1  =    2;
 39int E_2  =    2;
 40int E_3  =    2;
 41int E_4  =    2;
 42int E_5  =    2;
 43int is_master_triggered(void) ;
 44int is_transmit1_triggered(void) ;
 45int is_transmit2_triggered(void) ;
 46int is_transmit3_triggered(void) ;
 47int is_transmit4_triggered(void) ;
 48int is_transmit5_triggered(void) ;
 49void immediate_notify(void) ;
 50int token  ;
 51int __VERIFIER_nondet_int()  ;
 52int local  ;
 53void master(void) 
 54{ 
 55
 56  {
 57  if (m_pc == 0) {
 58    goto M_ENTRY;
 59  } else {
 60    if (m_pc == 1) {
 61      goto M_WAIT;
 62    } else {
 63
 64    }
 65  }
 66  M_ENTRY: ;
 67  {
 68  while (1) {
 69    while_0_continue: /* CIL Label */ ;
 70    {
 71    token = __VERIFIER_nondet_int();
 72    local = token;
 73    E_1 = 1;
 74    immediate_notify();
 75    E_1 = 2;
 76    m_pc = 1;
 77    m_st = 2;
 78    }
 79
 80    goto return_label;
 81    M_WAIT: ;
 82    if (token != local + 5) {
 83      {
 84      error();
 85      }
 86    } else {
 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_4 = 1;
194    immediate_notify();
195    E_4 = 2;
196    }
197  }
198  while_3_break: /* CIL Label */ ;
199  }
200
201  return_label: /* CIL Label */ 
202  return;
203}
204}
205void transmit4(void) 
206{ 
207
208  {
209  if (t4_pc == 0) {
210    goto T4_ENTRY;
211  } else {
212    if (t4_pc == 1) {
213      goto T4_WAIT;
214    } else {
215
216    }
217  }
218  T4_ENTRY: ;
219  {
220  while (1) {
221    while_4_continue: /* CIL Label */ ;
222    t4_pc = 1;
223    t4_st = 2;
224
225    goto return_label;
226    T4_WAIT: 
227    {
228    token += 1;
229    E_5 = 1;
230    immediate_notify();
231    E_5 = 2;
232    }
233  }
234  while_4_break: /* CIL Label */ ;
235  }
236
237  return_label: /* CIL Label */ 
238  return;
239}
240}
241void transmit5(void) 
242{ 
243
244  {
245  if (t5_pc == 0) {
246    goto T5_ENTRY;
247  } else {
248    if (t5_pc == 1) {
249      goto T5_WAIT;
250    } else {
251
252    }
253  }
254  T5_ENTRY: ;
255  {
256  while (1) {
257    while_5_continue: /* CIL Label */ ;
258    t5_pc = 1;
259    t5_st = 2;
260
261    goto return_label;
262    T5_WAIT: 
263    {
264    token += 1;
265    E_M = 1;
266    immediate_notify();
267    E_M = 2;
268    }
269  }
270  while_5_break: /* CIL Label */ ;
271  }
272
273  return_label: /* CIL Label */ 
274  return;
275}
276}
277int is_master_triggered(void) 
278{ int __retres1 ;
279
280  {
281  if (m_pc == 1) {
282    if (E_M == 1) {
283      __retres1 = 1;
284      goto return_label;
285    } else {
286
287    }
288  } else {
289
290  }
291  __retres1 = 0;
292  return_label: /* CIL Label */ 
293  return (__retres1);
294}
295}
296int is_transmit1_triggered(void) 
297{ int __retres1 ;
298
299  {
300  if (t1_pc == 1) {
301    if (E_1 == 1) {
302      __retres1 = 1;
303      goto return_label;
304    } else {
305
306    }
307  } else {
308
309  }
310  __retres1 = 0;
311  return_label: /* CIL Label */ 
312  return (__retres1);
313}
314}
315int is_transmit2_triggered(void) 
316{ int __retres1 ;
317
318  {
319  if (t2_pc == 1) {
320    if (E_2 == 1) {
321      __retres1 = 1;
322      goto return_label;
323    } else {
324
325    }
326  } else {
327
328  }
329  __retres1 = 0;
330  return_label: /* CIL Label */ 
331  return (__retres1);
332}
333}
334int is_transmit3_triggered(void) 
335{ int __retres1 ;
336
337  {
338  if (t3_pc == 1) {
339    if (E_3 == 1) {
340      __retres1 = 1;
341      goto return_label;
342    } else {
343
344    }
345  } else {
346
347  }
348  __retres1 = 0;
349  return_label: /* CIL Label */ 
350  return (__retres1);
351}
352}
353int is_transmit4_triggered(void) 
354{ int __retres1 ;
355
356  {
357  if (t4_pc == 1) {
358    if (E_4 == 1) {
359      __retres1 = 1;
360      goto return_label;
361    } else {
362
363    }
364  } else {
365
366  }
367  __retres1 = 0;
368  return_label: /* CIL Label */ 
369  return (__retres1);
370}
371}
372int is_transmit5_triggered(void) 
373{ int __retres1 ;
374
375  {
376  if (t5_pc == 1) {
377    if (E_5 == 1) {
378      __retres1 = 1;
379      goto return_label;
380    } else {
381
382    }
383  } else {
384
385  }
386  __retres1 = 0;
387  return_label: /* CIL Label */ 
388  return (__retres1);
389}
390}
391void update_channels(void) 
392{ 
393
394  {
395
396  return;
397}
398}
399void init_threads(void) 
400{ 
401
402  {
403  if (m_i == 1) {
404    m_st = 0;
405  } else {
406    m_st = 2;
407  }
408  if (t1_i == 1) {
409    t1_st = 0;
410  } else {
411    t1_st = 2;
412  }
413  if (t2_i == 1) {
414    t2_st = 0;
415  } else {
416    t2_st = 2;
417  }
418  if (t3_i == 1) {
419    t3_st = 0;
420  } else {
421    t3_st = 2;
422  }
423  if (t4_i == 1) {
424    t4_st = 0;
425  } else {
426    t4_st = 2;
427  }
428  if (t5_i == 1) {
429    t5_st = 0;
430  } else {
431    t5_st = 2;
432  }
433
434  return;
435}
436}
437int exists_runnable_thread(void) 
438{ int __retres1 ;
439
440  {
441  if (m_st == 0) {
442    __retres1 = 1;
443    goto return_label;
444  } else {
445    if (t1_st == 0) {
446      __retres1 = 1;
447      goto return_label;
448    } else {
449      if (t2_st == 0) {
450        __retres1 = 1;
451        goto return_label;
452      } else {
453        if (t3_st == 0) {
454          __retres1 = 1;
455          goto return_label;
456        } else {
457          if (t4_st == 0) {
458            __retres1 = 1;
459            goto return_label;
460          } else {
461            if (t5_st == 0) {
462              __retres1 = 1;
463              goto return_label;
464            } else {
465
466            }
467          }
468        }
469      }
470    }
471  }
472  __retres1 = 0;
473  return_label: /* CIL Label */ 
474  return (__retres1);
475}
476}
477void eval(void) 
478{// int __VERIFIER_nondet_int() ;
479  int tmp ;
480
481  {
482  {
483  while (1) {
484    while_6_continue: /* CIL Label */ ;
485    {
486    tmp = exists_runnable_thread();
487    }
488    if (tmp) {
489
490    } else {
491      goto while_6_break;
492    }
493    if (m_st == 0) {
494      int tmp_ndt_1;
495      tmp_ndt_1 = __VERIFIER_nondet_int();
496      if (tmp_ndt_1) {
497        {
498        m_st = 1;
499        master();
500        }
501      } else {
502
503      }
504    } else {
505
506    }
507    if (t1_st == 0) {
508      int tmp_ndt_2;
509      tmp_ndt_2 = __VERIFIER_nondet_int();
510      if (tmp_ndt_2) {
511        {
512        t1_st = 1;
513        transmit1();
514        }
515      } else {
516
517      }
518    } else {
519
520    }
521    if (t2_st == 0) {
522      int tmp_ndt_3;
523      tmp_ndt_3 = __VERIFIER_nondet_int();
524      if (tmp_ndt_3) {
525        {
526        t2_st = 1;
527        transmit2();
528        }
529      } else {
530
531      }
532    } else {
533
534    }
535    if (t3_st == 0) {
536      int tmp_ndt_4;
537      tmp_ndt_4 = __VERIFIER_nondet_int();
538      if (tmp_ndt_4) {
539        {
540        t3_st = 1;
541        transmit3();
542        }
543      } else {
544
545      }
546    } else {
547
548    }
549    if (t4_st == 0) {
550      int tmp_ndt_5;
551      tmp_ndt_5 = __VERIFIER_nondet_int();
552      if (tmp_ndt_5) {
553        {
554        t4_st = 1;
555        transmit4();
556        }
557      } else {
558
559      }
560    } else {
561
562    }
563    if (t5_st == 0) {
564      int tmp_ndt_6;
565      tmp_ndt_6 = __VERIFIER_nondet_int();
566      if (tmp_ndt_6) {
567        {
568        t5_st = 1;
569        transmit5();
570        }
571      } else {
572
573      }
574    } else {
575
576    }
577  }
578  while_6_break: /* CIL Label */ ;
579  }
580
581  return;
582}
583}
584void fire_delta_events(void) 
585{ 
586
587  {
588  if (M_E == 0) {
589    M_E = 1;
590  } else {
591
592  }
593  if (T1_E == 0) {
594    T1_E = 1;
595  } else {
596
597  }
598  if (T2_E == 0) {
599    T2_E = 1;
600  } else {
601
602  }
603  if (T3_E == 0) {
604    T3_E = 1;
605  } else {
606
607  }
608  if (T4_E == 0) {
609    T4_E = 1;
610  } else {
611
612  }
613  if (T5_E == 0) {
614    T5_E = 1;
615  } else {
616
617  }
618  if (E_M == 0) {
619    E_M = 1;
620  } else {
621
622  }
623  if (E_1 == 0) {
624    E_1 = 1;
625  } else {
626
627  }
628  if (E_2 == 0) {
629    E_2 = 1;
630  } else {
631
632  }
633  if (E_3 == 0) {
634    E_3 = 1;
635  } else {
636
637  }
638  if (E_4 == 0) {
639    E_4 = 1;
640  } else {
641
642  }
643  if (E_5 == 0) {
644    E_5 = 1;
645  } else {
646
647  }
648
649  return;
650}
651}
652void reset_delta_events(void) 
653{ 
654
655  {
656  if (M_E == 1) {
657    M_E = 2;
658  } else {
659
660  }
661  if (T1_E == 1) {
662    T1_E = 2;
663  } else {
664
665  }
666  if (T2_E == 1) {
667    T2_E = 2;
668  } else {
669
670  }
671  if (T3_E == 1) {
672    T3_E = 2;
673  } else {
674
675  }
676  if (T4_E == 1) {
677    T4_E = 2;
678  } else {
679
680  }
681  if (T5_E == 1) {
682    T5_E = 2;
683  } else {
684
685  }
686  if (E_M == 1) {
687    E_M = 2;
688  } else {
689
690  }
691  if (E_1 == 1) {
692    E_1 = 2;
693  } else {
694
695  }
696  if (E_2 == 1) {
697    E_2 = 2;
698  } else {
699
700  }
701  if (E_3 == 1) {
702    E_3 = 2;
703  } else {
704
705  }
706  if (E_4 == 1) {
707    E_4 = 2;
708  } else {
709
710  }
711  if (E_5 == 1) {
712    E_5 = 2;
713  } else {
714
715  }
716
717  return;
718}
719}
720void activate_threads(void) 
721{ int tmp ;
722  int tmp___0 ;
723  int tmp___1 ;
724  int tmp___2 ;
725  int tmp___3 ;
726  int tmp___4 ;
727
728  {
729  {
730  tmp = is_master_triggered();
731  }
732  if (tmp) {
733    m_st = 0;
734  } else {
735
736  }
737  {
738  tmp___0 = is_transmit1_triggered();
739  }
740  if (tmp___0) {
741    t1_st = 0;
742  } else {
743
744  }
745  {
746  tmp___1 = is_transmit2_triggered();
747  }
748  if (tmp___1) {
749    t2_st = 0;
750  } else {
751
752  }
753  {
754  tmp___2 = is_transmit3_triggered();
755  }
756  if (tmp___2) {
757    t3_st = 0;
758  } else {
759
760  }
761  {
762  tmp___3 = is_transmit4_triggered();
763  }
764  if (tmp___3) {
765    t4_st = 0;
766  } else {
767
768  }
769  {
770  tmp___4 = is_transmit5_triggered();
771  }
772  if (tmp___4) {
773    t5_st = 0;
774  } else {
775
776  }
777
778  return;
779}
780}
781void immediate_notify(void) 
782{ 
783
784  {
785  {
786  activate_threads();
787  }
788
789  return;
790}
791}
792void fire_time_events(void) 
793{ 
794
795  {
796  M_E = 1;
797
798  return;
799}
800}
801void reset_time_events(void) 
802{ 
803
804  {
805  if (M_E == 1) {
806    M_E = 2;
807  } else {
808
809  }
810  if (T1_E == 1) {
811    T1_E = 2;
812  } else {
813
814  }
815  if (T2_E == 1) {
816    T2_E = 2;
817  } else {
818
819  }
820  if (T3_E == 1) {
821    T3_E = 2;
822  } else {
823
824  }
825  if (T4_E == 1) {
826    T4_E = 2;
827  } else {
828
829  }
830  if (T5_E == 1) {
831    T5_E = 2;
832  } else {
833
834  }
835  if (E_M == 1) {
836    E_M = 2;
837  } else {
838
839  }
840  if (E_1 == 1) {
841    E_1 = 2;
842  } else {
843
844  }
845  if (E_2 == 1) {
846    E_2 = 2;
847  } else {
848
849  }
850  if (E_3 == 1) {
851    E_3 = 2;
852  } else {
853
854  }
855  if (E_4 == 1) {
856    E_4 = 2;
857  } else {
858
859  }
860  if (E_5 == 1) {
861    E_5 = 2;
862  } else {
863
864  }
865
866  return;
867}
868}
869void init_model(void) 
870{ 
871
872  {
873  m_i = 1;
874  t1_i = 1;
875  t2_i = 1;
876  t3_i = 1;
877  t4_i = 1;
878  t5_i = 1;
879
880  return;
881}
882}
883int stop_simulation(void) 
884{ int tmp ;
885  int __retres2 ;
886
887  {
888  {
889  tmp = exists_runnable_thread();
890  }
891  if (tmp) {
892    __retres2 = 0;
893    goto return_label;
894  } else {
895
896  }
897  __retres2 = 1;
898  return_label: /* CIL Label */ 
899  return (__retres2);
900}
901}
902void start_simulation(void) 
903{ int kernel_st ;
904  int tmp ;
905  int tmp___0 ;
906
907  {
908  {
909  kernel_st = 0;
910  update_channels();
911  init_threads();
912  fire_delta_events();
913  activate_threads();
914  reset_delta_events();
915  }
916  {
917  while (1) {
918    while_7_continue: /* CIL Label */ ;
919    {
920    kernel_st = 1;
921    eval();
922    }
923    {
924    kernel_st = 2;
925    update_channels();
926    }
927    {
928    kernel_st = 3;
929    fire_delta_events();
930    activate_threads();
931    reset_delta_events();
932    }
933    {
934    tmp = exists_runnable_thread();
935    }
936    if (tmp == 0) {
937      {
938      kernel_st = 4;
939      fire_time_events();
940      activate_threads();
941      reset_time_events();
942      }
943    } else {
944
945    }
946    {
947    tmp___0 = stop_simulation();
948    }
949    if (tmp___0) {
950      goto while_7_break;
951    } else {
952
953    }
954  }
955  while_7_break: /* CIL Label */ ;
956  }
957
958  return;
959}
960}
961int main(void) 
962{ int __retres1 ;
963
964  {
965  {
966  init_model();
967  start_simulation();
968  }
969  __retres1 = 0;
970  return (__retres1);
971}
972}
↑