Index of modules

A
AbstractInterpretation [Aorai_option]
AddingOperationNameAndStatusInSpecification [Aorai_option]
Aorai

Aorai plugin (AKA Ltl_to_acsl).

Aorai_dataflow

Compute the set of possible state at each function call and return.

Aorai_option
Aorai_register
Aorai_state [Data_for_aorai]
Aorai_typed_trans [Data_for_aorai]
Aorai_utils
Aorai_visitors
AutomataSimplification [Aorai_option]
Axiomatization [Aorai_option]
B
Bool3
Buchi [Aorai_option]
C
ConsiderAcceptance [Aorai_option]
D
Data_for_aorai
Deterministic [Aorai_option]

true if the user declares that its ya automaton is deterministic.

Dot [Aorai_option]
DotSeparatedLabels [Aorai_option]
H
Hashtbl [Datatype.S_with_collections]
K
Key [Datatype.Hashtbl]

Datatype for the keys of the hashtbl.

Key [Datatype.Map]

Datatype for the keys of the map.

L
Logic_simplification

Basic simplification over Promelaast.typed_condition

Ltl_File [Aorai_option]
Ltl_output
Ltlast

The abstract tree of LTL formula.

Ltllexer
Ltlparser
M
Make [Datatype.Hashtbl]

Build a datatype of the hashtbl according to the datatype of values in the hashtbl.

Make [Datatype.Map]

Build a datatype of the map according to the datatype of values in the map.

Map [Datatype.S_with_collections]
O
Output_C_File [Aorai_option]
Output_Spec [Aorai_option]
P
Path_analysis
Promelaast

The abstract tree of promela representation.

Promelalexer
Promelalexer_withexps
Promelaoutput
Promelaparser
Promelaparser_withexps
S
Set [Datatype.S_with_collections]
T
Test [Aorai_option]
To_Buchi [Aorai_option]
U
Utils_parser
Y
Ya [Aorai_option]
Yalexer
Yaparser