Public Member Functions
|AutomatonChecker (final File xmlFile)|
|Parses accepted XML automata definition and initializes internal structures related to automata definition. |
|Uniquelly identifies the checker by the string identifier. |
|CheckingResult||check (final LazyInternalStructures internals, final CheckerErrorReceiver errReciver, final CheckerProgressMonitor monitor) throws XMLAutomatonSyntaxErrorException|
|Does the source code checking itself. |
The checker is based on execution of finite automata specified in XML file whose states are propagated through program locations. Some automata states are considered as erroneous, so when automaton's transition to such erroneous state is invoked in some program location, then appropriate error message is reported. Program locations, which are considered for automata state propagation are found by pattern matching. These pattern are specified in the XML file defining automata as well.
Parses accepted XML automata definition and initializes internal structures related to automata definition.
|XMLdefinition||XML representation of AST|
|CheckingResult cz::muni::stanse::automatonchecker::AutomatonChecker::check||(||final LazyInternalStructures||internals,|
|)|| throws XMLAutomatonSyntaxErrorException
Does the source code checking itself.
Method searches through source code to find matching patterns defined in XML automata definition file. Each such matched location in the source code is assigned an instance of PatternLocation class. Initial location in the program is always introduced and is initialized with initial states of all automata to be run on the source code.
The computation itself is simple distribution of automata states between instances of PatternLocation class (locations are linked together with respect to control-flow of source code). Automata states are transformed with respect to transition rules assigned to each PatternLocation and then distributed to linked locations. This procedure is finished, when no location was delivered automaton state, which was not processed in that location.
Error detection is the final phase of the procedure. All PatternLocations are crossed and checked for error states. Each PatternLocation has assigned set of error transition rules which are applied to all processed states in the location. If some error transition rule can be applied to processed states, then it means the source code contains error. Each error rule contains description of an error it checks for. Those error transition rules are defined in XML automaton definition file.
|units||List of translations units (described in internal structures like CFGs and ASTs)|
|XMLAutomatonSyntaxErrorException||Is thrown, when some semantic error is detected in XML automata definition.|