Showing error 235

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_1.cil.c
Line in file: 14
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
  9void error(void) 
 10{ 
 11
 12  {
 13  goto ERROR;
 14  ERROR: ;
 15  return;
 16}
 17}
 18
 19int q_buf_0  ;
 20int q_free  ;
 21int q_read_ev  ;
 22int q_write_ev  ;
 23int p_num_write  ;
 24int p_last_write  ;
 25int p_dw_st  ;
 26int p_dw_pc  ;
 27int p_dw_i  ;
 28int c_num_read  ;
 29int c_last_read  ;
 30int c_dr_st  ;
 31int c_dr_pc  ;
 32int c_dr_i  ;
 33int is_do_write_p_triggered(void) 
 34{ int __retres1 ;
 35
 36  {
 37  if ((int )p_dw_pc == 1) {
 38    if ((int )q_read_ev == 1) {
 39      __retres1 = 1;
 40      goto return_label;
 41    } else {
 42
 43    }
 44  } else {
 45
 46  }
 47  __retres1 = 0;
 48  return_label: /* CIL Label */ 
 49  return (__retres1);
 50}
 51}
 52int is_do_read_c_triggered(void) 
 53{ int __retres1 ;
 54
 55  {
 56  if ((int )c_dr_pc == 1) {
 57    if ((int )q_write_ev == 1) {
 58      __retres1 = 1;
 59      goto return_label;
 60    } else {
 61
 62    }
 63  } else {
 64
 65  }
 66  __retres1 = 0;
 67  return_label: /* CIL Label */ 
 68  return (__retres1);
 69}
 70}
 71void immediate_notify_threads(void) 
 72{ int tmp ;
 73  int tmp___0 ;
 74
 75  {
 76  {
 77  tmp = is_do_write_p_triggered();
 78  }
 79  if (tmp) {
 80    p_dw_st = 0;
 81  } else {
 82
 83  }
 84  {
 85  tmp___0 = is_do_read_c_triggered();
 86  }
 87  if (tmp___0) {
 88    c_dr_st = 0;
 89  } else {
 90
 91  }
 92
 93  return;
 94}
 95}
 96void do_write_p(void) 
 97{ 
 98
 99//  int __VERIFIER_nondet_int();
100
101  {
102  if ((int )p_dw_pc == 0) {
103    goto DW_ENTRY;
104  } else {
105    if ((int )p_dw_pc == 1) {
106      goto DW_WAIT_READ;
107    } else {
108
109    }
110  }
111  DW_ENTRY: 
112  {
113  while (1) {
114    while_0_continue: /* CIL Label */ ;
115    if ((int )q_free == 0) {
116      p_dw_st = 2;
117      p_dw_pc = 1;
118
119      goto return_label;
120      DW_WAIT_READ: ;
121    } else {
122
123    }
124    {
125    q_buf_0 = __VERIFIER_nondet_int();
126    p_last_write = q_buf_0;
127    p_num_write += 1;
128    q_free = 0;
129    q_write_ev = 1;
130    immediate_notify_threads();
131    q_write_ev = 2;
132    }
133  }
134  while_0_break: /* CIL Label */ ;
135  }
136  return_label: /* CIL Label */ 
137  return;
138}
139}
140static int a_t  ;
141void do_read_c(void) 
142{ int a ;
143
144  {
145  if ((int )c_dr_pc == 0) {
146    goto DR_ENTRY;
147  } else {
148    if ((int )c_dr_pc == 1) {
149      goto DR_WAIT_WRITE;
150    } else {
151
152    }
153  }
154  DR_ENTRY: 
155  {
156  while (1) {
157    while_1_continue: /* CIL Label */ ;
158    if ((int )q_free == 1) {
159      c_dr_st = 2;
160      c_dr_pc = 1;
161      a_t = a;
162
163      goto return_label;
164      DR_WAIT_WRITE: 
165      a = a_t;
166    } else {
167
168    }
169    {
170    a = q_buf_0;
171    c_last_read = a;
172    c_num_read += 1;
173    q_free = 1;
174    q_read_ev = 1;
175    immediate_notify_threads();
176    q_read_ev = 2;
177    }
178    if (p_last_write == c_last_read) {
179      if (p_num_write == c_num_read) {
180
181      } else {
182        {
183        error();
184        }
185      }
186    } else {
187      {
188      error();
189      }
190    }
191  }
192  while_1_break: /* CIL Label */ ;
193  }
194  return_label: /* CIL Label */ 
195  return;
196}
197}
198void init_threads(void) 
199{ 
200
201  {
202  if ((int )p_dw_i == 1) {
203    p_dw_st = 0;
204  } else {
205    p_dw_st = 2;
206  }
207  if ((int )c_dr_i == 1) {
208    c_dr_st = 0;
209  } else {
210    c_dr_st = 2;
211  }
212
213  return;
214}
215}
216int exists_runnable_thread(void) 
217{ int __retres1 ;
218
219  {
220  if ((int )p_dw_st == 0) {
221    __retres1 = 1;
222    goto return_label;
223  } else {
224    if ((int )c_dr_st == 0) {
225      __retres1 = 1;
226      goto return_label;
227    } else {
228
229    }
230  }
231  __retres1 = 0;
232  return_label: /* CIL Label */ 
233  return (__retres1);
234}
235}
236void eval(void) 
237{ int tmp ;
238  int tmp___0 ;
239  int tmp___1 ;
240//  int __VERIFIER_nondet_int(); 
241
242  {
243  {
244  while (1) {
245    while_2_continue: /* CIL Label */ ;
246    {
247    tmp___1 = exists_runnable_thread();
248    }
249    if (tmp___1) {
250
251    } else {
252      goto while_2_break;
253    }
254    if ((int )p_dw_st == 0) {
255      {
256        tmp = __VERIFIER_nondet_int();
257      }
258      if (tmp) {
259        {
260        p_dw_st = 1;
261        do_write_p();
262        }
263      } else {
264
265      }
266    } else {
267
268    }
269    if ((int )c_dr_st == 0) {
270      {
271        tmp___0 = __VERIFIER_nondet_int();
272      }
273      if (tmp___0) {
274        {
275        c_dr_st = 1;
276        do_read_c();
277        }
278      } else {
279
280      }
281    } else {
282
283    }
284  }
285  while_2_break: /* CIL Label */ ;
286  }
287
288  return;
289}
290}
291int stop_simulation(void) 
292{ int tmp ;
293  int __retres2 ;
294
295  {
296  {
297  tmp = exists_runnable_thread();
298  }
299  if (tmp) {
300    __retres2 = 0;
301    goto return_label;
302  } else {
303
304  }
305  __retres2 = 1;
306  return_label: /* CIL Label */ 
307  return (__retres2);
308}
309}
310void start_simulation(void) 
311{ int kernel_st ;
312  int tmp ;
313
314  {
315  {
316  kernel_st = 0;
317  init_threads();
318  }
319  {
320  while (1) {
321    while_3_continue: /* CIL Label */ ;
322    {
323    kernel_st = 1;
324    eval();
325    tmp = stop_simulation();
326    }
327    if (tmp) {
328      goto while_3_break;
329    } else {
330
331    }
332  }
333  while_3_break: /* CIL Label */ ;
334  }
335
336  return;
337}
338}
339void init_model(void) 
340{ 
341
342  {
343  q_free = 1;
344  q_write_ev = 2;
345  q_read_ev = q_write_ev;
346  p_num_write = 0;
347  p_dw_pc = 0;
348  p_dw_i = 1;
349  c_num_read = 0;
350  c_dr_pc = 0;
351  c_dr_i = 1;
352
353  return;
354}
355}
356int main(void) 
357{ int __retres1 ;
358
359  {
360  {
361  init_model();
362  start_simulation();
363  }
364  __retres1 = 0;
365  return (__retres1);
366}
367}
↑