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.

Further Reading

The options to configure the analysis as well as the syntax of the results are described in the Eva user manual.