Showing error 1490

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

Source: 

 1void __VERIFIER_assert(int cond) {
 2  if (!(cond)) {
 3    ERROR: goto ERROR;
 4  }
 5  return;
 6}
 7unsigned int __VERIFIER_nondet_uint();
 8unsigned int SIZE;
 9int linear_search(int *a, int n, int q) {
10  unsigned int j=0;
11  while (j<n && a[j]!=q) {
12  j++;
13  if (j==20) j=-1;
14  }
15  if (j<SIZE) return 1;
16  else return 0;
17}
18int main() {
19  SIZE=(__VERIFIER_nondet_uint()/2)+1;
20  int a[SIZE];
21  a[SIZE/2]=3;
22  __VERIFIER_assert(linear_search(a,SIZE,3));
23}
↑