Trying out Frama-C: analyzing a simple C program

The code to analyze as file first.c (download):

 int S=0;
 int T[5];
 int main(void)
 {
   int i;
   int *p = &T[0] ;
   for (i=0; i<5; i++)
     { S = S+i; *p++ = S; }
   return S;
 }

Invoking Frama-C:
```
frama-c-gui -slevel 10 -val first.c
```
Browsing the analysis results with Frama-C:

static int x = 1; static long mc1[8][8], mc2[8][8]; /* if (init) { for (;;) } (long m1[8][8], long m2[8][8]) { long i, j, k, tmp1[8][8], tmp2[8][8]; /* Loops indexes and temporary matrices. */ double ftmp1, ftmp2; static int init = 1; static long mc1[8][8], mc2[8][8]; /* hard-coded cosines matrices. */if (init) { for (i = 0; i < 8; i++) for (j = 0; j < 8; j++) { ftmp1 = ((j == 0) ? 0; static long mc1[8][8], mc2[8][8]; /* hard-coded cosines matrices. */if (init) { for (i = 0; i < 8; i++) for (j = 0; j < 8; j++) { ftmp1 = ((j == 0) ? 0.5 / sqrt (2.0) : 0.5) * cos ((2.0 * i + 1.0) * j * TH); ftmp2 = ftmp1; /* The well known formula. The max absolute value for ftmp1 and ftmp2 is 0.5. */ ftmp1 *= (1 << NBC1); if (ftmp1 < 0) ftmp1 -= 0.5; else ftmp1 += 0.5; mc1[i][j] = ftmp1; ftmp2 *= (1 << NBC2); /* Multiply the cosine coefficient by 2^NBC2. The max absolute value for * ftmp2 is 2^(NBC2-1). */ if (ftmp2 < 0) ftmp2 –= 0.5; else ftmp2 += 0.5; /* For symetrical rounding. */ mc2[i][j] = ftmp2; } init = 0; } /* Then the first pass. */ for(i = 0; i < 8; i++) for(j = 0; j < 8; j++) { for(k = 0, tmp1[i][j] = 0; k < 8; k++)tmp1[i][j] += mc1[i][k] * m1[k][j]; /* The [i,j] coefficient of the matrix product MC1*M1. */ tmp1[i][j] >>= (NBC1 + 10 – NBI); tmp1[i][j] += 1; /* For rounding purpose. */ tmp1[i][j] >>= 1; /* Final rounding. tmp1[i][j] is now represented on NBI bits. */if (tmp1[i][j] < -(1 <<