Merge branch 'fix/eva' into 'master'

Fixes plugin pages of Eva, Mthread and Studia

See merge request frama-c/frama-c.frama-c.com!8

_fc-plugins/eva.html

 ---
 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>
+</dl>
\ No newline at end of file

_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>
+</dl>
\ No newline at end of file

_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>
+</dl>
\ No newline at end of file