Evolved Value Analysis (EVA)

- Value analysis based on abstract interpretation
-
The Evolved Value Analysis plug-in computes variation domains for variables. It is quite automatic, although the user may guide the analysis in places. It handles a wide spectrum of C constructs. This plug-in uses abstract interpretation techniques.
The results of EVA can be exploited directly in two ways.
- They can be used to infer the absence of run-time errors. The results are displayed in reverse, that is, alarms are emitted for all the operations that could lead to a run-time error. If an alarm is not emitted for an operation in the source code, then this operation is guaranteed not to cause a run-time error.
- The Frama-C graphical user interface displays the inferred sets for possible values of a variable in each point of the analyzed program.
Maturity: industrialized.
- Quick Start
-
The plug-in can be used both with the graphical user interface and in batch mode. In batch mode, the command line may look like:
frama-c -val file1.c file2.c
A list of alarms (corresponding to possible run-time errors as computed by the analysis) is produced on the standard output.
The results of EVA are used by many other plug-ins. In this cases, the analysis is initiated automatically by the exploiting plug-in, but it is still possible to configure it for the case at hand (e.g. through the same command-line options that would be used in conjunction with -val).
- First Example
-
Consider the following function, in file test.c:
int abs(int x) { if (x < 0) return -x; else return x; }
On this code, Eva reports the possible integer overflow when x is the smallest negative integer by emitting an alarm at line 2. The alarm is the ACSL assertion assert -x ≤ 2147483647; that guards against the overflow.
Eva also displays the possible values of the variables at the end of the function. Here, we can see that the result is always positive.$ frama-c -val test.c -main abs […] mytests/test.c:2:[value] warning: signed overflow. assert -x ≤ 2147483647; [value] done for function abs [value] ====== VALUES COMPUTED ====== [value:final-states] Values at end of function abs: __retres ∈ [0..2147483647]
One can also inspect in the graphical interface of Frama-C the alarms emitted by Eva, as well as the possible values inferred at each program point.
- Technical Notes
-
Recursive calls are currently not supported.
Only sequential code can be analyzed at this time.
- Further Readings
-
The options to configure the analysis as well as the syntax of the results are described in the EVA user manual.