Merge branch 'plugins-to-markdown' into 'master'

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

See merge request !30

_fc-plugins/aorai.html

----
-layout: plugin
-title: Aoraï
-description: Verify specifications expressed as LTL (Linear Temporal Logic) formulas.
-key: specifications
-distrib_mode: main
----
-
-<dl class="defnitionList">
-  <dt class="subTitle">Overview</dt>
-
-  <dd>
-	<p>The <b>Aoraï</b> plug-in provides a method to automatically annotate a C program according to an LTL formula <i>F</i> such that, if the annotations are verified, then we ensure that the program respects <i>F</i>.</p>
-	<p>The classical method to validate annotations is to use
-   the <a href="wp.html">Wp</a> or <a href="eva.html">Eva</a> plug-ins.</p>
-  </dd>
-
-  <dt class="subTitle">Installation Dependencies</dt>
-
-  <dd>
-	<p>Aoraï is now available in the main Frama-C distribution. It used to be available from <a class="extlink" href="http://amazones.gforge.inria.fr/aorai/">http://amazones.gforge.inria.fr/aorai/</a>, but the version currently hosted there is obsolete and won't compile with newer versions of Frama-C. In order to install or update this plug-in, you need to have the Frama-C <a href="http://frama-c.com/">framework</a>.</p> 
-	<p>If you want to use LTL syntax for properties, then you have to install the ltl2ba tool in your current path. This tool is distributed under the GPL licence and converts a LTL formula into a Büchi automaton. You can find this tool on the homepage of its author <a class="extlink" href="http://www.lsv.ens-cachan.fr/~gastin/ltl2ba/index.php">Paul Gastin</a> (ENS Cachan).</p>
-  </dd>
-
-  <dt class="subTitle">Usage</dt>
-
-  <dd>
-	<p>The plug-in is activated with one of the following command lines:</p>
-<pre>frama-c file.c -aorai-ltl file.ltl
-</pre>
-<pre>frama-c file.c -aorai-automata file.ya
-</pre>
-	These two commands differ only by the syntax used to express the
-	property to be verified: <i>.ltl</i> files are described in a ltl
-	like syntax, while <i>.ya</i> are description of automata in a
-	yacc-like syntax.
-	<p>Options are:</p>
-	<dl>
-	<dt><tt>-aorai-verbose</tt></dt>
-	<dd>Gives some information during computation, such as
-	used/produced files and heuristics applied</dd>
-	<dt><tt>-aorai-show-op-spec</tt></dt>
-	<dd>Displays, at the end of the process, the computed specification
-	of each operation, in terms of Büchi states and transitions.</dd>
-	<dt><tt>-aorai-dot</tt></dt>
-	<dd>Generates a dot file of the Büchi automaton. Dot is a graph
-	format used by the <a class="extlink" href="http://www.graphviz.org">GraphViz tool</a>.</dd>
-	<dt><tt>-aorai-acceptance</tt></dt>
-	<dd>if set, considers acceptation states (Only on finite traces).
-	If not, only the safety is verified.</dd>
-	<dt><tt>-aorai-output-c-file</tt> <i>file</i></dt>
-	<dd>Outputs the annotated program in <i>file</i> (defaults is to
-	derive a name from the one of the first input file)</dd>
-	<dt><tt>-aorai-help</tt></dt>
-	<dd>Gives the whole list of options</dd>
-	</dl>
-  </dd>
-
-  <dt class="subTitle">Ressources</dt>
-
-  <dd>
-	<ul class="none">
-	<li><a class="pdf" href="/download/frama-c-aorai-manual.pdf">Short
-	Documentation</a></li>
-	<li><a class="src" href="/download/frama-c-aorai-example.tgz">Couple
-	of simple examples</a></li>
-	</ul>
-	<p>Other ressources can be found at <a class="extlink" href="http://amazones.gforge.inria.fr/aorai/">the official web page of
-	Aoraï.</a></p>
-  </dd>
-
-  <dt class="subTitle">Installation Dependencies</dt>
-
-  <dd>
-	<ul>
-	<li>Only the safety part of properties is checked. The liveness part is not truly considered. Currently, a liveness property is	only a restriction to the terminating state of the program that	have to be an acceptation state. Hence, if the program terminates, then the liveness property is verified.</li>
-	<li>Currently, function pointers are not supported.</li>
-	<li>In the init state from the automaton, conditions on C-array or C-structure are not statically evaluated (it's an optimization) but are supported.</li>
-	</ul>
-  </dd>
-  
-  <dt class="subTitle">Contact</dt>
-
-  <dd>
-	<p>Aoraï has been originally written by Nicolas Stouls (  <a class="email" href="mailto:nicolas.stouls@insa-lyon.fr?subject=%5BPlug-in%20Aorai%5D">Nicolas Stouls</a>, <a class="extlink" href="http://www.citi-lab.fr/">CITI Labs</a>, <a class="extlink" href="http://amazones.gforge.inria.fr/">AMAZONES team</a>). It is currently maintained by CEA LIST as part of the main Frama-C distribution. See our <a href="contact.html">contact</a> page for more information.</p>
-	<p><span class="title">End Note:</span> to the question "<i>Why this name: Aoraï ?</i>" my answer is: why not ? Aoraï is the name of the tallest reachable mount in the Tahiti island and its reachability is not always obvious.</p>
-  </dd>
-</dl>

_fc-plugins/aorai.md

+---
+layout: plugin
+title: Aoraï
+description: Verify specifications expressed as LTL (Linear Temporal Logic) formulas.
+key: specifications
+distrib_mode: main
+manual_pdf: /download/frama-c-aorai-manual.pdf
+---
+
+## Overview
+
+The **Aoraï** plug-in provides a method to automatically annotate a C program
+according to an LTL formula *F* such that, if the annotations are verified,
+then we ensure that the program respects *F*.
+The classical method to validate annotations is to use the [Wp](wp.html) or
+[Eva](eva.html) plug-ins.
+
+## Installation Dependencies
+
+Aoraï is available in the main Frama-C distribution. It used to be
+available from http://amazones.gforge.inria.fr/aorai, but the version
+currently hosted there is obsolete and won't compile with newer versions of
+Frama-C.
+
+If you want to use LTL syntax for properties, you have to install the
+[ltl2ba](http://www.lsv.ens-cachan.fr/~gastin/ltl2ba/index.php) tool in your
+path. This tool is distributed by its author, Paul Gastin (ENS Cachan),
+under the GPL licence and converts an LTL formula into a Büchi automaton.
+
+## Usage
+
+The plug-in is activated with one of the following command lines:
+
+    frama-c file.c -aorai-ltl file.ltl
+
+    frama-c file.c -aorai-automata file.ya
+
+These two commands differ only by the syntax used to express the
+property to be verified: *.ltl* files are described in an ltl-like syntax,
+while *.ya* are description of automata in an yacc-like syntax.
+Options are:
+
+- `-aorai-verbose`:
+  Gives some information during computation, such as used/produced files
+  and heuristics applied.
+
+- `-aorai-show-op-spec`:
+  Displays, at the end of the process, the computed specification
+  of each operation, in terms of Büchi states and transitions.
+
+- `-aorai-dot`:
+  Generates a dot file of the Büchi automaton. Dot is a graph
+  format used by the [GraphViz](http://www.graphviz.org) tool.
+
+- `-aorai-acceptance`:
+  If set, considers acceptation states (Only on finite traces).
+  If not, only the safety is verified.
+
+- `-aorai-output-c-file`: *file*
+  Outputs the annotated program in *file* (the default is to
+  derive a name from the one of the first input file).
+
+- `-aorai-help`:
+  Gives the whole list of options.
+
+## Installation Dependencies
+
+- Only the safety part of properties is checked. The liveness part is not truly
+  considered. Currently, a liveness property is only a restriction that the
+  terminating state of the program has to be an accepting state.
+  Hence, if the program terminates, then the liveness property is verified.
+- Currently, function pointers are not supported.
+- In the init state from the automaton, conditions on C arrays and C structures
+  are not statically evaluated (which would be an optimization)
+  but are supported.
+
+## Contact
+
+Aoraï has been originally written by
+[Nicolas Stouls]( mailto:nicolas.stouls@insa-lyon.fr?subject=[Plug-in Aorai]),
+[CITI Labs](http://www.citi-lab.fr), [AMAZONES team](http://amazones.gforge.inria.fr).
+It is currently maintained by CEA LIST as part of the main Frama-C distribution.
+See our [contact](contact.html) page for more information.
+
+**End Note:** to the question "*Why this name: Aoraï?*" my answer is: why not?
+Aoraï is the name of the tallest reachable mount in the Tahiti island and its
+reachability is not always obvious.
+
+## Further Reading
+
+- [Short Documentation]({{page.manual_pdf}})
+- [A few simple examples](/download/frama-c-aorai-example.tgz)
+
+Other resources can be found at
+[the official web page of Aoraï](http://amazones.gforge.inria.fr/aorai/).

_fc-plugins/cafe.html

----
-layout: plugin
-title: CaFE
-description: Verification of CaRet temporal logic properties
-key: specifications
-distrib_mode: free
----
-
-<dl class="defnitionList">
-  <dt class="subTitle">Overview</dt>
-  <dd><p>CaFE (CaRet Frama-C Extension) is a small model-checker dedicated
-      to prove CaRet properties over C programs.
-      <a href="https://doi.org/10.1007/978-3-540-24730-2_35">CaRet</a> is
-      "a temporal logic of nested calls and returns", i.e. a flavor of
-      temporal logic well suited to describe a program's call stack.
-    </p>
-  </dd>
-  <dt class="subTitle">Use</dt>
-  <dd>
-    <p><a href="https://github.com/Stevendeo/CaFE">CaFE</a> is available as a
-      separate open-source plug-in. Once installed, it will be activated by
-      the <tt>-cafe</tt> option, while <tt>-cafe-formula</tt> allows specifying
-      the file in which to formula to be verified lies. A typical command will
-      thus be the following:
-      <pre>frama-c -cafe file.c -cafe-formula file.caret</pre>
-    </p>
-    <p>Note that CaFE uses <a href="eva.html">Eva</a> internally to compute
-      an over-approximation of the states of the program.
-    </p>
-  </dd>
-</dl>

_fc-plugins/cafe.md

+---
+layout: plugin
+title: CaFE
+description: Verification of CaRet temporal logic properties
+key: specifications
+distrib_mode: free
+repo_url: https://github.com/Stevendeo/CaFE
+---
+
+## Overview
+
+CaFE (CaRet Frama-C Extension) is a small model-checker dedicated
+to prove CaRet properties over C programs.
+[CaRet](https://doi.org/10.1007/978-3-540-24730-2_35) is
+"a temporal logic of nested calls and returns", i.e. a flavor of
+temporal logic well suited to describe a program's call stack.
+
+## Usage
+
+[CaFE]({{page.repo_url}}) is available as a
+separate open-source plug-in. Once installed, it will be activated by
+the `-cafe` option, while `-cafe-formula` allows specifying
+the file in which to formula to be verified lies. A typical command will
+thus be the following:
+
+    frama-c -cafe file.c -cafe-formula file.caret
+
+## Dependencies
+
+CaFE uses [Eva](eva.html) internally to compute an over-approximation
+of the states of the program.

_fc-plugins/conc2seq.html

----
-layout: plugin
-title: Conc2seq
-description: Verification of concurrent programs
-key: concurrent
-distrib_mode: proto
----
-
-<dl class="defnitionList">
-  <dt class="subTitle">Overview</dt>
-  <dd><p>Conc2seq is dedicated to the verification of concurrent C
-      programs. More specifically, it proposes an instrumentation of the
-      original code that simulates all possible interleavings allowed by
-      the norm. The resulting instrumented code is then a sequential
-      programs that can be analyzed as such. Note however that the
-      transformation assumes that the original code is sequentially consistent,
-      which must be verified independently (e.g. by using the
-      <a href="mthread.html">Mthread plugin</a>).
-    </p>
-  </dd>
-  <dt class="subTitle">Use</dt>
-  <dd>
-    As the plugin is in an early stage of development, it is currently only
-    available upon request.
-  </dd>
-</dl>

_fc-plugins/conc2seq.md

+---
+layout: plugin
+title: Conc2seq
+description: Verification of concurrent programs
+key: concurrent
+distrib_mode: free
+repo_url: https://github.com/AllanBlanchard/Frama-C-Conc2Seq
+---
+
+## Overview
+
+Conc2seq is dedicated to the verification of concurrent C programs.
+More specifically, it proposes an instrumentation of the original code
+that simulates all possible interleavings allowed by the C standard.
+The resulting instrumented code is then a sequential program that can be
+analyzed as such. Note however that the transformation assumes that the
+original code is sequentially consistent, which must be verified independently
+(e.g. by using the [Mthread plugin](mthread.html)).
+
+## Usage
+
+Conc2Seq is available as an external open-source [plug-in]({{page.repo_url}}).
+
+Once installed, it is enabled with the `-c2s` option, which will generate a
+sequential version of the concurrent API implementation provided to Frama-C.
+The generated code and specification is available a new project.
+To output this simulating program into a file, use the option
+`-c2s-output filename`.

_fc-plugins/e-acsl.html

----
-layout: plugin
-title: E-ACSL
-description: Runtime Verification Tool
-key: main
-download: http://frama-c.com/download/e-acsl/e-acsl-manual-19.0-Potassium.pdf
-distrib_mode: main
----
-
-<dl class="defnitionList">
-  <dt class="subTitle">Overview</dt>
-
-  <dd>
-	<p>Frama-C's <strong>E-ACSL</strong> plug-in automatically
-	translates an annotated C program into another program that
-	detects the violated annotations at runtime. If no annotation
-	is violated, the behavior of the new program is the same as
-	the one of the original program.</p>
-
-	<p>Combined with other Frama-C plug-ins that generate
-	annotations, the verification process is pretty automatic and
-	may verify much more properties than standard testing. This
-	way, it is a <a class="plain" href=
-	"https://en.wikipedia.org/wiki/Memory_debugger">memory
-	debugger</a> offering functionalities comparable to Valgrind
-	or AddressSanitizer, and even more powerful.</p>
-
-        <p>More precisely, possible usages include
-          <ol>
-            <li>detection of a large class of undefined behavior (in conjunction
-              with the <a href="rte.html">RTE</a> plug-in);
-            </li>
-            <li>verification of high-level properties (in conjunction for
-              instance with the <a href="aorai.html">Aoraï</a> or
-              <a href="secureflow.html">SecureFlow</a> plug-ins);
-            </li>
-            <li>complementing static and dynamic analyses (i.e. trying to
-              find test cases that triggers alarms generated by
-              <a href="eva.html">Eva</a> or act
-              as counter-example for annotations marked as unknown by
-              <a href="wp.html">WP</a>),
-               in conjunction with
-              the <a href="stady.html">StaDy</a> plug-in;
-            </li>
-            <li>debugging specification, in conjunction with a test-case
-              generator such as <a href="pathcrawler.html">PathCrawler</a>
-              or <a href="http://lcamtuf.coredump.cx/afl/">AFL</a>
-            </li>
-          </ol>
-        </p>
-  </dd>
-
-  <dt class="subTitle">Quick Start</dt>
-
-  <dd>
-	<p>E-ACSL comes with a convenient script <em>e-acsl-gcc.sh</em> which may be called as follow:</p>
-	<pre>$ e-acsl-gcc.sh -c &lt;files&gt;</pre>
-
-	<p>It generates three files <em>./a.out</em>, <em>./a.out.frama-c</em> and <em>./a.out.e-acsl</em>. The first one
-	is the binary produced by <em>gcc</em> from the input files, the second one is the instrumented file with the
-	monitor generated by E-ACSL from the input files. The third one is the binary produced by <em>gcc</em> from this
-	latter file, so monitoring the annotations. Its execution behaves in the same way than the two other files, except
-	that it fails if an annotation is violated.</p>
-
-	<p>In order to automatically check that no <b>undefined behaviors</b> of many kinds are executed, the script can be simply used as
-	follows:</p>
-	<pre>$ e-acsl-gcc.sh -c --rte=all &lt;files&gt;</pre>
-
-	<p>
-</dd>

_fc-plugins/e-acsl.md

+---
+layout: plugin
+title: E-ACSL
+description: Runtime Verification Tool
+key: main
+manual_pdf: http://frama-c.com/download/e-acsl/e-acsl-manual.pdf
+additional:
+  - name: "E-ACSL Language Reference Manual"
+    link: http://frama-c.com/download/e-acsl/e-acsl.pdf
+  - name: "E-ACSL Language Reference Implementation Manual"
+    link: http://frama-c.com/download/e-acsl/e-acsl-implementation.pdf
+distrib_mode: main
+---
+
+## Overview
+
+Frama-C's **E-ACSL** plug-in automatically translates an annotated C program
+into another program that detects the violated annotations at runtime.
+If no annotation is violated, the behavior of the new program is the same as
+the one of the original program.
+
+Combined with other Frama-C plug-ins that generate annotations, the
+verification process is pretty automatic and may verify much more properties
+than standard testing. This way, it is a
+[memory debugger](https://en.wikipedia.org/wiki/Memory_debugger)
+offering functionalities comparable to Valgrind and AddressSanitizer,
+and even more powerful.
+
+More precisely, possible usages include:
+
+- detection of a large class of undefined behaviors (in conjunction
+  with the [RTE](rte.html) plug-in);
+- verification of high-level properties (in conjunction for
+  instance with the [Aoraï](aorai.html) or [SecureFlow](secureflow.html)
+  plug-ins);
+- complementing static and dynamic analyses (i.e. trying to
+  find test cases that trigger alarms generated by [Eva](eva.html) or act
+  as counter-examples for annotations marked as unknown by [WP](wp.html)),
+  in conjunction with the [StaDy](stady.html) plug-in;
+- debugging specifications, in conjunction with a test-case generator such as
+  [PathCrawler](pathcrawler.html) or [AFL](http://lcamtuf.coredump.cx/afl)
+
+## Quick Start
+
+E-ACSL comes with a convenient script *e-acsl-gcc.sh* which may be called
+as follows:
+
+    e-acsl-gcc.sh -c <files>
+
+It generates three files, `./a.out`, `./a.out.frama-c` and `./a.out.e-acsl`.
+The first one is the binary produced by `gcc` from the input files;
+the second one is the instrumented file with the monitor generated by E-ACSL
+from the input files. The third one is the binary produced by `gcc` from this
+latter file, so monitoring the annotations.
+Its execution behaves in the same way as the two other files, except that it
+fails if an annotation is violated.
+
+In order to automatically check that no **undefined behaviors** of many kinds
+are executed, the script can be simply used as follows:
+
+    e-acsl-gcc.sh -c --rte=all <files>
+
+## Dependencies
+
+The **E-ACSL** plug-in can use the results of both [RTE](rte.html) and
+[Eva](eva.html) plug-ins. It can be combined with several other plug-ins,
+such as [WP](wp.html), [Aoraï](aorai.html), [SecureFlow](secureflow.html),
+[StaDy](stady.html), [PathCrawler](pathcrawler.html), etc.
+
+## Further Reading
+
+- [E-ACSL User Manual]({{page.manual_pdf}})
+{% for add in page.additional %}
+- [{{add.name}}]({{add.link}}){% endfor %}

_fc-plugins/eva.html

----
-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
----
-
-<figure class="pluginDetailThumb">
-  <img src="/assets/img/plugins/eva.png" alt="">
-</figure>
-
-<dl class="defnitionList">
-  <dt class="subTitle">Value analysis based on abstract interpretation</dt>
-
-  <dd>
-	<p>The <b>Evolved Value Analysis</b> 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.</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
-	  operation in the source code, then this operation is guaranteed not to cause a run-time error.</li>
-
-	  <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>
-  </dd>
-
-  <dt class="subTitle">Quick Start</dt>
-
-  <dd>
-	<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 -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
-	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>-eva</tt>).</p>
-  </dd>
-
-  <dt class="subTitle">First Example</dt>
-
-  <dd>
-	<p>Consider the following function, in file <em>test.c</em>:</p>
-	<pre>
-int abs(int x) {
-  if (x &lt; 0) return -x;
-  else return x;
-}
-</pre>
-
-	<p>On this code, Eva reports the possible integer overflow when <tt>x</tt> is the smallest negative integer by
-	emitting an alarm at line 2. The alarm is the ACSL assertion <tt>assert -x ≤ 2147483647;</tt> that guards against
-	the overflow.<br>
-	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 -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]
-</pre>
-
-	<p>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.</p>
-  </dd>
-
-  <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>
-  </dd>
-
-  <dt class="subTitle">Further Readings</dt>
-
-  <dd>
-	<p>The options to configure the analysis as well as the syntax of the results are described in the <a class="plain"
-	href="{{page.manual_pdf}}">Eva user manual</a>.</p>
-  </dd>
-
-  <dt class="subTitle"></dt>
-
-  <dd></dd>
-</dl>

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

_fc-plugins/frama-clang.html

----
-layout: plugin
-title: Frama-Clang
-description: C++ front-end to Frama-C, based on the clang compiler.
-key: front
-distrib_mode: free
----
-
-<figure class="pluginDetailThumb">
-  <img src="/assets/img/plugins/frama-clang.png" alt="">
-</figure>
-
-<dl class="defnitionList">
-  <dt class="subTitle">Overview</dt>
-
-  <dd>
-	<p>Frama-Clang is a plugin that allows Frama-C to take as input C++ programs. As its name implies, it is based on the <a href="http://clang.llvm.org">clang</a> compiler, the C/C++/Objective-C front-end of the <a href="http://llvm.org">llvm</a> platform. More precisely Frama-Clang is composed of two parts: a clang plugin (written in C++) that produces a simplified version of the clang AST, and a normal Frama-C plugin that takes as input this simplified version an produces a normal Frama-C AST.</p> 
-	<p>When this plug-in is in use, Frama-C will consider all files ending in <tt>.cpp</tt>, <tt>.c++</tt>, <tt>.C</tt>, <tt>.cxx</tt>, <tt>.cc</tt> and <tt>.ii</tt> (considered as already pre-processed) as C++ files and give them to Frama-Clang to translate them into Frama-C's internal representation (i.e. a plain C AST). Once this has been done, any existing analysis can be launched as usual.</p>
-	<p><b>Caveat:</b> Frama-Clang is currently in an early stage of development. It is known to be incomplete and comes without any bug-freeness guarantee. Moreover, the translation from C++ to C does not make any attempt to optimize the resulting code for the back-end analyzers such as <a href="/fc-plugins/eva.html">Value Analysis</a> or <a href="/fc-plugins/wp.html">WP</a>. Further work is thus needed before Frama-Clang can claim to be a grown-up plug-in. Feel free to <a href="mailto:support@frama-c.com">contact us</a> if you're interested in participating to its maturation.</p>
-  </dd>
-
-  <dt class="subTitle">Installation</dt>
-
-  <dd>
-	<h3>Download</h3>
-	<p>Current version is 0.0.7. The frama-clang plugin can be downloaded
-          <a href="/download/frama-clang-0.0.7.tar.gz">here</a></p>
-	<h3>Requirements</h3>
-	<ul>
-	<li>Frama-C 19.x</li>
-	<li>OCaml 4.02.3 or higher, the same version as the one used to
-	compile Frama-C itself</li>
-	<li>camlp4 (a version compatible with the OCaml version you're
-	using)</li>
-	<li>clang and libclang version 6, 7 or 8.
-          You also need llvm-config (llvm-config-x.y for Debian and
-	  Ubuntu users, as explained in
-          <a href="https://bugs.launchpad.net/ubuntu/+source/llvm-3.1/+bug/991493">
-            this bug report</a>).</li>
-	</ul>
-	<h3>Installation steps</h3>
-	<pre>tar xzvf frama-clang-0.0.7.tar.gz
-cd frama-clang-0.0.7
-./configure
-make
-make install
-	</pre>
-	Depending on your Frama-C installation, this last step might
-	require root permissions
-	<h3>Changes</h3>
-        <h4>v0.0.7</h4>
-        <ul>
-          <li>Compatibility with Frama-C 19.x Potassium</li>
-          <li>Compatibility with Clang 6.0, 7.0 and 8.0</li>
-          <li>Rewritten ACSL++ parser, providing easier extensibility
-            and maintenance</li>
-          <li>Frama-Clang now has a
-            <a href="/download/frama-clang-manual-0.0.7.pdf">manual</a></li>
-          <li>Improved support of STL</li>
-          <li>Preliminary support for lambdas</li>
-          <li>Improved support of template instantiations</li>
-        </ul>
-	<h4>v0.0.6</h4>
-	<ul>
-	<li>Compatibility with Frama-C 17 Chlorine</li>
-	</ul>
-	<h4>v0.0.5</h4>
-	<ul>
-	<li>Compatibility with Clang/LLVM as packaged by Debian/Ubuntu</li>
-	</ul>
-	<h4>v0.0.4</h4>
-	<ul>
-	<li>Compatibility with Frama-C 16 Sulfur</li>
-	<li>Compatibility with Clang/LLVM 5.0.0</li>
-	<li>Improved translation for <tt>const</tt>-qualified objects</li>
-	<li>Fixes translation of implicit functions for classes with
-	virtual inheritance</li>
-	</ul>
-	<h4>v0.0.3</h4>
-	<ul>
-	<li>Compatibility with Frama-C 15 Phosphorus</li>
-	<li>Improved handling of constructors and destructors for local
-	variables</li>
-	</ul>
-	<h4>v0.0.2</h4>
-	<ul>
-	<li>Compatibility with Frama-C 14 Silicon</li>
-	<li>Adding compatibility with Clang/LLVM 3.9.0 and 4.0.0</li>
-	<li>Various fixes in support of virtual inheritance and
-	templates</li>
-	<li>Better support for parsing GNU STL headers</li>
-	</ul>
-	<h4>v0.0.1</h4>
-	<ul>
-	<li>Initial release</li>
-	</ul>
-	<h3>Previous versions</h3>
-	<ul>
-	<li><a href="/download/frama-clang-0.0.6.tar.gz">0.0.6</a>
-	compatible with Frama-C 17.0</li>
-	<li><a href="/download/frama-clang-0.0.5.tar.gz">0.0.5</a>
-	compatible with Frama-C Sulfur-20171101</li>
-	<li><a href="/download/frama-clang-0.0.4.tar.gz">0.0.5</a>
-	compatible with Frama-C Sulfur-20171101</li>
-	<li><a href="/download/frama-clang-0.0.3.tar.gz">0.0.3</a>
-	compatible with Frama-C Phosphorus-20170501</li>
-	<li><a href="/download/frama-clang-0.0.2.tar.gz">0.0.2</a>
-	compatible with Frama-C Silicon-20161101</li>
-	<li><a href="/download/frama-clang-0.0.1.tar.gz">0.0.1</a>
-	compatible with Frama-C Aluminium-20160502</li>
-  </dd>
-  
-  <dt class="subTitle">Command-line options</dt>
-
-  <dd>
-	<ul>
-	<li><tt>-cxx-demangling-short</tt> The translation to C implies a transformation of C++ global identifiers (with namespaces, templates, and function arguments to account for overloading) into unambiguous valid C symbols. This operation is known as name mangling. A mangled name is good from the machine point of view but not human friendly. With this option, which is the default, Frama-C perform the reverse conversion and displays the corresponding unqualified identifier</li>
-	<li><tt>-cxx-demangling-full</tt> With this option, the demangling displays the fully-qualified identifiers</li>
-	<li><tt>-cxx-keep-mangling</tt> With this option, mangled names are displayed as is. Mainly useful to pretty-print compilable C code.</li>
-	<li><tt>-cxx-c++-stdlib-path</tt> <i>path</i> specifies where to look for standard C++ library headers (default is the path to Frama-Clang headers, which are very incomplete </li>
-	<li><tt>-cxx-nostdinc</tt> Do not include Frama-C's C/C++ standard headers in search path, but use directly standard system headers instead. Note that you need to ensure that <tt>-machdep</tt> matches your machine architecture (or pass <tt>-cpp-extra-args</tt> arguments for cross-compilation to the desired architecture)</li>
-	<li><tt>-cxx-clang-command</tt> <i>cmd</i> allows to change the name of the command that launches clang and its Frama-C-specific plug-in. This should not be needed if Frama-Clang has been properly installed.</li>
-	</ul>
-  </dd>
-  
-  <dt class="subTitle">ACSL++</dt>
-
-  <dd>
-	<p>It is possible to annotate C++ code with a language very similar to ACSL. The only distinction is currently that C++ scoping rules apply for global identifiers. Classes can have member logic functions and member predicates. They are never static, and take an implicit <tt>\this</tt> object as receiver argument, similar to the <tt>this</tt> <i>pointer</i> in the code (which is of course accessible in function contracts, assertions and loop annotations). Finally, it is possible to define <tt>class invariant</tt>, similar to ACSL's type invariants for the current class. The following class provides a short example of ACSL++ annotations:</p>
-<pre>class A {
-public:
-  int x;
-  /*@ class invariant pos = \this.x &gt;= 0; */
-
-  /*@ predicate bigger(A a) = x &gt; a.x; */
-
-  /*@ requires \valid(a);
-      // The 'this' pointer is always valid within a method.
-      // No need to add a requires for that
-      requires this-&gt;bigger(*a);
-      assigns this-&gt;x;
-      ensures this-&gt;x == \at(this-&gt;x, Pre) - a-&gt;x;
-   */
-   void f(A* a) { x -= a -&gt; x; }
-};
-</pre>
-  </dd>
-</dl>
-<p style="font-size: .8em"><a name="credit" id="credit"></a> The
-llvm wyvern logo is <a href="http://llvm.org/Logo.html">© Apple,
-inc</a></p>

_fc-plugins/frama-clang.md

+---
+layout: plugin
+title: Frama-Clang
+description: C++ front-end to Frama-C, based on the clang compiler.
+key: front
+distrib_mode: free
+manual_pdf: /download/frama-clang-manual-0.0.7.pdf
+---
+
+![Frama-Clang logo](/assets/img/plugins/frama-clang.png)
+
+## Overview
+
+Frama-Clang is a plugin that allows Frama-C to take as input C++ programs.
+As its name implies, it is based on the [clang](http://clang.llvm.org)
+compiler, the C/C++/Objective-C front-end of the [llvm](http://llvm.org)
+platform. More precisely, Frama-Clang is composed of two parts: a clang plugin
+(written in C++) that produces a simplified version of the clang AST, and a
+normal Frama-C plugin that takes as input this simplified version and produces
+a normal Frama-C AST.
+
+When this plug-in is in use, Frama-C will consider all files ending in `.cpp`,
+`.c++`, `.C`, `.cxx`, `.cc` and `.ii` (considered as already pre-processed)
+as C++ files and give them to Frama-Clang to translate them into Frama-C's
+internal representation (i.e. a plain C AST).
+Once this has been done, any existing analyses can be launched as usual.
+
+**Caveat:** Frama-Clang is currently in an early stage of development.
+It is known to be incomplete and comes without any bug-freeness guarantees.
+Moreover, the translation from C++ to C does not make any attempts to optimize
+the resulting code for the back-end analyzers such as [Eva](eva.html) or
+[WP](wp.html).
+Further work is thus needed before Frama-Clang can claim to be a grown-up
+plug-in. Feel free to [contact us](mailto:support@frama-c.com) if you're
+interested in participating in its maturation.
+
+## Installation
+
+### Download
+
+The current version is 0.0.7. The frama-clang plugin can be downloaded
+[here](/download/frama-clang-0.0.7.tar.gz).
+
+### Requirements
+
+- Frama-C 19.x
+- OCaml 4.02.3 or higher, the same version as the one used to
+compile Frama-C itself
+- camlp4 (a version compatible with the OCaml version you're using)
+- clang and libclang version 6, 7 or 8.
+
+You also need llvm-config (llvm-config-x.y for Debian and Ubuntu users,
+as explained in
+[this bug report](https://bugs.launchpad.net/ubuntu/+source/llvm-3.1/+bug/991493).
+
+### Installation steps
+
+```
+tar xzvf frama-clang-0.0.7.tar.gz
+cd frama-clang-0.0.7
+./configure
+make
+make install
+```
+
+Depending on your Frama-C installation, this last step might
+require root permissions.
+
+### Changes
+
+#### v0.0.7
+
+- Compatibility with Frama-C 19.x Potassium
+- Compatibility with Clang 6.0, 7.0 and 8.0
+- Rewritten ACSL++ parser, providing easier extensibility
+and maintenance
+- Frama-Clang now has a
+[manual]({{page.manual_pdf}})
+- Improved support of STL
+- Preliminary support for lambdas
+- Improved support of template instantiations
+
+#### v0.0.6
+
+- Compatibility with Frama-C 17 Chlorine
+
+#### v0.0.5
+
+- Compatibility with Clang/LLVM as packaged by Debian/Ubuntu
+
+#### v0.0.4
+
+- Compatibility with Frama-C 16 Sulfur
+- Compatibility with Clang/LLVM 5.0.0
+- Improved translation for `const`-qualified objects
+- Fixes translation of implicit functions for classes with
+virtual inheritance
+
+#### v0.0.3
+
+- Compatibility with Frama-C 15 Phosphorus
+- Improved handling of constructors and destructors for local
+variables
+
+#### v0.0.2
+
+- Compatibility with Frama-C 14 Silicon
+- Adding compatibility with Clang/LLVM 3.9.0 and 4.0.0
+- Various fixes in support of virtual inheritance and
+templates
+- Better support for parsing GNU STL headers
+
+#### v0.0.1
+
+- Initial release
+
+### Previous versions
+
+- [0.0.6](/download/frama-clang-0.0.6.tar.gz)
+compatible with Frama-C 17.0
+- [0.0.5](/download/frama-clang-0.0.5.tar.gz)
+compatible with Frama-C Sulfur-20171101
+- [0.0.5](/download/frama-clang-0.0.4.tar.gz)
+compatible with Frama-C Sulfur-20171101
+- [0.0.3](/download/frama-clang-0.0.3.tar.gz)
+compatible with Frama-C Phosphorus-20170501
+- [0.0.2](/download/frama-clang-0.0.2.tar.gz)
+compatible with Frama-C Silicon-20161101
+- [0.0.1](/download/frama-clang-0.0.1.tar.gz)
+compatible with Frama-C Aluminium-20160502
+
+<p style="font-size: .8em"><a name="credit" id="credit"></a> The
+llvm wyvern logo is <a href="http://llvm.org/Logo.html">© Apple,
+inc</a>

_fc-plugins/impact.html

----
-layout: plugin
-title: Impact analysis
-description: Highlights the locations in the source code that are impacted by a modification.
-key: browsing
-distrib_mode: main
----
-
-<dl class="defnitionList">
-  <dt class="subTitle">Overview</dt>
-
-  <dd>
-	<p>The <b>Impact analysis</b> plug-in allows the automatic computation of the set of statements impacted by the
-	side effects of a statement of a C program. Statements not appearing in this set are guaranteed not to be impacted
-	by the selected statement.</p>
-
-	<p>Impact analysis is available through a contextual menu at each statement in the Frama-C graphical user
-	interface. Invoking this analysis on a statement displays the impact of the statement on the rest of the
-	program.</p>
-
-	<p>
-	<img src="/assets/img/plugins/impact-img.png"></p>
-  </dd>
-
-  <dt class="subTitle">Usage</dt>
-
-  <dd>
-	<p>The plug-in can be used both with the graphical user interface and in batch mode. In batch mode, you must put
-	pragmas on the statements you want to analyze:<br>
-	<code>/*@ impact pragma stmt; */</code></p>
-
-	<p>Then, the following command line computes the impact from the pragma statements in the code of functions
-	<tt>f1,...,fn</tt>:<br>
-	<code>frama-c -impact-pragma f1,...,fn file1.c file2.c</code></p>
-
-	<p>To print the list of impacted statements on the standard output:<br>
-	<code>frama-c -impact-print file1.c file2.c</code></p>
-  </dd>
-
-  <dt class="subTitle">Dependency</dt>
-
-  <dd>
-	<p>This plug-in depends on results of the
-          <a href="eva.html">Eva</a> plug-in.</p>
-  </dd>
-</dl>

_fc-plugins/impact.md

+---
+layout: plugin
+title: Impact analysis
+description: Highlights the locations in the source code that are impacted by a modification.
+key: browsing
+distrib_mode: main
+---
+
+## Overview
+
+The **Impact analysis** plug-in allows the automatic computation of the set of
+statements impacted by the side effects of a statement of a C program.
+Statements not appearing in this set are guaranteed not to be impacted by the
+selected statement.
+
+Impact analysis is available through a contextual menu at each statement in the
+Frama-C graphical user interface. Invoking this analysis on a statement
+displays the impact of the statement on the rest of the program.
+
+![Impact screenshot on the GUI](/assets/img/plugins/impact-img.png)
+
+## Usage
+
+The plug-in can be used both with the graphical user interface and in batch
+mode. In batch mode, you must put pragmas on the statements you want to analyze:
+`/*@ impact pragma stmt; */`
+
+Then, the following command line computes the impact from the pragma statements
+in the code of functions `f1,...,fn`:
+
+    frama-c -impact-pragma f1,...,fn file1.c file2.c
+
+To print the list of impacted statements on the standard output:
+
+    frama-c -impact-print file1.c file2.c
+
+## Dependencies
+
+This plug-in depends on results of the [Eva](eva.html) plug-in.

_fc-plugins/instantiate.md

+---
+layout: plugin
+title: Instantiate
+description: Instantiate creates function specializations for other plugins.
+key: code
+distrib_mode: main
+---
+
+## Overview
+
+The **Instantiate** plug-in (distributed with Frama-C and disabled by
+default) is meant to build function specialization to C functions in a
+project when the original specification (or prototype of the function)
+cannot be efficiently used by some plugins. Generally, it is used to
+specialize functions that receive `void*` parameters.
+
+For each call for which an instantiation generator is available and if
+the call is well-typed according to this generator, **Instantiate**
+replaces this call with a call to an automatically generated
+specialization corresponding to the call. Note that the contract of the
+generated function is considered verified.
+
+## Quick Start
+
+The plug-in is enabled by setting the option `-instantiate`. The result
+can be output via the kernel option `-print`. It can also be directly
+used by other plug-ins.
+
+## Example
+
+Example input:
+
+```
+#include <string.h>
+void main(void){
+  char copy[13];
+  memcpy(copy, "Hello world!", 13);
+}
+```
+
+Example output:
+
+```
+/* Generated by Frama-C */
+#include "stddef.h"
+#include "string.h"
+#include "strings.h"
+/*@ requires
+      separation: \separated(dest + (0 .. len - 1), src + (0 .. len - 1));
+    requires aligned_end: len % 1 ≡ 0;
+    requires valid_dest: \valid(dest + (0 .. len - 1));
+    requires valid_read_src: \valid_read(src + (0 .. len - 1));
+    ensures
+      copied: ∀ ℤ j0; 0 ≤ j0 < len ⇒ *(dest + j0) ≡ *(src + j0);
+    ensures result: \result ≡ dest;
+    assigns *(dest + (0 .. len - 1)), \result;
+    assigns *(dest + (0 .. len - 1)) \from *(src + (0 .. len - 1));
+    assigns \result \from dest;
+ */
+char *memcpy_char(char *dest, char const *src, size_t len)
+{
+  char *__retres;
+  __retres = (char *)memcpy((void *)dest,(void const *)src,len);
+  return __retres;
+}
+
+void main(void)
+{
+  char copy[13];
+  memcpy_char(copy,"Hello world!",(unsigned int)13);
+  return;
+}
+```
+
+## Technical Notes
+
+- The default behavior of this plugin is to replace calls in every
+  functions. The option `-instantiate-fct` can be used to select the
+  functions to process.
+
+- Currently, the plugin supports `memcmp`, `memcpy`, `memmove`,
+  `memset` (partially, check the `README` for more details),
+  `malloc`, `calloc` and `free`. The support of each of this function
+  is enabled by default and can be deactivated using the option
+  `-instantiate-no-<function name>`
+
+## Further Reading
+
+Information about the plug-in is available via its help option:
+
+    frama-c -instantiate-help
\ No newline at end of file

_fc-plugins/jcard.html

----
-layout: plugin
-title: JCard
-description: JavaCard Front-End for Frama-C
-key: front
-distrib_mode: obsolete
----
-
-<dl class="defnitionList">
-  <dt class="subTitle">Overview</dt>
-  <dd><p>JCard is a JavaCard front-end for Frama-C, based on
-      <a href="http://javalib.gforge.inria.fr/">JavaLib and Sawja</a>.
-      It is meant to transform Java bytecode into Frama-C's internal C
-      representation. After that, main analysis plug-ins can operate as
-      usual.
-    </p>
-  </dd>
-  <dt class="subTitle">Use</dt>
-  <dd>
-    <p>Once installed, JCard will automatically consider any <tt>.java</tt>
-    or <tt>.class</tt> file passed on the Frama-C command line as java input
-    and attempt to parse them.</p>
-    <p>JCard is not publicly released, and there is no guarantee that it
-      is compatible with current Frama-C version. It is usually made available
-      as part of collaborative projects or through direct partnership.
-    </p>
-  </dd>
-</dl>

_fc-plugins/jcard.md

+---
+layout: plugin
+title: JCard
+description: JavaCard Front-End for Frama-C
+key: front
+distrib_mode: obsolete
+---
+
+## Overview
+
+JCard is a JavaCard front-end for Frama-C, based on
+[JavaLib and Sawja](http://javalib.gforge.inria.fr/).
+It is meant to transform Java bytecode into Frama-C's internal C
+representation. After that, main analysis plug-ins can operate as
+usual.
+
+## Usage
+
+Once installed, JCard will automatically consider any `.java`
+or `.class` file passed on the Frama-C command line as java input
+and attempt to parse them.
+JCard is not publicly released, and there is no guarantee that it
+is compatible with the current Frama-C version. It is usually made available
+as part of collaborative projects or through direct partnerships.

_fc-plugins/jessie.html

----
-layout: plugin
-title: Jessie
-description: A deductive verification plug-in.
-key: main
-distrib_mode: obsolete
----
-
-<dl class="defnitionList">
-  <dt class="subTitle">Overview</dt>
-
-  <dd>
-        <p><b>Warning</b> Jessie is currently not actively maintained and
-          probably incompatible with latest Frama-C versions
-        </p>
-	<p>The <b>Jessie</b> plug-in allows deductive verification of C programs annotated with <a class="extlink" href=https://github.com/acsl-language/acsl>ACSL</a>. It uses internally the languages and tools of the
-	<a class="extlink" href="http://why3.lri.fr">Why3 environment</a>.
-        The generated verification conditions can be submitted to many external
-        automatic
-	provers including
-	<a href="https://alt-ergo.ocamlpro.com/">Alt-Ergo</a>, <a href=
-	"https://github.com/Z3Prover">Z3</a> and <a href="https://cvc4.github.io/">CVC4</a>.</p>
-
-	<p>For more complex situations, interactive theorem provers can be used to establish validity of VCs. Please look
-	at the <a class="extlink" href="http://krakatoa.lri.fr/">Jessie</a> web page for more details.</p>
-  </dd>
-
-  <dt class="subTitle">Usage</dt>
-
-  <dd>
-	<p>The plug-in is activated with the following command line:</p>
-	<pre>
-frama-c -jessie [options] &lt;file&gt;.c</pre>
-
-	<p>A short manual including a tutorial and reference is available on the <a href="http://krakatoa.lri.fr/">Jessie
-	Web page</a>. Please read this document for details on other command-line options and supported or unsupported
-	features.</p>
-  </dd>
-</dl>

_fc-plugins/jessie.md

+---
+layout: plugin
+title: Jessie
+description: A deductive verification plug-in
+key: main
+distrib_mode: obsolete
+---
+
+## Overview
+
+**Warning** Jessie is currently not actively maintained and
+probably incompatible with the latest Frama-C versions.
+
+The **Jessie** plug-in allows deductive verification of C programs annotated
+with [ACSL](acsl.html). It uses internally the languages and tools of the
+[Why3](http://why3.lri.fr) environment.
+The generated verification conditions can be submitted to many external
+automatic provers including
+[Alt-Ergo](https://alt-ergo.ocamlpro.com/),
+[Z3](https://github.com/Z3Prover) and [CVC4](https://cvc4.github.io/).
+
+For more complex situations, interactive theorem provers can be used to
+establish validity of VCs. Please look at the
+[Jessie](http://krakatoa.lri.fr) web page for more details.
+
+## Usage
+
+The plug-in is activated with the following command line:
+
+    frama-c -jessie [options] <file>.c
+
+A short manual including a tutorial and reference is available on the
+[Jessie](http://krakatoa.lri.fr) web page. Please read this document for
+details on other command-line options, as well as supported and unsupported
+features.

_fc-plugins/markdown-report.html

----
-layout: plugin
-title: Markdown Report (MdR)
-description: Markdown and SARIF reports on status of ACSL annotations
-key: reporting
-distrib_mode: main
----
-
-<dl class="defnitionList">
-  <dt class="subTitle">Overview</dt>
-  <dd><p>Markdown Report, or MdR for short 
-      is meant to provide a summary of the status (valid, invalid,
-      unknown) of ACSL annotations present on the code under analysis. It
-      features a draft mode, which will output a skeleton of a report in the
-      <a href="https://pandoc.org/MANUAL.html#pandocs-markdown">pandoc-markdown
-      </a> format, with some space left for the user to provide additional
-      information about the context of the analysis, such as an explanation
-      about the ACSL specification used for stubbing a function,
-      or the reasons why an alarm emitted by
-      <a href="eva.html">Eva</a>
-      is in fact a false alarm and can thus be ignored.
-    </p>
-    <p>Once the user is satisfied with the text they have provided, the final
-      document can be produced by MdR. Two output formats can be chosen, either
-      Pandoc Markdown, which can then be transformed into most popular
-      formats (pdf, docx, odt, html, ...) with the
-      <a href="https://pandoc.org"> pandoc</a> tool,
-      or <a href="https://www.oasis-open.org/committees/tc_home.php?wg_abbrev=sarif">SARIF</a>,
-      the Static Analyzer Results Interchange Format,
-      a json schema aiming at unifiying the output formats of static analyzers.
-    </p>
-  </dd>
-  <dt class="subTitle">Use</dt>
-  <dd>
-    <p>MdR is part of the main distribution of Frama-C. It is typically
-      used after a main analysis, e.g. with
-      <code>frama-c -eva file.c -then -mdr-gen sarif -mdr-out file.json</code>
-    </p>
-    <p>MdR is currently in an early stage of development, notably its SARIF
-      output is known to be quite incomplete.
-    </p>
-  </dd>
-</dl>