Showing error 2327

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_unsafe.cil.c
Line in file: 9
Project: SV-COMP 2013
Project version: 2.6.28
Tools: Manual Work
Entered: 2013-01-17 16:57:54 UTC

Source: 

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