Showing error 2321

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