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

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.TSStateChangingFlowNode

Direct Known Subclasses:

TSStateFilterNode, TSStateSetFlowNode, TSTransitionFlowNode

public abstract class TSStateChangingFlowNode
extends TSFlowNode

This class is a parent to all classes that actually change the typestate analysis. It also provides helper methods to create those nodes.

Author:

Daniel Wand (typestate@ewand.de)

Constructor Summary

TSStateChangingFlowNode()

Method Summary

static TSStateChangingFlowNode	analyseRequireState(AliasAnalysisVarHandle var, javax.lang.model.element.AnnotationMirror requireState, com.sun.source.tree.Tree tree) Handles the @RequireState creation of a FlowNode
static TSStateChangingFlowNode	analyseRequireState(AliasAnalysisVarHandle var, java.util.Collection<java.lang.String> isInList, com.sun.source.tree.Tree tree) Handles the @RequireState creation of a FlowNode
static StateChanges	getAllStateChanges(checkers.types.AnnotatedTypeMirror method, com.sun.source.tree.Tree tree) Get State Changes annotated with @ChangeState or @TS({ @ChangeStates, ...})
static java.util.Set<java.lang.String>	getAllStateChangesFromSet(checkers.types.AnnotatedTypeMirror method, com.sun.source.tree.Tree tree)
static java.util.Set<java.lang.String>	getAllStateChangesToSet(checkers.types.AnnotatedTypeMirror method, com.sun.source.tree.Tree tree)
static Pair<java.lang.String,java.util.Set<java.lang.String>>	getChangeState(javax.lang.model.element.AnnotationMirror a) Parse a ChangeState(from,to) annotation and returns the corresponding map
static TSStateSetFlowNode	getSetStateFlowNode(AliasAnalysisVarHandle handle, com.sun.source.tree.Tree tree, javax.lang.model.element.AnnotationMirror setState)
static TSFlowNode	TSFlowNodefromAnnotatedTree(AliasAnalysisVarHandle var, com.sun.source.tree.Tree tree, checkers.types.AnnotatedTypeFactory factory) Creates and returns a flownode (for the control flow graph) which corresponds to changing the typestate of the variable which is handled by the var AliasAnalysisVarHandle.
static TSFlowNode	TSFlowNodefromAnnotatedType(AliasAnalysisVarHandle var, com.sun.source.tree.Tree tree, checkers.types.AnnotatedTypeMirror annotatedType, boolean annotationOptional, checkers.types.AnnotatedTypeFactory factory) Creates and returns a flownode (for the control flow graph) which corresponds to changing the typestate of the variable which is handled by the var AliasAnalysisVarHandle.

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

getDummyNode, getFixpointNode

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

TSStateChangingFlowNode

public TSStateChangingFlowNode()

Method Detail

getSetStateFlowNode

public static final TSStateSetFlowNode getSetStateFlowNode(AliasAnalysisVarHandle handle,
                                                           com.sun.source.tree.Tree tree,
                                                           javax.lang.model.element.AnnotationMirror setState)

TSFlowNodefromAnnotatedTree

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

Creates and returns a flownode (for the control flow graph) which corresponds to changing the typestate of the variable which is handled by the var AliasAnalysisVarHandle. The typestate changes are parsed out of the annotations.

Parameters:

var - The Alias Handle of the objects whose typestate is to be changes during the analysis

tree - The tree from which to parse the annotation that tell the analysis how to change the typestate

factory -

Returns:

The FlowNode that should be inserted in the Control Flow Graph

TSFlowNodefromAnnotatedType

public static final TSFlowNode TSFlowNodefromAnnotatedType(AliasAnalysisVarHandle var,
                                                           com.sun.source.tree.Tree tree,
                                                           checkers.types.AnnotatedTypeMirror annotatedType,
                                                           boolean annotationOptional,
                                                           checkers.types.AnnotatedTypeFactory factory)

Creates and returns a flownode (for the control flow graph) which corresponds to changing the typestate of the variable which is handled by the var AliasAnalysisVarHandle. The typestate changes are parsed out of the annotations.

Parameters:

var - The Alias Handle of the objects whose typestate is to be changes during the analysis

tree - The tree for which potential errors are to be reported

The - annotated Type from which to parse the annotation that tell the analysis how to change the typestate

factory -

Returns:

The FlowNode that should be inserted in the Control Flow Graph

analyseRequireState

public static final TSStateChangingFlowNode analyseRequireState(AliasAnalysisVarHandle var,
                                                                javax.lang.model.element.AnnotationMirror requireState,
                                                                com.sun.source.tree.Tree tree)

Handles the @RequireState creation of a FlowNode

analyseRequireState

public static final TSStateChangingFlowNode analyseRequireState(AliasAnalysisVarHandle var,
                                                                java.util.Collection<java.lang.String> isInList,
                                                                com.sun.source.tree.Tree tree)

Handles the @RequireState creation of a FlowNode

getChangeState

public static final Pair<java.lang.String,java.util.Set<java.lang.String>> getChangeState(javax.lang.model.element.AnnotationMirror a)

Parse a ChangeState(from,to) annotation and returns the corresponding map

Parameters:

a - Assumes that his parameter is a @ChangeState annotation, the behavior is undefined if it is not

getAllStateChanges

public static final StateChanges getAllStateChanges(checkers.types.AnnotatedTypeMirror method,
                                                    com.sun.source.tree.Tree tree)

Get State Changes annotated with @ChangeState or @TS({ @ChangeStates, ...})

Parameters:

method - Parse the Annotations from here

tree - Code that is "responsible" (used for error reporting)

getAllStateChangesFromSet

public static final java.util.Set<java.lang.String> getAllStateChangesFromSet(checkers.types.AnnotatedTypeMirror method,
                                                                              com.sun.source.tree.Tree tree)

getAllStateChangesToSet

public static final java.util.Set<java.lang.String> getAllStateChangesToSet(checkers.types.AnnotatedTypeMirror method,
                                                                            com.sun.source.tree.Tree tree)