Aoraï plug-in (Aka LTL to ACSL)
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.
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.yaThese 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.
- Gives some information during computation, such as used/produced files and heuristics applied
- Displays, at the end of the process, the computed specification of each operation, in terms of Büchi states and transitions.
- Generates a dot file of the Büchi automaton. Dot is a graph format used by the GraphViz tool.
- if set, considers acceptation states (Only on finite traces). If not, only the safty is verified.
- -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)
- Gives the whole list of options
Other ressources can be found at the official web page of Aoraï.
- Only the safety part of properties is check. 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.
- 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.
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.