Showing error 275

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