Securing the future of your critical activities
The Frama-C source code analysis platform provides tools to make your code safer and more
secure.
Download Frama-C
Get Started
Trying out Frama-C analyzing
a simple C program
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;
}