Showing error 1495

User: Jiri Slaby
Error type: Reachable Error Location
Error type description: A specified error location is reachable in some program path
File location: loops/matrix_safe.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}
 7int __VERIFIER_nondet_int();
 8
 9main()
10{
11  unsigned int N_LIN=1;
12  unsigned int N_COL=1;
13  unsigned int j,k;
14  int matriz[N_COL][N_LIN], maior;
15
16  maior = __VERIFIER_nondet_int();
17  for(j=0;j<N_COL;j++)
18    for(k=0;k<N_LIN;k++)
19    {
20       matriz[j][k] = __VERIFIER_nondet_int();
21
22       if(matriz[j][k]>=maior)
23          maior = matriz[j][k];
24    }
25
26  __VERIFIER_assert(matriz[0][0]<=maior);
27}
↑