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

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

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, OccurrencesgetVarOccurrences ()
Map< CFGNode, CFGHandlegetDictionary ()
CFGNode getStartNode ()
State getStartState ()

Detailed Description

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

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

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


State cz::muni::stanse::lockchecker::FunctionStateSummary::getOutputState (  )  [inline]

output state of this function

ErrorHolder cz::muni::stanse::lockchecker::FunctionStateSummary::getErrHolder (  )  [inline]

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

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

summary of the called function
varTransformations between this and called function

Map<String, Occurrences> cz::muni::stanse::lockchecker::FunctionStateSummary::getVarOccurrences (  )  [inline]

map of variable occurrences (identifier, Occurrences)

Map<CFGNode, CFGHandle> cz::muni::stanse::lockchecker::FunctionStateSummary::getDictionary (  )  [inline]

dictionary used to translate between node and handle

CFGNode cz::muni::stanse::lockchecker::FunctionStateSummary::getStartNode (  )  [inline]

start node of this summary's function

State cz::muni::stanse::lockchecker::FunctionStateSummary::getStartState (  )  [inline]

start state of this summary's function

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

Generated on Thu Jan 13 16:24:09 2011 for Stanse by  doxygen 1.5.6