Showing error 2326

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