Eva, an Evolved Value Analysis

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 of possible values for each variable, in each point of the analyzed program.

Quick Start

The plug-in can be used both with the graphical user interface and in batch mode (recommended). In batch mode, the command line may look like:

frama-c -eva 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 case, 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 ‑eva.

First Example

Consider the following function, in file test.c:

int abs(int x) {
  if (x < 0) return -x;
  else return x;
}

In 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 protects against an 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 -eva test.c -main abs
[…]
mytests/test.c:2:[eva] warning: signed overflow. assert -x ≤ 2147483647;
[eva] done for function abs
[eva] ====== VALUES COMPUTED ======
[eva: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

Maturity: industrialized.
Recursive calls are currently not supported.
Only sequential code can be analyzed at this time.