| Aorai |
Aorai plugin (AKA Ltl_to_acsl).
|
| Aorai_dataflow |
Compute the set of possible state at each function call and return.
|
| Aorai_option | true if the user declares that its ya automaton is deterministic.
|
| Aorai_register | |
| Aorai_utils |
Given a transition a function and a function status (call or return)
it returns if the cross condition can be satisfied
with only function status.
|
| Aorai_visitors |
This visitor adds an auxiliary function for each C function which takes
care of setting the automaton in a correct state before calling the
original one, and replaces each occurrence of the original function by
the auxiliary one.
|
| Bool3 | |
| Data_for_aorai |
Module of data management used in all the plugin Aorai.
|
| Logic_simplification |
Basic simplification over
Promelaast.typed_condition
|
| Ltl_output | |
| Ltlast |
The abstract tree of LTL formula.
|
| Ltllexer | |
| Ltlparser | |
| Path_analysis |
since Nitrogen-20111001
|
| Promelaast |
The abstract tree of promela representation.
|
| Promelalexer | |
| Promelalexer_withexps | |
| Promelaoutput | |
| Promelaparser | |
| Promelaparser_withexps | |
| Utils_parser | |
| Yalexer | |
| Yaparser |