Showing error 2277

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_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: 

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