[plugins] Convert to Markdown, normalize section names and URLs

_fc-plugins/eva.md

+---
+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}}).