Showing error 237

User: Jiri Slaby
Error type: Reachable Error Location
Error type description: A specified error location is reachable in some program path
File location: systemc/pc_sfifo_2.cil.c
Line in file: 15
Project: SV-COMP 2012
Tools: Manual Work
Entered: 2012-11-19 13:47:39 UTC

Source: 

  1/*int nondet(void)
  2{
  3  int x;
  4  {
  5    return (x);
  6  }
  7  }*/
  8
  9
 10void error(void) 
 11{ 
 12
 13  {
 14  goto ERROR;
 15  ERROR: ;
 16  return;
 17}
 18}
 19
 20int q_buf_0  ;
 21int q_free  ;
 22int q_read_ev  ;
 23int q_write_ev  ;
 24int q_req_up  ;
 25int q_ev  ;
 26void update_fifo_q(void) 
 27{ 
 28
 29  {
 30  if ((int )q_free == 0) {
 31    q_write_ev = 0;
 32  } else {
 33
 34  }
 35  if ((int )q_free == 1) {
 36    q_read_ev = 0;
 37  } else {
 38
 39  }
 40  q_ev = 0;
 41  q_req_up = 0;
 42
 43  return;
 44}
 45}
 46int p_num_write  ;
 47int p_last_write  ;
 48int p_dw_st  ;
 49int p_dw_pc  ;
 50int p_dw_i  ;
 51int c_num_read  ;
 52int c_last_read  ;
 53int c_dr_st  ;
 54int c_dr_pc  ;
 55int c_dr_i  ;
 56int is_do_write_p_triggered(void) 
 57{ int __retres1 ;
 58
 59  {
 60  if ((int )p_dw_pc == 1) {
 61    if ((int )q_read_ev == 1) {
 62      __retres1 = 1;
 63      goto return_label;
 64    } else {
 65
 66    }
 67  } else {
 68
 69  }
 70  __retres1 = 0;
 71  return_label: /* CIL Label */ 
 72  return (__retres1);
 73}
 74}
 75int is_do_read_c_triggered(void) 
 76{ int __retres1 ;
 77
 78  {
 79  if ((int )c_dr_pc == 1) {
 80    if ((int )q_write_ev == 1) {
 81      __retres1 = 1;
 82      goto return_label;
 83    } else {
 84
 85    }
 86  } else {
 87
 88  }
 89  __retres1 = 0;
 90  return_label: /* CIL Label */ 
 91  return (__retres1);
 92}
 93}
 94void immediate_notify_threads(void) 
 95{ int tmp ;
 96  int tmp___0 ;
 97
 98  {
 99  {
100  tmp = is_do_write_p_triggered();
101  }
102  if (tmp) {
103    p_dw_st = 0;
104  } else {
105
106  }
107  {
108  tmp___0 = is_do_read_c_triggered();
109  }
110  if (tmp___0) {
111    c_dr_st = 0;
112  } else {
113
114  }
115
116  return;
117}
118}
119void do_write_p(void) 
120{ 
121//  int __VERIFIER_nondet_int();
122
123  {
124  if ((int )p_dw_pc == 0) {
125    goto DW_ENTRY;
126  } else {
127    if ((int )p_dw_pc == 1) {
128      goto DW_WAIT_READ;
129    } else {
130
131    }
132  }
133  DW_ENTRY: 
134  {
135  while (1) {
136    while_0_continue: /* CIL Label */ ;
137    if ((int )q_free == 0) {
138      p_dw_st = 2;
139      p_dw_pc = 1;
140
141      goto return_label;
142      DW_WAIT_READ: ;
143    } else {
144
145    }
146    {
147      q_buf_0 = __VERIFIER_nondet_int();
148    p_last_write = q_buf_0;
149    p_num_write += 1;
150    q_free = 0;
151    q_req_up = 1;
152    }
153  }
154  while_0_break: /* CIL Label */ ;
155  }
156  return_label: /* CIL Label */ 
157  return;
158}
159}
160static int a_t  ;
161void do_read_c(void) 
162{ int a ;
163
164  {
165  if ((int )c_dr_pc == 0) {
166    goto DR_ENTRY;
167  } else {
168    if ((int )c_dr_pc == 1) {
169      goto DR_WAIT_WRITE;
170    } else {
171
172    }
173  }
174  DR_ENTRY: 
175  {
176  while (1) {
177    while_1_continue: /* CIL Label */ ;
178    if ((int )q_free == 1) {
179      c_dr_st = 2;
180      c_dr_pc = 1;
181      a_t = a;
182
183      goto return_label;
184      DR_WAIT_WRITE: 
185      a = a_t;
186    } else {
187
188    }
189    a = q_buf_0;
190    c_last_read = a;
191    c_num_read += 1;
192    q_free = 1;
193    q_req_up = 1;
194    if (p_last_write == c_last_read) {
195      if (p_num_write == c_num_read) {
196
197      } else {
198        {
199        error();
200        }
201      }
202    } else {
203      {
204      error();
205      }
206    }
207  }
208  while_1_break: /* CIL Label */ ;
209  }
210  return_label: /* CIL Label */ 
211  return;
212}
213}
214void update_channels(void) 
215{ 
216
217  {
218  if ((int )q_req_up == 1) {
219    {
220    update_fifo_q();
221    }
222  } else {
223
224  }
225
226  return;
227}
228}
229void init_threads(void) 
230{ 
231
232  {
233  if ((int )p_dw_i == 1) {
234    p_dw_st = 0;
235  } else {
236    p_dw_st = 2;
237  }
238  if ((int )c_dr_i == 1) {
239    c_dr_st = 0;
240  } else {
241    c_dr_st = 2;
242  }
243
244  return;
245}
246}
247int exists_runnable_thread(void) 
248{ int __retres1 ;
249
250  {
251  if ((int )p_dw_st == 0) {
252    __retres1 = 1;
253    goto return_label;
254  } else {
255    if ((int )c_dr_st == 0) {
256      __retres1 = 1;
257      goto return_label;
258    } else {
259
260    }
261  }
262  __retres1 = 0;
263  return_label: /* CIL Label */ 
264  return (__retres1);
265}
266}
267void fire_delta_events(void) 
268{ 
269
270  {
271  if ((int )q_read_ev == 0) {
272    q_read_ev = 1;
273  } else {
274
275  }
276  if ((int )q_write_ev == 0) {
277    q_write_ev = 1;
278  } else {
279
280  }
281
282  return;
283}
284}
285void reset_delta_events(void) 
286{ 
287
288  {
289  if ((int )q_read_ev == 1) {
290    q_read_ev = 2;
291  } else {
292
293  }
294  if ((int )q_write_ev == 1) {
295    q_write_ev = 2;
296  } else {
297
298  }
299
300  return;
301}
302}
303void activate_threads(void) 
304{ int tmp ;
305  int tmp___0 ;
306
307  {
308  {
309  tmp = is_do_write_p_triggered();
310  }
311  if (tmp) {
312    p_dw_st = 0;
313  } else {
314
315  }
316  {
317  tmp___0 = is_do_read_c_triggered();
318  }
319  if (tmp___0) {
320    c_dr_st = 0;
321  } else {
322
323  }
324
325  return;
326}
327}
328void eval(void) 
329{ int tmp ;
330  int tmp___0 ;
331  int tmp___1 ;
332//  int __VERIFIER_nondet_int(); 
333
334  {
335  {
336  while (1) {
337    while_2_continue: /* CIL Label */ ;
338    {
339    tmp___1 = exists_runnable_thread();
340    }
341    if (tmp___1) {
342
343    } else {
344      goto while_2_break;
345    }
346    if ((int )p_dw_st == 0) {
347      {
348        tmp = __VERIFIER_nondet_int();
349      }
350      if (tmp) {
351        {
352        p_dw_st = 1;
353        do_write_p();
354        }
355      } else {
356
357      }
358    } else {
359
360    }
361    if ((int )c_dr_st == 0) {
362      {
363        tmp___0 = __VERIFIER_nondet_int();
364      }
365      if (tmp___0) {
366        {
367        c_dr_st = 1;
368        do_read_c();
369        }
370      } else {
371
372      }
373    } else {
374
375    }
376  }
377  while_2_break: /* CIL Label */ ;
378  }
379
380  return;
381}
382}
383int stop_simulation(void) 
384{ int tmp ;
385  int __retres2 ;
386
387  {
388  {
389  tmp = exists_runnable_thread();
390  }
391  if (tmp) {
392    __retres2 = 0;
393    goto return_label;
394  } else {
395
396  }
397  __retres2 = 1;
398  return_label: /* CIL Label */ 
399  return (__retres2);
400}
401}
402void start_simulation(void) 
403{ int kernel_st ;
404  int tmp ;
405
406  {
407  {
408  kernel_st = 0;
409  update_channels();
410  init_threads();
411  fire_delta_events();
412  activate_threads();
413  reset_delta_events();
414  }
415  {
416  while (1) {
417    while_3_continue: /* CIL Label */ ;
418    {
419    kernel_st = 1;
420    eval();
421    }
422    {
423    kernel_st = 2;
424    update_channels();
425    }
426    {
427    kernel_st = 3;
428    fire_delta_events();
429    activate_threads();
430    reset_delta_events();
431    tmp = stop_simulation();
432    }
433    if (tmp) {
434      goto while_3_break;
435    } else {
436
437    }
438  }
439  while_3_break: /* CIL Label */ ;
440  }
441
442  return;
443}
444}
445void init_model(void) 
446{ 
447
448  {
449  q_free = 1;
450  q_write_ev = 2;
451  q_read_ev = q_write_ev;
452  p_num_write = 0;
453  p_dw_pc = 0;
454  p_dw_i = 1;
455  c_num_read = 0;
456  c_dr_pc = 0;
457  c_dr_i = 1;
458
459  return;
460}
461}
462int main(void) 
463{ int __retres1 ;
464
465  {
466  {
467  init_model();
468  start_simulation();
469  }
470  __retres1 = 0;
471  return (__retres1);
472}
473}
↑