Showing error 226

User: Jiri Slaby
Error type: Reachable Error Location
Error type description: A specified error location is reachable in some program path
File location: systemc/kundu.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 clk ;
 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//  int __VERIFIER_nondet_int();
343
344  {
345  {
346  while (1) {
347    while_3_continue: /* CIL Label */ ;
348    {
349    tmp___2 = exists_runnable_thread();
350    }
351    if (tmp___2) {
352
353    } else {
354      goto while_3_break;
355    }
356    if ((int )P_1_st == 0) {
357      {
358      tmp = __VERIFIER_nondet_int();
359      }
360      if (tmp) {
361        {
362        P_1_st = 1;
363        P_1();
364        }
365      } else {
366
367      }
368    } else {
369
370    }
371    if ((int )P_2_st == 0) {
372      {
373      tmp___0 = __VERIFIER_nondet_int();
374      }
375      if (tmp___0) {
376        {
377        P_2_st = 1;
378        P_2();
379        }
380      } else {
381
382      }
383    } else {
384
385    }
386    if ((int )C_1_st == 0) {
387      {
388        tmp___1 = __VERIFIER_nondet_int();
389      }
390      if (tmp___1) {
391        {
392        C_1_st = 1;
393        C_1();
394        }
395      } else {
396
397      }
398    } else {
399
400    }
401  }
402  while_3_break: /* CIL Label */ ;
403  }
404
405  return;
406}
407}
408void fire_delta_events(void) 
409{ 
410
411  {
412
413  return;
414}
415}
416void reset_delta_events(void) 
417{ 
418
419  {
420
421  return;
422}
423}
424void fire_time_events(void) 
425{ 
426
427  {
428  C_1_ev = 1;
429  
430  if (clk == 1) {
431
432    P_1_ev = 1;
433    P_2_ev = 1;
434
435    clk = 0;
436  
437  } else {
438    {
439      clk = clk + 1;
440    }
441  }
442
443
444
445  return;
446}
447}
448void reset_time_events(void) 
449{ 
450
451  {
452  if ((int )P_1_ev == 1) {
453    P_1_ev = 2;
454  } else {
455
456  }
457  if ((int )P_2_ev == 1) {
458    P_2_ev = 2;
459  } else {
460
461  }
462  if ((int )C_1_ev == 1) {
463    C_1_ev = 2;
464  } else {
465
466  }
467
468  return;
469}
470}
471void activate_threads(void) 
472{ int tmp ;
473  int tmp___0 ;
474  int tmp___1 ;
475
476  {
477  {
478  tmp = is_P_1_triggered();
479  }
480  if (tmp) {
481    P_1_st = 0;
482  } else {
483
484  }
485  {
486  tmp___0 = is_P_2_triggered();
487  }
488  if (tmp___0) {
489    P_2_st = 0;
490  } else {
491
492  }
493  {
494  tmp___1 = is_C_1_triggered();
495  }
496  if (tmp___1) {
497    C_1_st = 0;
498  } else {
499
500  }
501
502  return;
503}
504}
505void immediate_notify(void) 
506{ 
507
508  {
509  {
510  activate_threads();
511  }
512
513  return;
514}
515}
516int stop_simulation(void) 
517{ int tmp ;
518  int __retres2 ;
519
520  {
521  {
522  tmp = exists_runnable_thread();
523  }
524  if (tmp) {
525    __retres2 = 0;
526    goto return_label;
527  } else {
528
529  }
530  __retres2 = 1;
531  return_label: /* CIL Label */ 
532  return (__retres2);
533}
534}
535void start_simulation(void) 
536{ int kernel_st ;
537  int tmp ;
538  int tmp___0 ;
539
540  {
541  {
542  kernel_st = 0;
543  update_channels();
544  init_threads();
545  fire_delta_events();
546  activate_threads();
547  reset_delta_events();
548  }
549  {
550  while (1) {
551    while_4_continue: /* CIL Label */ ;
552    {
553    kernel_st = 1;
554    eval();
555    }
556    {
557    kernel_st = 2;
558    update_channels();
559    }
560    {
561    kernel_st = 3;
562    fire_delta_events();
563    activate_threads();
564    reset_delta_events();
565    }
566    {
567    tmp = exists_runnable_thread();
568    }
569    if (tmp == 0) {
570      {
571      kernel_st = 4;
572      fire_time_events();
573      activate_threads();
574      reset_time_events();
575      }
576    } else {
577
578    }
579    {
580    tmp___0 = stop_simulation();
581    }
582    if (tmp___0) {
583      goto while_4_break;
584    } else {
585
586    }
587  }
588  while_4_break: /* CIL Label */ ;
589  }
590
591  return;
592}
593}
594void init_model(void) 
595{ 
596
597  {
598  P_1_i = 1;
599  P_2_i = 1;
600  C_1_i = 1;
601
602  return;
603}
604}
605int main(void) 
606{ int count ;
607  int __retres2 ;
608
609  {
610  {
611  num  =    0;
612  i  =    0;
613  clk = 0;
614  max_loop = 8;
615  e  ;
616  timer  =    0;
617  P_1_pc  =    0;
618  P_2_pc  =    0;
619  C_1_pc  =    0;
620
621  count = 0;
622  init_model();
623  start_simulation();
624  }
625  __retres2 = 0;
626  return (__retres2);
627}
628}
629
630
631
↑