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.
intS=0;intT[5];intmain(void){int i;int*p=&T[0];for(i=0;i<5;i++){S=S+i;*p++=S;}returnS;}01This command-line creates an analysis project for file first.c.frama-c-gui-slevel103-val2first.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++;}returnS;}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++;}returnS;}*tmp = S;modifiesT[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;
intmain(void){inti;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++;}returnS;}
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 ++;
intmain(void){inti;int*p;01This analysis highlights all the statements impacted by the selected statement.p = T;1i=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++;}returnS;}