Download Frama-C
Get Started

Trying out Frama-C analyzing
a simple C program

Browsing the analysis results with Frama-C

Interface Overview
Value Analysis
Effects Analysis
Dependency Analysis
Impact Analysis
01This command-line creates an analysis project for file first.c.
02Option -val runs the Evolved Value Analysis plug-in and prepares its results.
03Option -slevel 10 is one of several options that influence the precision of the value analysis.
 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;
 }


  01This command-line creates an analysis project for file first.c.frama-c-gui -slevel 103 -val2 first.c102Option -val runs the Evolved Value Analysis plug-in and prepares its results.

01The Evolved Value Analysis (EVA) plug-in computes sets of possible values for every variable at each point of the program.
02When the execution reaches the highlighted point inside the loop, the variable S always contains either 0, 1, 3, or 6. Frama-C guarantees that it does not take any other values at that point.
  i = 0;
  while (i < 5) {
    {
      int *tmp;
      01The Evolved Value Analysis (EVA) plug-in computes sets of possible values for every variable at each point of the program.S1 += i;
    { /* sequence */
         tmp = p;
         p ++;
         *tmp = S;
       }
    }
    i++;
  }
  return S;
 }

 S  {0; 1; 3; 6}202When the execution reaches the highlighted point inside the loop, the variable S always contains either 0, 1, 3, or 6. Frama-C guarantees that it does not take any other values at that point.
 S (after)  {0; 1; 3; 6; 10}
01For each statement, Frama-C can provide an exhaustive list of the memory cells that may be modified by this statement during the execution, even if the statement uses pointers.
02Frama-C guarantees that anytime it is executed, the statement *tmp = S; does not change any memory location other than the cells of the array T.
  p = T;
  i = 0;
  while (i < 5) {
    {
      int *tmp;
      S += i;
       { /* sequence */
         tmp = p;
         p ++;
         01For each statement, Frama-C can provide an exhaustive list of the memory cells that may be modified by this statement during the execution, even if the statement uses pointers.*tmp = S;1
       }
    }
    i++;
  }
  return S;
 }
 
 *tmp = S; modifies T[0..4]02Frama-C guarantees that anytime it is executed, the statement *tmp = S; does not change any memory location other than the cells of the array T.2
01The dependencies plug-in highlights the statements that define the value of variable S at this point.
02The value contained in variable S at the statement *tmp = S; was defined by the statement S += i;
int main(void)
{
  int i;
  int *p;
  p = T;
  i = 0;
  while (i < 5) {
    {
      int *tmp;
      S += i;202The value contained in variable S at the statement *tmp = S; was defined by the statement S += i;
       { /* sequence */
         tmp = p;
         p ++;
         01The dependencies plug-in highlights the statements that define the value of variable S at this point.*tmp = S1;
       }
    }
    i++;
  }
  return S;
}
01This analysis highlights all the statements impacted by the selected statement.
02This statement has repercussions on the statements tmp = p; p++; *tmp = S;. It is guaranteed not to affect the statements S += i; and i ++;
int main(void)
{
  int i;
  int *p;
  01This analysis highlights all the statements impacted by the selected statement.p = T;1
  i = 0;
  while (i < 5) {
    {
      int *tmp;
      S += i;
       { /* sequence */
         tmp = p;
         p++;
         *tmp = S;202This statement has repercussions on the statements tmp = p; p++; *tmp = S;. It is guaranteed not to affect the statements S += i; and i ++;
       }
    }
    i++;
  }
  return S;
}

Frama-C Calendar

A new day in Frama-C

Read More

A new day in Frama-C

Read More

Get Frama-C

Frama-C is only available for Desktop

Discover more about Frama-C Download Frama-C
SECURE
SECURE