Showing error 1494

User: Jiri Slaby
Error type: Reachable Error Location
Error type description: A specified error location is reachable in some program path
File location: loops/ludcmp_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}
 7double a[50][50], b[50], x[50];
 8int ludcmp(int nmax, int n, double eps);
 9static double fabs(double n)
10{
11  double f;
12  if (n >= 0) f = n;
13  else f = -n;
14  return f;
15}
16void main()
17{
18 int i, j, nmax = 50, n = 5, chkerr;
19 double eps, w;
20 eps = 1.0e-6;
21 for(i = 0; i <= n; i++)
22 {
23   w = 0.0;
24   for(j = 0; j <= n; j++)
25   {
26     a[i][j] = (i + 1) + (j + 1);
27     if(i == j) a[i][j] *= 10.0;
28     w += a[i][j];
29   }
30                        __VERIFIER_assert(i==2);
31   b[i] = w;
32 }
33 chkerr = ludcmp(nmax, n, eps);
34}
35int ludcmp(int nmax, int n, double eps)
36{
37 int i, j, k;
38 double w, y[100];
39 if(n > 99 || eps <= 0.0) return(999);
40 for(i = 0; i < n; i++)
41 {
42   if(fabs(a[i][i]) <= eps) return(1);
43   for(j = i+1; j <= n; j++)
44   {
45     w = a[j][i];
46     if(i != 0)
47       for(k = 0; k < i; k++)
48         w -= a[j][k] * a[k][i];
49     a[j][i] = w / a[i][i];
50   }
51   for(j = i+1; j <= n; j++)
52     {
53       w = a[i+1][j];
54       for(k = 0; k <= i; k++)
55         w -= a[i+1][k] * a[k][j];
56       a[i+1][j] = w;
57     }
58 }
59 y[0] = b[0];
60 for(i = 1; i <= n; i++)
61   {
62     w = b[i];
63     for(j = 0; j < i; j++)
64       w -= a[i][j] * y[j];
65     y[i] = w;
66   }
67 x[n] = y[n] / a[n][n];
68 for(i = n-1; i >= 0; i--)
69   {
70     w = y[i];
71     for(j = i+1; j <= n; j++)
72       w -= a[i][j] * x[j];
73     x[i] = w / a[i][i] ;
74   }
75 return(0);
76}