Skip to content
Snippets Groups Projects

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

Merged [plugins] Convert to Markdown, normalize section names and URLs
plugins-to-markdown into master
1 unresolved thread
Merged Andre Maroneze requested to merge plugins-to-markdown into master
1 unresolved thread
Viewing commit 2f3df371
Show latest version
56 files
+ 1823
− 1827
Compare changes
  • Side-by-side
  • Inline
Files
56
_fc-plugins/aorai.html deleted 100755 → 0
+ 0
− 88
---
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>