cz::muni::stanse::lockchecker::FunctionStateSummary Class Reference

Collaboration diagram for cz::muni::stanse::lockchecker::FunctionStateSummary:

[legend]

List of all members.

Public Member Functions
	FunctionStateSummary (Map< CFGNode, CFGHandle > dictionary, StateRepository repos, CFGNode startNode, State startState, Configuration conf)
void	setOutputState (State outputState)
State	getOutputState ()
ErrorHolder	getErrHolder ()
void	changeVarsOccurrence (int increment, CFGNode node, State state)
String	toString ()
void	join (FunctionStateSummary summary, VarTransformations varTransformations)
Map< String, Occurrences >	getVarOccurrences ()
Map< CFGNode, CFGHandle >	getDictionary ()
CFGNode	getStartNode ()
State	getStartState ()

---

Detailed Description

This class represents summary for a given function with given entered state

Author:

Radim Cebis

---

Constructor & Destructor Documentation

cz::muni::stanse::lockchecker::FunctionStateSummary::FunctionStateSummary	(	Map< CFGNode, CFGHandle >	dictionary,
		StateRepository	repos,
		CFGNode	startNode,
		State	startState,
		Configuration	conf
	)			[inline]

Constructs function state summary for a given startNode and startState

Parameters:

	dictionary
	repos	State repository
	startNode	this summary's function start node
	startState	this summary's function start state
	conf	Configuration

---

Member Function Documentation

void cz::muni::stanse::lockchecker::FunctionStateSummary::setOutputState

(

State

outputState

)

[inline]

Sets output state of this function

Parameters:

outputState

State cz::muni::stanse::lockchecker::FunctionStateSummary::getOutputState

(

)

[inline]

Returns:

output state of this function

ErrorHolder cz::muni::stanse::lockchecker::FunctionStateSummary::getErrHolder

(

)

[inline]

Returns:

error holder of this summary

void cz::muni::stanse::lockchecker::FunctionStateSummary::changeVarsOccurrence	(	int	increment,
		CFGNode	node,
		State	state
	)			[inline]

Changes variable occurrence for the given node and state

Parameters:

	increment	how much increment the occurrence - should be 1 or -1
	node	containing the occurrence
	state	for which occurrence should be changed

String cz::muni::stanse::lockchecker::FunctionStateSummary::toString

(

)

[inline]

void cz::muni::stanse::lockchecker::FunctionStateSummary::join	(	FunctionStateSummary	summary,
		VarTransformations	varTransformations
	)			[inline]

Joins this summary with the summary of the called function

Parameters:

	summary	of the called function
	varTransformations	between this and called function

Map<String, Occurrences> cz::muni::stanse::lockchecker::FunctionStateSummary::getVarOccurrences

(

)

[inline]

Returns:

map of variable occurrences (identifier, Occurrences)

Map<CFGNode, CFGHandle> cz::muni::stanse::lockchecker::FunctionStateSummary::getDictionary

(

)

[inline]

Returns:

dictionary used to translate between node and handle

CFGNode cz::muni::stanse::lockchecker::FunctionStateSummary::getStartNode

(

)

[inline]

Returns:

start node of this summary's function

State cz::muni::stanse::lockchecker::FunctionStateSummary::getStartState

(

)

[inline]

Returns:

start state of this summary's function

---

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

• src/cz/muni/stanse/lockchecker/FunctionStateSummary.java