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

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

Direct Known Subclasses:

TSAliasAnalysisAssignmentFlowNode, TSAliasAnalysisEndOfScope, TSDummyFlowNode, TSFixpointerIterationFlowNode, TSStateChangingFlowNode

public abstract class TSFlowNode
extends FlowNode<MethodTypestateAnalysis>

This class is a parent to all classes of the control flow graph that are used by the typestate analysis. It also provides helper methods to create those nodes.

Constructor Summary

TSFlowNode()

Method Summary

static TSFlowNode	getDummyNode(java.lang.String id) Get an dummy FlowNode, it will just pass on the analysis.
static TSFlowNode	getFixpointNode(java.lang.String id) Returns a TSFixpointerIterationFlowNode.
static TSFlowNode	TSFlowNodefromAnnotatedTree(AliasAnalysisVarHandle var, com.sun.source.tree.Tree tree, checkers.types.AnnotatedTypeFactory factory) Factory method to create typestate changning FlowNodes for the control flow graph.

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

addSuccessor, forwardAnalysis, hasSuccessors, printAll, toString

Methods inherited from class java.lang.Object

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

Constructor Detail

TSFlowNode

public TSFlowNode()

Method Detail

TSFlowNodefromAnnotatedTree

public static TSFlowNode TSFlowNodefromAnnotatedTree(AliasAnalysisVarHandle var,
                                                     com.sun.source.tree.Tree tree,
                                                     checkers.types.AnnotatedTypeFactory factory)

Factory method to create typestate changning FlowNodes for the control flow graph.

Parameters:

factory - the AnnotatedTypeFactory to use for this part of the code

var - the alias analysis handle for the variable whose typestate is to be changed

tree - the tree containing the typestate annotations

Returns:

A TSFlowNode that changes the typestate of the passed var, or null if no FlowNode needs to be integrated in the graph.

getFixpointNode

public static final TSFlowNode getFixpointNode(java.lang.String id)

Returns a TSFixpointerIterationFlowNode. Which should be always used to handle point in the graph where the analysis will need to fixpoint iterate.

Parameters:

id - the debug name

Returns:

A fixpoint iteration TSFlowNode

getDummyNode

public static final TSFlowNode getDummyNode(java.lang.String id)

Get an dummy FlowNode, it will just pass on the analysis.

Parameters:

id - the debug name

Returns:

The dummy FlowNode.