Showing error 1488

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_unsafe.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 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:
 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: ;
 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: ;
 95  }
 96  P_1_st = 2;
 97
 98  return_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:
118  return (__retres1);
119}
120}
121int C_1_pc ;
122int C_1_st ;
123int C_1_i ;
124int C_1_ev ;
125int C_1_pr ;
126void C_1(void)
127{ char c ;
128
129  {
130  if ((int )C_1_pc == 0) {
131    goto C_1_ENTRY_LOC;
132  } else {
133    if ((int )C_1_pc == 1) {
134      goto C_1_WAIT_1_LOC;
135    } else {
136      if ((int )C_1_pc == 2) {
137        goto C_1_WAIT_2_LOC;
138      } else {
139
140      }
141    }
142  }
143  C_1_ENTRY_LOC:
144  {
145  while (i < max_loop) {
146    while_2_continue: ;
147    if (num == 0) {
148      timer = 1;
149      i += 1;
150      C_1_pc = 1;
151      C_1_st = 2;
152
153      goto return_label;
154      C_1_WAIT_1_LOC: ;
155    } else {
156
157    }
158    num -= 1;
159    if (! (num >= 0)) {
160      {
161 error();
162      }
163    } else {
164
165    }
166    {
167    c = read_data(num);
168    i += 1;
169    C_1_pc = 2;
170    C_1_st = 2;
171    }
172
173    goto return_label;
174    C_1_WAIT_2_LOC: ;
175  }
176  while_2_break: ;
177  }
178  C_1_st = 2;
179
180  return_label:
181  return;
182}
183}
184int is_C_1_triggered(void)
185{ int __retres1 ;
186
187  {
188  if ((int )C_1_pc == 1) {
189    if ((int )e == 1) {
190      __retres1 = 1;
191      goto return_label;
192    } else {
193
194    }
195  } else {
196
197  }
198  if ((int )C_1_pc == 2) {
199    if ((int )C_1_ev == 1) {
200      __retres1 = 1;
201      goto return_label;
202    } else {
203
204    }
205  } else {
206
207  }
208  __retres1 = 0;
209  return_label:
210  return (__retres1);
211}
212}
213void update_channels(void)
214{
215
216  {
217
218  return;
219}
220}
221void init_threads(void)
222{
223
224  {
225  if ((int )P_1_i == 1) {
226    P_1_st = 0;
227  } else {
228    P_1_st = 2;
229  }
230  if ((int )C_1_i == 1) {
231    C_1_st = 0;
232  } else {
233    C_1_st = 2;
234  }
235
236  return;
237}
238}
239int exists_runnable_thread(void)
240{ int __retres1 ;
241
242  {
243  if ((int )P_1_st == 0) {
244    __retres1 = 1;
245    goto return_label;
246  } else {
247      if ((int )C_1_st == 0) {
248        __retres1 = 1;
249        goto return_label;
250      } else {
251
252      }
253    }
254  }
255  __retres1 = 0;
256  return_label:
257  return (__retres1);
258}
259
260void eval(void)
261{ int tmp ;
262  int tmp___0 ;
263  int tmp___1 ;
264  int tmp___2 ;
265
266
267  {
268  {
269  while (1) {
270    while_3_continue: ;
271    {
272    tmp___2 = exists_runnable_thread();
273    }
274    if (tmp___2) {
275
276    } else {
277      goto while_3_break;
278    }
279    if ((int )P_1_st == 0) {
280      {
281      tmp = __VERIFIER_nondet_int();
282      }
283      if (tmp) {
284        {
285        P_1_st = 1;
286        P_1();
287        }
288      } else {
289
290      }
291    } else {
292
293    }
294    if ((int )C_1_st == 0) {
295      {
296 tmp___1 = __VERIFIER_nondet_int();
297      }
298      if (tmp___1) {
299        {
300        C_1_st = 1;
301        C_1();
302        }
303      } else {
304
305      }
306    } else {
307
308    }
309  }
310  while_3_break: ;
311  }
312
313  return;
314}
315}
316void fire_delta_events(void)
317{
318
319  {
320
321  return;
322}
323}
324void reset_delta_events(void)
325{
326
327  {
328
329  return;
330}
331}
332void fire_time_events(void)
333{
334
335  {
336  C_1_ev = 1;
337
338  P_1_ev = 1;
339
340
341
342
343  return;
344}
345}
346void reset_time_events(void)
347{
348
349  {
350  if ((int )P_1_ev == 1) {
351    P_1_ev = 2;
352  } else {
353
354  }
355  if ((int )C_1_ev == 1) {
356    C_1_ev = 2;
357  } else {
358
359  }
360
361  return;
362}
363}
364void activate_threads(void)
365{ int tmp ;
366  int tmp___0 ;
367  int tmp___1 ;
368
369  {
370  {
371  tmp = is_P_1_triggered();
372  }
373  if (tmp) {
374    P_1_st = 0;
375  } else {
376
377  }
378  {
379  tmp___1 = is_C_1_triggered();
380  }
381  if (tmp___1) {
382    C_1_st = 0;
383  } else {
384
385  }
386
387  return;
388}
389}
390void immediate_notify(void)
391{
392
393  {
394  {
395  activate_threads();
396  }
397
398  return;
399}
400}
401int stop_simulation(void)
402{ int tmp ;
403  int __retres2 ;
404
405  {
406  {
407  tmp = exists_runnable_thread();
408  }
409  if (tmp) {
410    __retres2 = 0;
411    goto return_label;
412  } else {
413
414  }
415  __retres2 = 1;
416  return_label:
417  return (__retres2);
418}
419}
420void start_simulation(void)
421{ int kernel_st ;
422  int tmp ;
423  int tmp___0 ;
424
425  {
426  {
427  kernel_st = 0;
428  update_channels();
429  init_threads();
430  fire_delta_events();
431  activate_threads();
432  reset_delta_events();
433  }
434  {
435  while (1) {
436    while_4_continue: ;
437    {
438    kernel_st = 1;
439    eval();
440    }
441    {
442    kernel_st = 2;
443    update_channels();
444    }
445    {
446    kernel_st = 3;
447    fire_delta_events();
448    activate_threads();
449    reset_delta_events();
450    }
451    {
452    tmp = exists_runnable_thread();
453    }
454    if (tmp == 0) {
455      {
456      kernel_st = 4;
457      fire_time_events();
458      activate_threads();
459      reset_time_events();
460      }
461    } else {
462
463    }
464    {
465    tmp___0 = stop_simulation();
466    }
467    if (tmp___0) {
468      goto while_4_break;
469    } else {
470
471    }
472  }
473  while_4_break: ;
474  }
475
476  return;
477}
478}
479void init_model(void)
480{
481
482  {
483  P_1_i = 1;
484  C_1_i = 1;
485
486  return;
487}
488}
489int main(void)
490{ int count ;
491  int __retres2 ;
492
493  {
494  {
495  num = 0;
496  i = 0;
497  max_loop = 2;
498  e ;
499  timer = 0;
500  P_1_pc = 0;
501  C_1_pc = 0;
502
503  count = 0;
504  init_model();
505  start_simulation();
506  }
507  __retres2 = 0;
508  return (__retres2);
509}
510}
↑