Showing error 2301

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