Showing error 1472

User: Jiri Slaby
Error type: Reachable Error Location
Error type description: A specified error location is reachable in some program path
File location: loops/bist.cell_safe.i
Line in file: 7
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();
  2void error(void)
  3{
  4
  5  {
  6  goto ERROR;
  7  ERROR: ;
  8  return;
  9}
 10}
 11
 12int b0_val ;
 13int b0_val_t ;
 14int b0_ev ;
 15int b0_req_up ;
 16int b1_val ;
 17int b1_val_t ;
 18int b1_ev ;
 19int b1_req_up ;
 20int d0_val ;
 21int d0_val_t ;
 22int d0_ev ;
 23int d0_req_up ;
 24int d1_val ;
 25int d1_val_t ;
 26int d1_ev ;
 27int d1_req_up ;
 28int z_val ;
 29int z_val_t ;
 30int z_ev ;
 31int z_req_up ;
 32int comp_m1_st ;
 33int comp_m1_i ;
 34void method1(void)
 35{ int s1 ;
 36  int s2 ;
 37  int s3 ;
 38
 39  {
 40  if (b0_val) {
 41    if (d1_val) {
 42      s1 = 0;
 43    } else {
 44      s1 = 1;
 45    }
 46  } else {
 47    s1 = 1;
 48  }
 49  if (d0_val) {
 50    if (b1_val) {
 51      s2 = 0;
 52    } else {
 53      s2 = 1;
 54    }
 55  } else {
 56    s2 = 1;
 57  }
 58  if (s2) {
 59    s3 = 0;
 60  } else {
 61    if (s1) {
 62      s3 = 0;
 63    } else {
 64      s3 = 1;
 65    }
 66  }
 67  if (s2) {
 68    if (s1) {
 69      s2 = 1;
 70    } else {
 71      s2 = 0;
 72    }
 73  } else {
 74    s2 = 0;
 75  }
 76  if (s2) {
 77    z_val_t = 0;
 78  } else {
 79    if (s3) {
 80      z_val_t = 0;
 81    } else {
 82      z_val_t = 1;
 83    }
 84  }
 85  z_req_up = 1;
 86  comp_m1_st = 2;
 87
 88  return;
 89}
 90}
 91int is_method1_triggered(void)
 92{ int __retres1 ;
 93
 94  {
 95  if ((int )b0_ev == 1) {
 96    __retres1 = 1;
 97    goto return_label;
 98  } else {
 99    if ((int )b1_ev == 1) {
100      __retres1 = 1;
101      goto return_label;
102    } else {
103      if ((int )d0_ev == 1) {
104        __retres1 = 1;
105        goto return_label;
106      } else {
107        if ((int )d1_ev == 1) {
108          __retres1 = 1;
109          goto return_label;
110        } else {
111
112        }
113      }
114    }
115  }
116  __retres1 = 0;
117  return_label:
118  return (__retres1);
119}
120}
121void update_b0(void)
122{
123
124  {
125  if ((int )b0_val != (int )b0_val_t) {
126    b0_val = b0_val_t;
127    b0_ev = 0;
128  } else {
129
130  }
131  b0_req_up = 0;
132
133  return;
134}
135}
136void update_b1(void)
137{
138
139  {
140  if ((int )b1_val != (int )b1_val_t) {
141    b1_val = b1_val_t;
142    b1_ev = 0;
143  } else {
144
145  }
146  b1_req_up = 0;
147
148  return;
149}
150}
151void update_d0(void)
152{
153
154  {
155  if ((int )d0_val != (int )d0_val_t) {
156    d0_val = d0_val_t;
157    d0_ev = 0;
158  } else {
159
160  }
161  d0_req_up = 0;
162
163  return;
164}
165}
166void update_d1(void)
167{
168
169  {
170  if ((int )d1_val != (int )d1_val_t) {
171    d1_val = d1_val_t;
172    d1_ev = 0;
173  } else {
174
175  }
176  d1_req_up = 0;
177
178  return;
179}
180}
181void update_z(void)
182{
183
184  {
185  if ((int )z_val != (int )z_val_t) {
186    z_val = z_val_t;
187    z_ev = 0;
188  } else {
189
190  }
191  z_req_up = 0;
192
193  return;
194}
195}
196void update_channels(void)
197{
198
199  {
200  if ((int )b0_req_up == 1) {
201    {
202    update_b0();
203    }
204  } else {
205
206  }
207  if ((int )b1_req_up == 1) {
208    {
209    update_b1();
210    }
211  } else {
212
213  }
214  if ((int )d0_req_up == 1) {
215    {
216    update_d0();
217    }
218  } else {
219
220  }
221  if ((int )d1_req_up == 1) {
222    {
223    update_d1();
224    }
225  } else {
226
227  }
228  if ((int )z_req_up == 1) {
229    {
230    update_z();
231    }
232  } else {
233
234  }
235
236  return;
237}
238}
239void init_threads(void)
240{
241
242  {
243  if ((int )comp_m1_i == 1) {
244    comp_m1_st = 0;
245  } else {
246    comp_m1_st = 2;
247  }
248
249  return;
250}
251}
252int exists_runnable_thread(void)
253{ int __retres1 ;
254
255  {
256  if ((int )comp_m1_st == 0) {
257    __retres1 = 1;
258    goto return_label;
259  } else {
260
261  }
262  __retres1 = 0;
263  return_label:
264  return (__retres1);
265}
266}
267void eval(void)
268{ int tmp ;
269  int tmp___0 ;
270
271
272  {
273  {
274  while (1) {
275    while_0_continue: ;
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: ;
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:
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: ;
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: ;
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}
↑