Showing error 228

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_BUG.cil.c
Line in file: 7
Project: SV-COMP 2012
Tools: Manual Work
Entered: 2012-11-19 13:47:39 UTC

Source: 

  1
  2void error(void) 
  3{ 
  4
  5  {
  6  goto ERROR;
  7  ERROR: ;
  8  return;
  9}
 10}
 11
 12void immediate_notify(void) ;
 13int max_loop ;
 14int num ;
 15int i  ;
 16int e  ;
 17int timer ;
 18char data_0  ;
 19char data_1  ;
 20char read_data(int i___0 ) 
 21{ char c ;
 22  char __retres3 ;
 23
 24  {
 25  if (i___0 == 0) {
 26    __retres3 = data_0;
 27    goto return_label;
 28  } else {
 29    if (i___0 == 1) {
 30      __retres3 = data_1;
 31      goto return_label;
 32    } else {
 33      {
 34        error();
 35      }
 36    }
 37  }
 38  __retres3 = c;
 39  return_label: /* CIL Label */ 
 40  return (__retres3);
 41}
 42}
 43void write_data(int i___0 , char c ) 
 44{ 
 45
 46  {
 47  if (i___0 == 0) {
 48    data_0 = c;
 49  } else {
 50    if (i___0 == 1) {
 51      data_1 = c;
 52    } else {
 53      {
 54        error();
 55      }
 56    }
 57  }
 58
 59  return;
 60}
 61}
 62int P_1_pc;
 63int P_1_st  ;
 64int P_1_i  ;
 65int P_1_ev  ;
 66void P_1(void) 
 67{ 
 68
 69  {
 70  if ((int )P_1_pc == 0) {
 71    goto P_1_ENTRY_LOC;
 72  } else {
 73    if ((int )P_1_pc == 1) {
 74      goto P_1_WAIT_LOC;
 75    } else {
 76
 77    }
 78  }
 79  P_1_ENTRY_LOC: 
 80  {
 81  while (i < max_loop) {
 82    while_0_continue: /* CIL Label */ ;
 83    {
 84    write_data(num, 'A');
 85    num += 1;
 86    P_1_pc = 1;
 87    P_1_st = 2;
 88    }
 89
 90    goto return_label;
 91    P_1_WAIT_LOC: ;
 92  }
 93  while_0_break: /* CIL Label */ ;
 94  }
 95  P_1_st = 2;
 96
 97  return_label: /* CIL Label */ 
 98  return;
 99}
100}
101int is_P_1_triggered(void) 
102{ int __retres1 ;
103
104  {
105  if ((int )P_1_pc == 1) {
106    if ((int )P_1_ev == 1) {
107      __retres1 = 1;
108      goto return_label;
109    } else {
110
111    }
112  } else {
113
114  }
115  __retres1 = 0;
116  return_label: /* CIL Label */ 
117  return (__retres1);
118}
119}
120int P_2_pc  ;
121int P_2_st  ;
122int P_2_i  ;
123int P_2_ev  ;
124void P_2(void) 
125{ 
126
127  {
128  if ((int )P_2_pc == 0) {
129    goto P_2_ENTRY_LOC;
130  } else {
131    if ((int )P_2_pc == 1) {
132      goto P_2_WAIT_LOC;
133    } else {
134
135    }
136  }
137  P_2_ENTRY_LOC: 
138  {
139  while (i < max_loop) {
140    while_1_continue: /* CIL Label */ ;
141    {
142    write_data(num, 'B');
143    num += 1;
144    }
145    if (timer) {
146      {
147      timer = 0;
148      e = 1;
149      immediate_notify();
150      e = 2;
151      }
152    } else {
153
154    }
155    P_2_pc = 1;
156    P_2_st = 2;
157
158    goto return_label;
159    P_2_WAIT_LOC: ;
160  }
161  while_1_break: /* CIL Label */ ;
162  }
163  P_2_st = 2;
164
165  return_label: /* CIL Label */ 
166  return;
167}
168}
169int is_P_2_triggered(void) 
170{ int __retres1 ;
171
172  {
173  if ((int )P_2_pc == 1) {
174    if ((int )P_2_ev == 1) {
175      __retres1 = 1;
176      goto return_label;
177    } else {
178
179    }
180  } else {
181
182  }
183  __retres1 = 0;
184  return_label: /* CIL Label */ 
185  return (__retres1);
186}
187}
188int C_1_pc  ;
189int C_1_st  ;
190int C_1_i  ;
191int C_1_ev  ;
192int C_1_pr  ;
193void C_1(void) 
194{ char c ;
195
196  {
197  if ((int )C_1_pc == 0) {
198    goto C_1_ENTRY_LOC;
199  } else {
200    if ((int )C_1_pc == 1) {
201      goto C_1_WAIT_1_LOC;
202    } else {
203      if ((int )C_1_pc == 2) {
204        goto C_1_WAIT_2_LOC;
205      } else {
206
207      }
208    }
209  }
210  C_1_ENTRY_LOC: 
211  {
212  while (i < max_loop) {
213    while_2_continue: /* CIL Label */ ;
214    if (num == 0) {
215      timer = 1;
216      i += 1;
217      C_1_pc = 1;
218      C_1_st = 2;
219
220      goto return_label;
221      C_1_WAIT_1_LOC: ;
222    } else {
223
224    }
225    num -= 1;
226    if (! (num >= 0)) {
227      {
228        error();
229      }
230    } else {
231
232    }
233    {
234    c = read_data(num);
235    i += 1;
236    C_1_pc = 2;
237    C_1_st = 2;
238    }
239
240    goto return_label;
241    C_1_WAIT_2_LOC: ;
242  }
243  while_2_break: /* CIL Label */ ;
244  }
245  C_1_st = 2;
246
247  return_label: /* CIL Label */ 
248  return;
249}
250}
251int is_C_1_triggered(void) 
252{ int __retres1 ;
253
254  {
255  if ((int )C_1_pc == 1) {
256    if ((int )e == 1) {
257      __retres1 = 1;
258      goto return_label;
259    } else {
260
261    }
262  } else {
263
264  }
265  if ((int )C_1_pc == 2) {
266    if ((int )C_1_ev == 1) {
267      __retres1 = 1;
268      goto return_label;
269    } else {
270
271    }
272  } else {
273
274  }
275  __retres1 = 0;
276  return_label: /* CIL Label */ 
277  return (__retres1);
278}
279}
280void update_channels(void) 
281{ 
282
283  {
284
285  return;
286}
287}
288void init_threads(void) 
289{ 
290
291  {
292  if ((int )P_1_i == 1) {
293    P_1_st = 0;
294  } else {
295    P_1_st = 2;
296  }
297  if ((int )P_2_i == 1) {
298    P_2_st = 0;
299  } else {
300    P_2_st = 2;
301  }
302  if ((int )C_1_i == 1) {
303    C_1_st = 0;
304  } else {
305    C_1_st = 2;
306  }
307
308  return;
309}
310}
311int exists_runnable_thread(void) 
312{ int __retres1 ;
313
314  {
315  if ((int )P_1_st == 0) {
316    __retres1 = 1;
317    goto return_label;
318  } else {
319    if ((int )P_2_st == 0) {
320      __retres1 = 1;
321      goto return_label;
322    } else {
323      if ((int )C_1_st == 0) {
324        __retres1 = 1;
325        goto return_label;
326      } else {
327
328      }
329    }
330  }
331  __retres1 = 0;
332  return_label: /* CIL Label */ 
333  return (__retres1);
334}
335}
336void eval(void) 
337{ int tmp ;
338  int tmp___0 ;
339  int tmp___1 ;
340  int tmp___2 ;
341//  int __VERIFIER_nondet_int();
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
↑