Plugins Kernel Specification GUI Ivette

Aoraï

Overview

The Aoraï plug-in provides a method to automatically annotate a C program according to a state automaton describing the sequences of function calls that are allowed during an execution of the program. The classical method to validate annotations is to use the Wp or Eva 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 that website no longer exists, and the version that used to be hosted there was obsolete and did not compile with newer versions of Frama-C.

Usage

The plug-in is activated with the following command line:

frama-c file.c -aorai-automata file.ya

file.ya is supposed to contain the description of the automaton using a simple format specific to Aoraï.

Other options include:

  • -aorai-verbose: Gives some information during computation, such as used/produced files and heuristics applied.

  • -aorai-dot: Generates a dot file of the 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.

Installation Dependencies

  • 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.

Contact

Aoraï has been originally written by Nicolas Stouls, CITI Labs, Phenix 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.

Further Reading