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
Compare
and
Show latest version
23 files
+ 283
− 340
Compare changes
  • Side-by-side
  • Inline
Files
23
_fc-plugins/aorai.md
+ 52
− 50
@@ -4,85 +4,87 @@ 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.
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.
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 [framework](http://frama-c.com/).
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).
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 a ltl
like syntax, while *.ya* are description of automata in a
yacc-like syntax.
Options are:
<dl>
<dt>`-aorai-verbose`
Gives some information during computation, such as
used/produced files and heuristics applied
<dt>`-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.
<dt>`-aorai-dot`
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>.
<dt>`-aorai-acceptance`
if set, considers acceptation states (Only on finite traces).
If not, only the safety is verified.
<dt>`-aorai-output-c-file` *file*
Outputs the annotated program in *file* (defaults is to
derive a name from the one of the first input file)
<dt>`-aorai-help`
Gives the whole list of options
frama-c file.c -aorai-ltl file.ltl
frama-c file.c -aorai-automata file.ya
## Ressources
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.
<ul class="none">
- <a class="pdf" href="/download/frama-c-aorai-manual.pdf">Short
Documentation</a>
- <a class="src" href="/download/frama-c-aorai-example.tgz">Couple
of simple examples</a>
- `-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.
Other ressources can be found at <a class="extlink" href="http://amazones.gforge.inria.fr/aorai/">the official web page of
Aoraï.</a>
- `-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.
## Installation Dependencies
- `-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 isonly a restriction to the terminating state of the program thathave to be an acceptation 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-array or C-structure are not statically evaluated (it's 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.
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 [contact](contact.html) page for more information.
<span class="title">End Note:</span> 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/).