Showing error 2296

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