Showing error 1487

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