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 or Eva plug-ins.
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 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.
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 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.
- 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.
Aoraï has been originally written by Nicolas Stouls, CITI Labs, AMAZONES team. It is currently maintained by CEA LIST as part of the main Frama-C distribution. See our contact 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.
Other resources can be found at the official web page of Aoraï.