Showing error 243

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