de.unisaarland.cs.st.jerify.verifier.cfg.flownodes.typestate
Class TSFixpointerIterationFlowNode

java.lang.Object
  de.unisaarland.cs.st.jerify.verifier.cfg.flownodes.FlowNode<MethodTypestateAnalysis>
      de.unisaarland.cs.st.jerify.verifier.cfg.flownodes.typestate.TSFlowNode
          de.unisaarland.cs.st.jerify.verifier.cfg.flownodes.typestate.TSFixpointerIterationFlowNode

public class TSFixpointerIterationFlowNode
extends TSFlowNode

A FlowNode does not do anything to the analysis data, but is a point in the graph where the analysis will pass several time, e.g. to fixpoint iterate the analysis of a loop. If you expect a FlowNode to handle a fixpoint iteration always use this class.

Author:

Daniel Wand (typestate@ewand.de)

Method Summary

void	forwardAnalysis(CFGAnalysis<MethodTypestateAnalysis> newAnalysis) Only further propagate the analysis if it is not a subset of the previously seen analyses.
void	printAll() print all nodes of this cfg (all reachable)
java.lang.String	toString()

Methods inherited from class de.unisaarland.cs.st.jerify.verifier.cfg.flownodes.typestate.TSFlowNode

getDummyNode, getFixpointNode, TSFlowNodefromAnnotatedTree

Methods inherited from class de.unisaarland.cs.st.jerify.verifier.cfg.flownodes.FlowNode

addSuccessor, hasSuccessors

Methods inherited from class java.lang.Object

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

Method Detail

toString

public final java.lang.String toString()

Specified by:

toString in class FlowNode<MethodTypestateAnalysis>

printAll

public final void printAll()

Description copied from class: FlowNode

print all nodes of this cfg (all reachable)

Overrides:

printAll in class FlowNode<MethodTypestateAnalysis>

forwardAnalysis

public final void forwardAnalysis(CFGAnalysis<MethodTypestateAnalysis> newAnalysis)

Only further propagate the analysis if it is not a subset of the previously seen analyses.

Specified by:

forwardAnalysis in class FlowNode<MethodTypestateAnalysis>

Parameters:

newAnalysis - the current analysis that is propagated through the control flow graph.