Showing error 274

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