Showing error 225

User: Jiri Slaby
Error type: Reachable Error Location
Error type description: A specified error location is reachable in some program path
File location: systemc/bist_cell.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 b0_val  ;
 20int b0_val_t  ;
 21int b0_ev  ;
 22int b0_req_up  ;
 23int b1_val  ;
 24int b1_val_t  ;
 25int b1_ev  ;
 26int b1_req_up  ;
 27int d0_val  ;
 28int d0_val_t  ;
 29int d0_ev  ;
 30int d0_req_up  ;
 31int d1_val  ;
 32int d1_val_t  ;
 33int d1_ev  ;
 34int d1_req_up  ;
 35int z_val  ;
 36int z_val_t  ;
 37int z_ev  ;
 38int z_req_up  ;
 39int comp_m1_st  ;
 40int comp_m1_i  ;
 41void method1(void) 
 42{ int s1 ;
 43  int s2 ;
 44  int s3 ;
 45
 46  {
 47  if (b0_val) {
 48    if (d1_val) {
 49      s1 = 0;
 50    } else {
 51      s1 = 1;
 52    }
 53  } else {
 54    s1 = 1;
 55  }
 56  if (d0_val) {
 57    if (b1_val) {
 58      s2 = 0;
 59    } else {
 60      s2 = 1;
 61    }
 62  } else {
 63    s2 = 1;
 64  }
 65  if (s2) {
 66    s3 = 0;
 67  } else {
 68    if (s1) {
 69      s3 = 0;
 70    } else {
 71      s3 = 1;
 72    }
 73  }
 74  if (s2) {
 75    if (s1) {
 76      s2 = 1;
 77    } else {
 78      s2 = 0;
 79    }
 80  } else {
 81    s2 = 0;
 82  }
 83  if (s2) {
 84    z_val_t = 0;
 85  } else {
 86    if (s3) {
 87      z_val_t = 0;
 88    } else {
 89      z_val_t = 1;
 90    }
 91  }
 92  z_req_up = 1;
 93  comp_m1_st = 2;
 94
 95  return;
 96}
 97}
 98int is_method1_triggered(void) 
 99{ int __retres1 ;
100
101  {
102  if ((int )b0_ev == 1) {
103    __retres1 = 1;
104    goto return_label;
105  } else {
106    if ((int )b1_ev == 1) {
107      __retres1 = 1;
108      goto return_label;
109    } else {
110      if ((int )d0_ev == 1) {
111        __retres1 = 1;
112        goto return_label;
113      } else {
114        if ((int )d1_ev == 1) {
115          __retres1 = 1;
116          goto return_label;
117        } else {
118
119        }
120      }
121    }
122  }
123  __retres1 = 0;
124  return_label: /* CIL Label */ 
125  return (__retres1);
126}
127}
128void update_b0(void) 
129{ 
130
131  {
132  if ((int )b0_val != (int )b0_val_t) {
133    b0_val = b0_val_t;
134    b0_ev = 0;
135  } else {
136
137  }
138  b0_req_up = 0;
139
140  return;
141}
142}
143void update_b1(void) 
144{ 
145
146  {
147  if ((int )b1_val != (int )b1_val_t) {
148    b1_val = b1_val_t;
149    b1_ev = 0;
150  } else {
151
152  }
153  b1_req_up = 0;
154
155  return;
156}
157}
158void update_d0(void) 
159{ 
160
161  {
162  if ((int )d0_val != (int )d0_val_t) {
163    d0_val = d0_val_t;
164    d0_ev = 0;
165  } else {
166
167  }
168  d0_req_up = 0;
169
170  return;
171}
172}
173void update_d1(void) 
174{ 
175
176  {
177  if ((int )d1_val != (int )d1_val_t) {
178    d1_val = d1_val_t;
179    d1_ev = 0;
180  } else {
181
182  }
183  d1_req_up = 0;
184
185  return;
186}
187}
188void update_z(void) 
189{ 
190
191  {
192  if ((int )z_val != (int )z_val_t) {
193    z_val = z_val_t;
194    z_ev = 0;
195  } else {
196
197  }
198  z_req_up = 0;
199
200  return;
201}
202}
203void update_channels(void) 
204{ 
205
206  {
207  if ((int )b0_req_up == 1) {
208    {
209    update_b0();
210    }
211  } else {
212
213  }
214  if ((int )b1_req_up == 1) {
215    {
216    update_b1();
217    }
218  } else {
219
220  }
221  if ((int )d0_req_up == 1) {
222    {
223    update_d0();
224    }
225  } else {
226
227  }
228  if ((int )d1_req_up == 1) {
229    {
230    update_d1();
231    }
232  } else {
233
234  }
235  if ((int )z_req_up == 1) {
236    {
237    update_z();
238    }
239  } else {
240
241  }
242
243  return;
244}
245}
246void init_threads(void) 
247{ 
248
249  {
250  if ((int )comp_m1_i == 1) {
251    comp_m1_st = 0;
252  } else {
253    comp_m1_st = 2;
254  }
255
256  return;
257}
258}
259int exists_runnable_thread(void) 
260{ int __retres1 ;
261
262  {
263  if ((int )comp_m1_st == 0) {
264    __retres1 = 1;
265    goto return_label;
266  } else {
267
268  }
269  __retres1 = 0;
270  return_label: /* CIL Label */ 
271  return (__retres1);
272}
273}
274void eval(void) 
275{ int tmp ;
276  int tmp___0 ;
277 // int __VERIFIER_nondet_int(); 
278
279  {
280  {
281  while (1) {
282    while_0_continue: /* CIL Label */ ;
283    {
284    tmp___0 = exists_runnable_thread();
285    }
286    if (tmp___0) {
287
288    } else {
289      goto while_0_break;
290    }
291    if ((int )comp_m1_st == 0) {
292      {
293        tmp = __VERIFIER_nondet_int(); 
294      }
295      if (tmp) {
296        {
297        comp_m1_st = 1;
298        method1();
299        }
300      } else {
301
302      }
303    } else {
304
305    }
306  }
307  while_0_break: /* CIL Label */ ;
308  }
309
310  return;
311}
312}
313void fire_delta_events(void) 
314{ 
315
316  {
317  if ((int )b0_ev == 0) {
318    b0_ev = 1;
319  } else {
320
321  }
322  if ((int )b1_ev == 0) {
323    b1_ev = 1;
324  } else {
325
326  }
327  if ((int )d0_ev == 0) {
328    d0_ev = 1;
329  } else {
330
331  }
332  if ((int )d1_ev == 0) {
333    d1_ev = 1;
334  } else {
335
336  }
337  if ((int )z_ev == 0) {
338    z_ev = 1;
339  } else {
340
341  }
342
343  return;
344}
345}
346void reset_delta_events(void) 
347{ 
348
349  {
350  if ((int )b0_ev == 1) {
351    b0_ev = 2;
352  } else {
353
354  }
355  if ((int )b1_ev == 1) {
356    b1_ev = 2;
357  } else {
358
359  }
360  if ((int )d0_ev == 1) {
361    d0_ev = 2;
362  } else {
363
364  }
365  if ((int )d1_ev == 1) {
366    d1_ev = 2;
367  } else {
368
369  }
370  if ((int )z_ev == 1) {
371    z_ev = 2;
372  } else {
373
374  }
375
376  return;
377}
378}
379void activate_threads(void) 
380{ int tmp ;
381
382  {
383  {
384  tmp = is_method1_triggered();
385  }
386  if (tmp) {
387    comp_m1_st = 0;
388  } else {
389
390  }
391
392  return;
393}
394}
395int stop_simulation(void) 
396{ int tmp ;
397  int __retres2 ;
398
399  {
400  {
401  tmp = exists_runnable_thread();
402  }
403  if (tmp) {
404    __retres2 = 0;
405    goto return_label;
406  } else {
407
408  }
409  __retres2 = 1;
410  return_label: /* CIL Label */ 
411  return (__retres2);
412}
413}
414void start_simulation(void) 
415{ int kernel_st ;
416  int tmp ;
417
418  {
419  {
420  kernel_st = 0;
421  update_channels();
422  init_threads();
423  fire_delta_events();
424  activate_threads();
425  reset_delta_events();
426  }
427  {
428  while (1) {
429    while_1_continue: /* CIL Label */ ;
430    {
431    kernel_st = 1;
432    eval();
433    }
434    {
435    kernel_st = 2;
436    update_channels();
437    }
438    {
439    kernel_st = 3;
440    fire_delta_events();
441    activate_threads();
442    reset_delta_events();
443    tmp = stop_simulation();
444    }
445    if (tmp) {
446      goto while_1_break;
447    } else {
448
449    }
450  }
451  while_1_break: /* CIL Label */ ;
452  }
453
454  return;
455}
456}
457void init_model(void) 
458{ 
459
460  {
461  b0_val = 0;
462  b0_ev = 2;
463  b0_req_up = 0;
464  b1_val = 0;
465  b1_ev = 2;
466  b1_req_up = 0;
467  d0_val = 0;
468  d0_ev = 2;
469  d0_req_up = 0;
470  d1_val = 0;
471  d1_ev = 2;
472  d1_req_up = 0;
473  z_val = 0;
474  z_ev = 2;
475  z_req_up = 0;
476  b0_val_t = 1;
477  b0_req_up = 1;
478  b1_val_t = 1;
479  b1_req_up = 1;
480  d0_val_t = 1;
481  d0_req_up = 1;
482  d1_val_t = 1;
483  d1_req_up = 1;
484  comp_m1_i = 0;
485
486  return;
487}
488}
489int main(void) 
490{ int __retres1 ;
491
492  {
493  {
494  init_model();
495  start_simulation();
496  }
497  if (! ((int )z_val == 0)) {
498    {
499    error();
500    }
501  } else {
502
503  }
504  __retres1 = 0;
505  return (__retres1);
506}
507}
↑