Showing error 227

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_BUG.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 num ;
 15int i  ;
 16int e  ;
 17int timer ;
 18char data_0  ;
 19char data_1  ;
 20char read_data(int i___0 ) 
 21{ char c ;
 22  char __retres3 ;
 23
 24  {
 25  if (i___0 == 0) {
 26    __retres3 = data_0;
 27    goto return_label;
 28  } else {
 29    if (i___0 == 1) {
 30      __retres3 = data_1;
 31      goto return_label;
 32    } else {
 33      {
 34        error();
 35      }
 36    }
 37  }
 38  __retres3 = c;
 39  return_label: /* CIL Label */ 
 40  return (__retres3);
 41}
 42}
 43void write_data(int i___0 , char c ) 
 44{ 
 45
 46  {
 47  if (i___0 == 0) {
 48    data_0 = c;
 49  } else {
 50    if (i___0 == 1) {
 51      data_1 = c;
 52    } else {
 53      {
 54        error();
 55      }
 56    }
 57  }
 58
 59  return;
 60}
 61}
 62int P_1_pc;
 63int P_1_st  ;
 64int P_1_i  ;
 65int P_1_ev  ;
 66void P_1(void) 
 67{ 
 68
 69  {
 70  if ((int )P_1_pc == 0) {
 71    goto P_1_ENTRY_LOC;
 72  } else {
 73    if ((int )P_1_pc == 1) {
 74      goto P_1_WAIT_LOC;
 75    } else {
 76
 77    }
 78  }
 79  P_1_ENTRY_LOC: 
 80  {
 81  while (i < max_loop) {
 82    while_0_continue: /* CIL Label */ ;
 83    {
 84    write_data(num, 'A');
 85    num += 1;
 86    P_1_pc = 1;
 87    P_1_st = 2;
 88    }
 89
 90    goto return_label;
 91    P_1_WAIT_LOC: ;
 92  }
 93  while_0_break: /* CIL Label */ ;
 94  }
 95  P_1_st = 2;
 96
 97  return_label: /* CIL Label */ 
 98  return;
 99}
100}
101int is_P_1_triggered(void) 
102{ int __retres1 ;
103
104  {
105  if ((int )P_1_pc == 1) {
106    if ((int )P_1_ev == 1) {
107      __retres1 = 1;
108      goto return_label;
109    } else {
110
111    }
112  } else {
113
114  }
115  __retres1 = 0;
116  return_label: /* CIL Label */ 
117  return (__retres1);
118}
119}
120int C_1_pc  ;
121int C_1_st  ;
122int C_1_i  ;
123int C_1_ev  ;
124int C_1_pr  ;
125void C_1(void) 
126{ char c ;
127
128  {
129  if ((int )C_1_pc == 0) {
130    goto C_1_ENTRY_LOC;
131  } else {
132    if ((int )C_1_pc == 1) {
133      goto C_1_WAIT_1_LOC;
134    } else {
135      if ((int )C_1_pc == 2) {
136        goto C_1_WAIT_2_LOC;
137      } else {
138
139      }
140    }
141  }
142  C_1_ENTRY_LOC: 
143  {
144  while (i < max_loop) {
145    while_2_continue: /* CIL Label */ ;
146    if (num == 0) {
147      timer = 1;
148      i += 1;
149      C_1_pc = 1;
150      C_1_st = 2;
151
152      goto return_label;
153      C_1_WAIT_1_LOC: ;
154    } else {
155
156    }
157    num -= 1;
158    if (! (num >= 0)) {
159      {
160        error();
161      }
162    } else {
163
164    }
165    {
166    c = read_data(num);
167    i += 1;
168    C_1_pc = 2;
169    C_1_st = 2;
170    }
171
172    goto return_label;
173    C_1_WAIT_2_LOC: ;
174  }
175  while_2_break: /* CIL Label */ ;
176  }
177  C_1_st = 2;
178
179  return_label: /* CIL Label */ 
180  return;
181}
182}
183int is_C_1_triggered(void) 
184{ int __retres1 ;
185
186  {
187  if ((int )C_1_pc == 1) {
188    if ((int )e == 1) {
189      __retres1 = 1;
190      goto return_label;
191    } else {
192
193    }
194  } else {
195
196  }
197  if ((int )C_1_pc == 2) {
198    if ((int )C_1_ev == 1) {
199      __retres1 = 1;
200      goto return_label;
201    } else {
202
203    }
204  } else {
205
206  }
207  __retres1 = 0;
208  return_label: /* CIL Label */ 
209  return (__retres1);
210}
211}
212void update_channels(void) 
213{ 
214
215  {
216
217  return;
218}
219}
220void init_threads(void) 
221{ 
222
223  {
224  if ((int )P_1_i == 1) {
225    P_1_st = 0;
226  } else {
227    P_1_st = 2;
228  }
229  if ((int )C_1_i == 1) {
230    C_1_st = 0;
231  } else {
232    C_1_st = 2;
233  }
234
235  return;
236}
237}
238int exists_runnable_thread(void) 
239{ int __retres1 ;
240
241  {
242  if ((int )P_1_st == 0) {
243    __retres1 = 1;
244    goto return_label;
245  } else {
246      if ((int )C_1_st == 0) {
247        __retres1 = 1;
248        goto return_label;
249      } else {
250
251      }
252    }
253  }
254  __retres1 = 0;
255  return_label: /* CIL Label */ 
256  return (__retres1);
257}
258
259void eval(void) 
260{ int tmp ;
261  int tmp___0 ;
262  int tmp___1 ;
263  int tmp___2 ;
264//  int __VERIFIER_nondet_int();
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
↑