The Aoraï plug-in for Frama-C 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 Jessie plug-in and the Why tool.

The plug-in source code is available in the resources section. In order to install this plug-in, you need to have the Frama-C framework.

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 Paul Gastin (ENS Cachan).

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 to property to verify: .ltl files are described in a ltl like syntax, while .ya are description of automata in a 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 tool.

-aorai-acceptance

if set, considers acceptation states (Only on finite traces). If not, only the safty is verified.

-aorai-help

Gives the whole list of options

• Source code of Aoraï with installer (for SVN version of Frama-C)
• Source code of Aoraï with installer (for public version of Frama-C Carbon)
• Source code of Aoraï with installer (for public version of Frama-C Boron)
• Short Documentation
• Couple of simple examples

Currently, the switch statement is not supported and only the safety part of the LTL formula is check. The variant generation is a future for the implementation.

For any questions, remarks or suggestions, please contact  Nicolas Stouls (CITI Labs, AMAZONES team).

End Note: to the question "Why this name: Aoraï ?" my answer is: why not ? Aoraï is the name of the taller reachable mount in the Tahiti island and its reachability is not always obvious.