Showing error 2325

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