Showing error 2299

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