diff --git a/_fc-plugins/eva.html b/_fc-plugins/eva.html
index 89e64084ad866baf8ea61045b965822858e45520..fb224c3e704e02691a981939ddec953758c1966b 100755
--- a/_fc-plugins/eva.html
+++ b/_fc-plugins/eva.html
@@ -1,6 +1,6 @@
---
layout: plugin
-title: Evolved Value Analysis (EVA)
+title: Eva, an Evolved Value Analysis
description: Automatically computes variation domains for the variables of the program.
key: main
swipper: yes
@@ -18,9 +18,10 @@ swipper: yes
although the user may guide the analysis in places. It handles a wide spectrum of C constructs. This plug-in uses
abstract interpretation techniques.</p>
- <p>The results of <b>EVA</b> can be exploited directly in two ways.</p>
<img src="/assets/img/plugins/eva-img.png">
+ <p>The results of <b>Eva</b> can be exploited directly in two ways.</p>
+
<ul>
<li>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
@@ -29,8 +30,6 @@ swipper: yes
<li>The Frama-C graphical user interface displays the inferred sets for possible values of a variable in each
point of the analyzed program.</li>
</ul>
-
- <p>Maturity: industrialized.</p>
</dd>
<dt class="subTitle">Quick Start</dt>
@@ -39,15 +38,15 @@ swipper: yes
<p>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:</p>
<pre>
-frama-c -val file1.c file2.c
+frama-c -eva file1.c file2.c
</pre>
<p>A list of alarms (corresponding to possible run-time errors as computed by the analysis) is produced on the
standard output.</p>
- <p>The results of <b>EVA</b> are used by many other plug-ins. In this cases, the analysis is initiated
+ <p>The results of <b>Eva</b> 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 (<i>e.g.</i>
- through the same command-line options that would be used in conjunction with <tt>-val</tt>).</p>
+ through the same command-line options that would be used in conjunction with <tt>-eva</tt>).</p>
</dd>
<dt class="subTitle">First Example</dt>
@@ -67,12 +66,12 @@ int abs(int x) {
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.</p>
<pre>
-$ frama-c -val test.c -main abs
+$ frama-c -eva 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:
+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]
</pre>
@@ -83,6 +82,8 @@ mytests/test.c:2:[value] warning: signed overflow. assert -x ≤ 2147483647;
<dt class="subTitle">Technical Notes</dt>
<dd>
+ <p>Maturity: industrialized.</p>
+
<p>Recursive calls are currently not supported.</p>
<p>Only sequential code can be analyzed at this time.</p>
@@ -92,10 +93,10 @@ mytests/test.c:2:[value] warning: signed overflow. assert -x ≤ 2147483647;
<dd>
<p>The options to configure the analysis as well as the syntax of the results are described in the <a class="plain"
- href="/download/frama-c-value-analysis.pdf">EVA user manual</a>.</p>
+ href="/download/frama-c-value-analysis.pdf">Eva user manual</a>.</p>
</dd>
<dt class="subTitle"></dt>
<dd></dd>
-</dl>
\ No newline at end of file
+</dl>
diff --git a/_fc-plugins/mthread.html b/_fc-plugins/mthread.html
index 33d2ce9313bb7cf452ddf2d4578e13a9d686500a..04b7189852e8a31b1c9805d4275bd5f0e0ba985d 100755
--- a/_fc-plugins/mthread.html
+++ b/_fc-plugins/mthread.html
@@ -10,8 +10,8 @@ key: concurrent
<dt class="subTitle">Overview</dt>
<dd>
- <p>The <b>Mthread</b> plug-in automatically analyzes concurrent C programs, using the techniques used by the Value
- analysis. At the end of its execution, the concurrent behavior of each thread is over-approximated. Thus, the
+ <p>The <b>Mthread</b> plug-in automatically analyzes concurrent C programs, using the techniques used by Eva.
+ At the end of its execution, the concurrent behavior of each thread is over-approximated. Thus, the
information delivered by the plug-in take into account all the <i>possible concurrent behaviors</i> of the
program.</p>
@@ -36,7 +36,7 @@ key: concurrent
"http://localhost:8000/documentation/mthread/download/frama-c-mthread-graph.svg">this graph</a>.
</li>
- <li>For each program point of each thread, an over approximation of the possible values</li>
+ <li>For each program point of each thread, an over-approximation of the possible values</li>
</ul>
</dd>
@@ -119,6 +119,6 @@ key: concurrent
<dd>
<p>For any questions, remarks or suggestions, please contact <a class="email" href=
- "mailto:boris.yakobowski@cea.fr?subject=[Mthread]">Boris Yakobowski</a>.</p>
+ "mailto:tristan.le-gall@cea.fr?subject=[Mthread]">Tristan Le Gall</a>.</p>
</dd>
-</dl>
\ No newline at end of file
+</dl>
diff --git a/_fc-plugins/studia.html b/_fc-plugins/studia.html
index 903c7f65e78d10cb22b944458e2030bd91ea4772..86563e4186f1d529eb6b22696a4d00d1915062ea 100755
--- a/_fc-plugins/studia.html
+++ b/_fc-plugins/studia.html
@@ -18,7 +18,7 @@ key: browsing
<dt class="subTitle">Quick Start</dt>
<dd>
- <p><code>$ frama-c-gui -val studia.c</code></p>
+ <p><code>$ frama-c-gui -eva studia.c</code></p>
<p>Right-click on an expression in the code and choose the <strong>Studia</strong> context menu to access its
features.</p><img class="size-full wp-image-640" src="/assets/img/plugins/studia-img.png" alt="" width="630" height="189"
@@ -64,4 +64,4 @@ key: browsing
<dd>
<p>Automatically enabled after running EVA and opening the GUI.</p>
</dd>
-</dl>
\ No newline at end of file
+</dl>