Showing error 2278

User: Jiri Slaby
Error type: Reachable Error Location
Error type description: A specified error location is reachable in some program path
File location: systemc/kundu1_unsafe.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 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 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: /* CIL Label */ ;
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: /* CIL Label */ ;
177  }
178  C_1_st = 2;
179
180  return_label: /* CIL 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: /* CIL 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: /* CIL 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  while (1) {
269    while_3_continue: /* CIL Label */ ;
270    {
271    tmp___2 = exists_runnable_thread();
272    }
273    if (tmp___2) {
274
275    } else {
276      goto while_3_break;
277    }
278    if ((int )P_1_st == 0) {
279      {
280      tmp = __VERIFIER_nondet_int();
281      }
282      if (tmp) {
283        {
284        P_1_st = 1;
285        P_1();
286        }
287      } else {
288
289      }
290    } else {
291
292    }
293    if ((int )C_1_st == 0) {
294      {
295        tmp___1 = __VERIFIER_nondet_int();
296      }
297      if (tmp___1) {
298        {
299        C_1_st = 1;
300        C_1();
301        }
302      } else {
303
304      }
305    } else {
306
307    }
308  }
309  while_3_break: /* CIL Label */ ;
310  }
311
312  return;
313}
314}
315void fire_delta_events(void) 
316{ 
317
318  {
319
320  return;
321}
322}
323void reset_delta_events(void) 
324{ 
325
326  {
327
328  return;
329}
330}
331void fire_time_events(void) 
332{ 
333
334  {
335  C_1_ev = 1;
336  
337  P_1_ev = 1;
338  
339
340
341
342  return;
343}
344}
345void reset_time_events(void) 
346{ 
347
348  {
349  if ((int )P_1_ev == 1) {
350    P_1_ev = 2;
351  } else {
352
353  }
354  if ((int )C_1_ev == 1) {
355    C_1_ev = 2;
356  } else {
357
358  }
359
360  return;
361}
362}
363void activate_threads(void) 
364{ int tmp ;
365  int tmp___0 ;
366  int tmp___1 ;
367
368  {
369  {
370  tmp = is_P_1_triggered();
371  }
372  if (tmp) {
373    P_1_st = 0;
374  } else {
375
376  }
377  {
378  tmp___1 = is_C_1_triggered();
379  }
380  if (tmp___1) {
381    C_1_st = 0;
382  } else {
383
384  }
385
386  return;
387}
388}
389void immediate_notify(void) 
390{ 
391
392  {
393  {
394  activate_threads();
395  }
396
397  return;
398}
399}
400int stop_simulation(void) 
401{ int tmp ;
402  int __retres2 ;
403
404  {
405  {
406  tmp = exists_runnable_thread();
407  }
408  if (tmp) {
409    __retres2 = 0;
410    goto return_label;
411  } else {
412
413  }
414  __retres2 = 1;
415  return_label: /* CIL Label */ 
416  return (__retres2);
417}
418}
419void start_simulation(void) 
420{ int kernel_st ;
421  int tmp ;
422  int tmp___0 ;
423
424  {
425  {
426  kernel_st = 0;
427  update_channels();
428  init_threads();
429  fire_delta_events();
430  activate_threads();
431  reset_delta_events();
432  }
433  {
434  while (1) {
435    while_4_continue: /* CIL Label */ ;
436    {
437    kernel_st = 1;
438    eval();
439    }
440    {
441    kernel_st = 2;
442    update_channels();
443    }
444    {
445    kernel_st = 3;
446    fire_delta_events();
447    activate_threads();
448    reset_delta_events();
449    }
450    {
451    tmp = exists_runnable_thread();
452    }
453    if (tmp == 0) {
454      {
455      kernel_st = 4;
456      fire_time_events();
457      activate_threads();
458      reset_time_events();
459      }
460    } else {
461
462    }
463    {
464    tmp___0 = stop_simulation();
465    }
466    if (tmp___0) {
467      goto while_4_break;
468    } else {
469
470    }
471  }
472  while_4_break: /* CIL Label */ ;
473  }
474
475  return;
476}
477}
478void init_model(void) 
479{ 
480
481  {
482  P_1_i = 1;
483  C_1_i = 1;
484
485  return;
486}
487}
488int main(void) 
489{ int count ;
490  int __retres2 ;
491
492  {
493  {
494  num  =    0;
495  i  =    0;
496  max_loop = 2;
497  e  ;
498  timer  =    0;
499  P_1_pc  =    0;
500  C_1_pc  =    0;
501
502  count = 0;
503  init_model();
504  start_simulation();
505  }
506  __retres2 = 0;
507  return (__retres2);
508}
509}
510
511
512
↑