Showing error 1527

User: Jiri Slaby
Error type: Reachable Error Location
Error type description: A specified error location is reachable in some program path
File location: loops/toy_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 unsigned int __VERIFIER_nondet_uint();
  2extern int __VERIFIER_nondet_int();
  3void error(void)
  4{
  5  {
  6  goto ERROR;
  7  ERROR: ;
  8  return;
  9}
 10}
 11int c ;
 12int c_t ;
 13int c_req_up ;
 14int p_in ;
 15int p_out ;
 16int wl_st ;
 17int c1_st ;
Show full sources
↑