Showing error 2276

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