---
layout: plugin
title: Eva, an Evolved Value Analysis
description: Automatically computes variation domains for the variables of the program.
key: main
distrib_mode: main
manual_pdf: /download/frama-c-value-analysis.pdf
---

## 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.

<img src="/assets/img/plugins/eva-img.png">

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`:

```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](/html/acsl.html) 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]({{page.manual_pdf}}).