de.unisaarland.cs.st.jerify.verifier.typestate
Class MethodCFGWorkData

java.lang.Object
  de.unisaarland.cs.st.jerify.verifier.typestate.MethodCFGWorkData

public class MethodCFGWorkData
extends java.lang.Object

Used to store all information to create the flow data-structure while visiting each method.

Author:

Daniel Wand

See Also:

ClassCFG

Constructor Summary

MethodCFGWorkData(checkers.types.AnnotatedTypeFactory factory, TSFlowNode flowBegin, TSFlowNode flowEnd)
Create an TSInfo instance with the previous (aka first) Node and the methodEnd (aka last) Node beeing set.

MethodCFGWorkData(MethodCFGWorkData infos)
Copy constructor that only copies those elements that are always needed to be copied Does not copy methodThrows, because the branches dont need to know what is thrown outside their scode.

MethodCFGWorkData(TSFlowNode flowBegin, TSFlowNode flowEnd, ClassCFGAliasAnalysis aliasAnalysis, DataFlowCFGAnalysis dataflowAnalysis)
Create an TSInfo instance with the previous (aka first) Node and the methodEnd (aka last) Node beeing set.

Method Summary

void	addThrow(javax.lang.model.type.TypeMirror exception, Pair<AliasAnalysisVarHandle,TSFlowNode> information)
boolean	checkPrevious(com.sun.source.tree.Tree tree)
void	clearPreviousFlowNode()
MethodCFGWorkData	copy() Create a copy.
ClassCFGAliasAnalysis	getAliasAnalysis()
DataFlowCFGAnalysis	getDataFlowAnalysis()
TSFlowNode	getPrevious()
java.util.List<java.lang.String>	getRequiredReturnStates()
MethodCFGThrowsWorkData	getThrowInformation()
boolean	hasPreviousFlowNode()
void	setAliasAnalysis(ClassCFGAliasAnalysis aliasAnalysis)
void	setDataFlowAnalysis(DataFlowCFGAnalysis dataflowAnalysis)
void	setPreviousFlowNode(TSFlowNode newPrevious)
void	setRequiredReturnStates(java.util.List<java.lang.String> requiredReturnState)
void	setThrowInformation(MethodCFGThrowsWorkData methodThrows)
void	updatePreviousFlowNode(TSFlowNode newPrevious, com.sun.source.tree.Tree tree)

Methods inherited from class java.lang.Object

equals, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait

Constructor Detail

MethodCFGWorkData

public MethodCFGWorkData(MethodCFGWorkData infos)

Copy constructor that only copies those elements that are always needed to be copied Does not copy methodThrows, because the branches dont need to know what is thrown outside their scode. We simply merge in the throws of each branch later. (Be aware that this has to be done everywhere where branches merge)

Parameters:

infos -

MethodCFGWorkData

public MethodCFGWorkData(TSFlowNode flowBegin,
                         TSFlowNode flowEnd,
                         ClassCFGAliasAnalysis aliasAnalysis,
                         DataFlowCFGAnalysis dataflowAnalysis)

Create an TSInfo instance with the previous (aka first) Node and the methodEnd (aka last) Node beeing set.

Parameters:

previous -

methodEnd -

MethodCFGWorkData

public MethodCFGWorkData(checkers.types.AnnotatedTypeFactory factory,
                         TSFlowNode flowBegin,
                         TSFlowNode flowEnd)

Create an TSInfo instance with the previous (aka first) Node and the methodEnd (aka last) Node beeing set.

Parameters:

previous -

methodEnd -

Method Detail

updatePreviousFlowNode

public void updatePreviousFlowNode(TSFlowNode newPrevious,
                                   com.sun.source.tree.Tree tree)

getPrevious

public TSFlowNode getPrevious()

clearPreviousFlowNode

public void clearPreviousFlowNode()

setPreviousFlowNode

public void setPreviousFlowNode(TSFlowNode newPrevious)

hasPreviousFlowNode

public boolean hasPreviousFlowNode()

checkPrevious

public boolean checkPrevious(com.sun.source.tree.Tree tree)

addThrow

public void addThrow(javax.lang.model.type.TypeMirror exception,
                     Pair<AliasAnalysisVarHandle,TSFlowNode> information)

getThrowInformation

public MethodCFGThrowsWorkData getThrowInformation()

setThrowInformation

public void setThrowInformation(MethodCFGThrowsWorkData methodThrows)

setRequiredReturnStates

public void setRequiredReturnStates(java.util.List<java.lang.String> requiredReturnState)

getRequiredReturnStates

public java.util.List<java.lang.String> getRequiredReturnStates()

getAliasAnalysis

public ClassCFGAliasAnalysis getAliasAnalysis()

setAliasAnalysis

public void setAliasAnalysis(ClassCFGAliasAnalysis aliasAnalysis)

getDataFlowAnalysis

public DataFlowCFGAnalysis getDataFlowAnalysis()

setDataFlowAnalysis

public void setDataFlowAnalysis(DataFlowCFGAnalysis dataflowAnalysis)

copy

public final MethodCFGWorkData copy()

Create a copy. See the copy constructor for details what is copied.

Returns:

See Also:

#TSInfos(TSFlowNode previous, TSFlowNode methodEnd)