cz::muni::stanse::automatonchecker::AutomatonChecker Class Reference

Static checker which is able to detect locking problems, interrupts enabling/disabling problems, unnecessary check optimizations and points-to problems like null pointer dereference and memory leaks. More...

Inheritance diagram for cz::muni::stanse::automatonchecker::AutomatonChecker:

[legend]

Collaboration diagram for cz::muni::stanse::automatonchecker::AutomatonChecker:

[legend]

List of all members.

Public Member Functions
	AutomatonChecker (final File xmlFile)
	Parses accepted XML automata definition and initializes internal structures related to automata definition.
String	getName ()
	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.

---

Detailed Description

Static checker which is able to detect locking problems, interrupts enabling/disabling problems, unnecessary check optimizations and points-to problems like null pointer dereference and memory leaks.

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.

See also:

cz.muni.stanse.checker.Checker

---

Constructor & Destructor Documentation

cz::muni::stanse::automatonchecker::AutomatonChecker::AutomatonChecker

(

final File

xmlFile

)

[inline]

Parses accepted XML automata definition and initializes internal structures related to automata definition.

Parameters:

XMLdefinition

XML representation of AST

Exceptions:

XMLAutomatonSyntaxErrorException

---

Member Function Documentation

String cz::muni::stanse::automatonchecker::AutomatonChecker::getName

(

)

[inline, virtual]

Uniquelly identifies the checker by the string identifier.

Returns:

String which uniquelly identifies the checker.

See also:

cz.muni.stanse.checker.Checker::getName()

Implements cz::muni::stanse::checker::Checker.

CheckingResult cz::muni::stanse::automatonchecker::AutomatonChecker::check	(	final LazyInternalStructures	internals,
		final CheckerErrorReceiver	errReciver,
		final CheckerProgressMonitor	monitor
	)			throws XMLAutomatonSyntaxErrorException [inline, virtual]

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.

Parameters:

units

List of translations units (described in internal structures like CFGs and ASTs)

Returns:

List of errors found in the source code.

Exceptions:

XMLAutomatonSyntaxErrorException

Is thrown, when some semantic error is detected in XML automata definition.

See also:

cz.muni.stanse.checker.Checker::check(java.util.List)

Implements cz::muni::stanse::checker::Checker.

---

The documentation for this class was generated from the following file:

• src/cz/muni/stanse/automatonchecker/AutomatonChecker.java