Showing error 2279

User: Jiri Slaby
Error type: Reachable Error Location
Error type description: A specified error location is reachable in some program path
File location: systemc/kundu2_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: 

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