Aorai plugin


Directory plugins

Section Aorai (in plugins/aorai)


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