Showing error 2320

User: Jiri Slaby
Error type: Reachable Error Location
Error type description: A specified error location is reachable in some program path
File location: systemc/toy_safe.cil.c
Line in file: 12
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/* Generated by CIL v. 1.3.6 */
  3/* print_CIL_Input is true */
  4
  5
  6
  7void error(void) 
  8{ 
  9
 10  {
 11  goto ERROR;
 12  ERROR: ;
 13  return;
 14}
 15}
 16
 17int c  ;
 18int c_t  ;
 19int c_req_up  ;
 20int p_in  ;
 21int p_out  ;
 22int wl_st  ;
 23int c1_st  ;
 24int c2_st  ;
 25int wb_st  ;
 26int r_st  ;
 27int wl_i  ;
 28int c1_i  ;
 29int c2_i  ;
 30int wb_i  ;
 31int r_i  ;
 32int wl_pc  ;
 33int c1_pc  ;
 34int c2_pc  ;
 35int wb_pc  ;
 36int e_e  ;
 37int e_f  ;
 38int e_g  ;
 39int e_c  ;
 40int e_p_in  ;
 41int e_wl  ;
 42void write_loop(void) ;
 43void compute1(void) ;
 44void compute2(void) ;
 45void write_back(void) ;
 46void read(void) ;
 47int d  ;
 48int data  ;
 49int processed  ;
 50static int t_b  ;
 51void write_loop(void) 
 52{ int t ;
 53
 54  {
 55  if ((int )wl_pc == 0) {
 56    goto WL_ENTRY_LOC;
 57  } else {
 58    if ((int )wl_pc == 2) {
 59      goto WL_WAIT_2_LOC;
 60    } else {
 61      if ((int )wl_pc == 1) {
 62        goto WL_WAIT_1_LOC;
 63      } else {
 64
 65      }
 66    }
 67  }
 68  WL_ENTRY_LOC: 
 69  wl_st = 2;
 70  wl_pc = 1;
 71  e_wl = 0;
 72
 73  goto return_label;
 74  WL_WAIT_1_LOC: 
 75  {
 76  while (1) {
 77    while_0_continue: /* CIL Label */ ;
 78    t = d;
 79    data = d;
 80    processed = 0;
 81    e_f = 1;
 82    if ((int )c1_pc == 1) {
 83      if ((int )e_f == 1) {
 84        c1_st = 0;
 85      } else {
 86
 87      }
 88    } else {
 89
 90    }
 91    if ((int )c2_pc == 1) {
 92      if ((int )e_f == 1) {
 93        c2_st = 0;
 94      } else {
 95
 96      }
 97    } else {
 98
 99    }
100    e_f = 2;
101    wl_st = 2;
102    wl_pc = 2;
103    t_b = t;
104
105    goto return_label;
106    WL_WAIT_2_LOC: 
107    t = t_b;
108    if (d == t + 1) {
109
110    } else {
111      if (d == t + 2) {
112
113      } else {
114        {
115        error();
116        }
117      }
118    }
119  }
120  while_0_break: /* CIL Label */ ;
121  }
122  return_label: /* CIL Label */ 
123  return;
124}
125}
126void compute1(void) 
127{ 
128
129  {
130  if ((int )c1_pc == 0) {
131    goto C1_ENTRY_LOC;
132  } else {
133    if ((int )c1_pc == 1) {
134      goto C1_WAIT_LOC;
135    } else {
136
137    }
138  }
139  C1_ENTRY_LOC: 
140  {
141  while (1) {
142    while_1_continue: /* CIL Label */ ;
143    c1_st = 2;
144    c1_pc = 1;
145
146    goto return_label;
147    C1_WAIT_LOC: 
148    if (! processed) {
149      data += 1;
150      e_g = 1;
151      if ((int )wb_pc == 1) {
152        if ((int )e_g == 1) {
153          wb_st = 0;
154        } else {
155
156        }
157      } else {
158
159      }
160      e_g = 2;
161    } else {
162
163    }
164  }
165  while_1_break: /* CIL Label */ ;
166  }
167  return_label: /* CIL Label */ 
168  return;
169}
170}
171void compute2(void) 
172{ 
173
174  {
175  if ((int )c2_pc == 0) {
176    goto C2_ENTRY_LOC;
177  } else {
178    if ((int )c2_pc == 1) {
179      goto C2_WAIT_LOC;
180    } else {
181
182    }
183  }
184  C2_ENTRY_LOC: 
185  {
186  while (1) {
187    while_2_continue: /* CIL Label */ ;
188    c2_st = 2;
189    c2_pc = 1;
190
191    goto return_label;
192    C2_WAIT_LOC: 
193    if (! processed) {
194      data += 1;
195      e_g = 1;
196      if ((int )wb_pc == 1) {
197        if ((int )e_g == 1) {
198          wb_st = 0;
199        } else {
200
201        }
202      } else {
203
204      }
205      e_g = 2;
206    } else {
207
208    }
209  }
210  while_2_break: /* CIL Label */ ;
211  }
212  return_label: /* CIL Label */ 
213  return;
214}
215}
216void write_back(void) 
217{ 
218
219  {
220  if ((int )wb_pc == 0) {
221    goto WB_ENTRY_LOC;
222  } else {
223    if ((int )wb_pc == 1) {
224      goto WB_WAIT_LOC;
225    } else {
226
227    }
228  }
229  WB_ENTRY_LOC: 
230  {
231  while (1) {
232    while_3_continue: /* CIL Label */ ;
233    wb_st = 2;
234    wb_pc = 1;
235
236    goto return_label;
237    WB_WAIT_LOC: 
238    c_t = data;
239    c_req_up = 1;
240    processed = 1;
241  }
242  while_3_break: /* CIL Label */ ;
243  }
244  return_label: /* CIL Label */ 
245  return;
246}
247}
248void read(void) 
249{ 
250
251  {
252  d = c;
253  e_e = 1;
254  if ((int )wl_pc == 1) {
255    if ((int )e_wl == 1) {
256      wl_st = 0;
257    } else {
258      goto _L;
259    }
260  } else {
261    _L: /* CIL Label */ 
262    if ((int )wl_pc == 2) {
263      if ((int )e_e == 1) {
264        wl_st = 0;
265      } else {
266
267      }
268    } else {
269
270    }
271  }
272  e_e = 2;
273  r_st = 2;
274
275  return;
276}
277}
278void eval(void) 
279{ int tmp ;
280  int tmp___0 ;
281  int tmp___1 ;
282  int tmp___2 ;
283  int tmp___3 ;
284
285  {
286  {
287  while (1) {
288    while_4_continue: /* CIL Label */ ;
289    if ((int )wl_st == 0) {
290
291    } else {
292      if ((int )c1_st == 0) {
293
294      } else {
295        if ((int )c2_st == 0) {
296
297        } else {
298          if ((int )wb_st == 0) {
299
300          } else {
301            if ((int )r_st == 0) {
302
303            } else {
304              goto while_4_break;
305            }
306          }
307        }
308      }
309    }
310    if ((int )wl_st == 0) {
311      {
312        tmp =  __VERIFIER_nondet_int(); 
313      }
314      if (tmp) {
315        {
316        wl_st = 1;
317        write_loop();
318        }
319      } else {
320
321      }
322    } else {
323
324    }
325    if ((int )c1_st == 0) {
326      {
327        tmp___0 =  __VERIFIER_nondet_int(); 
328      }
329      if (tmp___0) {
330        {
331        c1_st = 1;
332        compute1();
333        }
334      } else {
335
336      }
337    } else {
338
339    }
340    if ((int )c2_st == 0) {
341      {
342        tmp___1 =  __VERIFIER_nondet_int(); 
343      }
344      if (tmp___1) {
345        {
346        c2_st = 1;
347        compute2();
348        }
349      } else {
350
351      }
352    } else {
353
354    }
355    if ((int )wb_st == 0) {
356      {
357        tmp___2 =  __VERIFIER_nondet_int(); 
358      }
359      if (tmp___2) {
360        {
361        wb_st = 1;
362        write_back();
363        }
364      } else {
365
366      }
367    } else {
368
369    }
370    if ((int )r_st == 0) {
371      {
372        tmp___3 = __VERIFIER_nondet_int();
373      }
374      if (tmp___3) {
375        {
376        r_st = 1;
377        read();
378        }
379      } else {
380
381      }
382    } else {
383
384    }
385  }
386  while_4_break: /* CIL Label */ ;
387  }
388
389  return;
390}
391}
392void start_simulation(void) 
393{ int kernel_st ;
394
395  {
396  kernel_st = 0;
397  if ((int )c_req_up == 1) {
398    if (c != c_t) {
399      c = c_t;
400      e_c = 0;
401    } else {
402
403    }
404    c_req_up = 0;
405  } else {
406
407  }
408  if ((int )wl_i == 1) {
409    wl_st = 0;
410  } else {
411    wl_st = 2;
412  }
413  if ((int )c1_i == 1) {
414    c1_st = 0;
415  } else {
416    c1_st = 2;
417  }
418  if ((int )c2_i == 1) {
419    c2_st = 0;
420  } else {
421    c2_st = 2;
422  }
423  if ((int )wb_i == 1) {
424    wb_st = 0;
425  } else {
426    wb_st = 2;
427  }
428  if ((int )r_i == 1) {
429    r_st = 0;
430  } else {
431    r_st = 2;
432  }
433  if ((int )e_f == 0) {
434    e_f = 1;
435  } else {
436
437  }
438  if ((int )e_g == 0) {
439    e_g = 1;
440  } else {
441
442  }
443  if ((int )e_e == 0) {
444    e_e = 1;
445  } else {
446
447  }
448  if ((int )e_c == 0) {
449    e_c = 1;
450  } else {
451
452  }
453  if ((int )e_wl == 0) {
454    e_wl = 1;
455  } else {
456
457  }
458  if ((int )wl_pc == 1) {
459    if ((int )e_wl == 1) {
460      wl_st = 0;
461    } else {
462      goto _L;
463    }
464  } else {
465    _L: /* CIL Label */ 
466    if ((int )wl_pc == 2) {
467      if ((int )e_e == 1) {
468        wl_st = 0;
469      } else {
470
471      }
472    } else {
473
474    }
475  }
476  if ((int )c1_pc == 1) {
477    if ((int )e_f == 1) {
478      c1_st = 0;
479    } else {
480
481    }
482  } else {
483
484  }
485  if ((int )c2_pc == 1) {
486    if ((int )e_f == 1) {
487      c2_st = 0;
488    } else {
489
490    }
491  } else {
492
493  }
494  if ((int )wb_pc == 1) {
495    if ((int )e_g == 1) {
496      wb_st = 0;
497    } else {
498
499    }
500  } else {
501
502  }
503  if ((int )e_c == 1) {
504    r_st = 0;
505  } else {
506
507  }
508  if ((int )e_e == 1) {
509    e_e = 2;
510  } else {
511
512  }
513  if ((int )e_f == 1) {
514    e_f = 2;
515  } else {
516
517  }
518  if ((int )e_g == 1) {
519    e_g = 2;
520  } else {
521
522  }
523  if ((int )e_c == 1) {
524    e_c = 2;
525  } else {
526
527  }
528  if ((int )e_wl == 1) {
529    e_wl = 2;
530  } else {
531
532  }
533  {
534  while (1) {
535    while_5_continue: /* CIL Label */ ;
536    {
537    kernel_st = 1;
538    eval();
539    }
540    kernel_st = 2;
541    if ((int )c_req_up == 1) {
542      if (c != c_t) {
543        c = c_t;
544        e_c = 0;
545      } else {
546
547      }
548      c_req_up = 0;
549    } else {
550
551    }
552    kernel_st = 3;
553    if ((int )e_f == 0) {
554      e_f = 1;
555    } else {
556
557    }
558    if ((int )e_g == 0) {
559      e_g = 1;
560    } else {
561
562    }
563    if ((int )e_e == 0) {
564      e_e = 1;
565    } else {
566
567    }
568    if ((int )e_c == 0) {
569      e_c = 1;
570    } else {
571
572    }
573    if ((int )e_wl == 0) {
574      e_wl = 1;
575    } else {
576
577    }
578    if ((int )wl_pc == 1) {
579      if ((int )e_wl == 1) {
580        wl_st = 0;
581      } else {
582        goto _L___0;
583      }
584    } else {
585      _L___0: /* CIL Label */ 
586      if ((int )wl_pc == 2) {
587        if ((int )e_e == 1) {
588          wl_st = 0;
589        } else {
590
591        }
592      } else {
593
594      }
595    }
596    if ((int )c1_pc == 1) {
597      if ((int )e_f == 1) {
598        c1_st = 0;
599      } else {
600
601      }
602    } else {
603
604    }
605    if ((int )c2_pc == 1) {
606      if ((int )e_f == 1) {
607        c2_st = 0;
608      } else {
609
610      }
611    } else {
612
613    }
614    if ((int )wb_pc == 1) {
615      if ((int )e_g == 1) {
616        wb_st = 0;
617      } else {
618
619      }
620    } else {
621
622    }
623    if ((int )e_c == 1) {
624      r_st = 0;
625    } else {
626
627    }
628    if ((int )e_e == 1) {
629      e_e = 2;
630    } else {
631
632    }
633    if ((int )e_f == 1) {
634      e_f = 2;
635    } else {
636
637    }
638    if ((int )e_g == 1) {
639      e_g = 2;
640    } else {
641
642    }
643    if ((int )e_c == 1) {
644      e_c = 2;
645    } else {
646
647    }
648    if ((int )e_wl == 1) {
649      e_wl = 2;
650    } else {
651
652    }
653    if ((int )wl_st == 0) {
654
655    } else {
656      if ((int )c1_st == 0) {
657
658      } else {
659        if ((int )c2_st == 0) {
660
661        } else {
662          if ((int )wb_st == 0) {
663
664          } else {
665            if ((int )r_st == 0) {
666
667            } else {
668              goto while_5_break;
669            }
670          }
671        }
672      }
673    }
674  }
675  while_5_break: /* CIL Label */ ;
676  }
677
678  return;
679}
680}
681int main(void) 
682{ int __retres1 ;
683
684  {
685  {
686  e_wl = 2;
687  e_c = e_wl;
688  e_g = e_c;
689  e_f = e_g;
690  e_e = e_f;
691  wl_pc = 0;
692  c1_pc = 0;
693  c2_pc = 0;
694  wb_pc = 0;
695  wb_i = 1;
696  c2_i = wb_i;
697  c1_i = c2_i;
698  wl_i = c1_i;
699  r_i = 0;
700  c_req_up = 0;
701  d = 0;
702  c = 0;
703  start_simulation();
704  }
705  __retres1 = 0;
706  return (__retres1);
707}
708}
↑