Showing error 2287

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