Trying out Frama-C: analyzing a simple C program

  1. 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;
     }
    
  2. Invoking Frama-C:
    frama-c-gui -slevel 10 -val first.c
  3. Browsing the analysis results with Frama-C: