Showing error 276

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