Showing error 1500

User: Jiri Slaby
Error type: Reachable Error Location
Error type description: A specified error location is reachable in some program path
File location: loops/n.c40_safe.i
Line in file: 18
Project: SV-COMP 2013
Project version: 2.6.28
Tools: Manual Work
Entered: 2013-01-17 16:57:54 UTC

Source: 

 1int __VERIFIER_nondet_int();
 2
 3  char x[100], y[100];
 4  int i,j,k;
 5
 6void main() {
 7  k = __VERIFIER_nondet_int();
 8
 9  i = 0;
10  while(x[i] != 0){
11    y[i] = x[i];
12    i++;
13  }
14  y[i] = 0;
15
16  if(k >= 0 && k < i)
17    if(y[k] == 0)
18      {ERROR: goto ERROR;}
19}
↑