org.checkerframework.framework.flow

Class CFAbstractTransfer<V extends CFAbstractValue<V>,S extends CFAbstractStore<V,S>,T extends CFAbstractTransfer<V,S,T>>

java.lang.Object

org.checkerframework.dataflow.cfg.node.AbstractNodeVisitor<TransferResult<V,S>,TransferInput<V,S>>

org.checkerframework.framework.flow.CFAbstractTransfer<V,S,T>

All Implemented Interfaces:

ForwardTransferFunction<V,S>, TransferFunction<V,S>, NodeVisitor<TransferResult<V,S>,TransferInput<V,S>>

Direct Known Subclasses:

CFTransfer, InitializationTransfer, KeyForTransfer, LockTransfer

public abstract class CFAbstractTransfer<V extends CFAbstractValue<V>,S extends CFAbstractStore<V,S>,T extends CFAbstractTransfer<V,S,T>>
extends AbstractNodeVisitor<TransferResult<V,S>,TransferInput<V,S>>
implements ForwardTransferFunction<V,S>

The default analysis transfer function for the Checker Framework propagates information through assignments and uses the AnnotatedTypeFactory to provide checker-specific logic how to combine types (e.g., what is the type of a string concatenation, given the types of the two operands) and as an abstraction function (e.g., determine the annotations on literals).

Design note: CFAbstractTransfer and its subclasses are supposed to act as transfer functions. But, since the AnnotatedTypeFactory already existed and performed checker-independent type propagation, CFAbstractTransfer delegates work to it instead of duplicating some logic in CFAbstractTransfer. The checker-specific subclasses of CFAbstractTransfer do implement transfer function logic themselves.

Field Summary

Fields

Modifier and Type	Field and Description
protected CFAbstractAnalysis<V,S,T>	analysis The analysis class this store belongs to.
protected boolean	sequentialSemantics Should the analysis use sequential Java semantics (i.e., assume that only one thread is running at all times)?

Constructor Summary

Constructors

Modifier	Constructor and Description
protected	CFAbstractTransfer(CFAbstractAnalysis<V,S,T> analysis)
protected	CFAbstractTransfer(CFAbstractAnalysis<V,S,T> analysis, boolean forceConcurrentSemantics) Constructor that allows forcing concurrent semantics to be on for this instance of CFAbstractTransfer.

Method Summary

Modifier and Type	Method and Description
protected void	addInformationFromPreconditions(S info, AnnotatedTypeFactory factory, UnderlyingAST.CFGMethod method, MethodTree methodTree, ExecutableElement methodElement) Add the information from all the preconditions of the method method with corresponding tree methodTree to the store info.
protected V	finishValue(V value, S store) This method is called before returning the abstract value value as the result of the transfer function.
protected V	finishValue(V value, S thenStore, S elseStore) This method is called before returning the abstract value value as the result of the transfer function.
protected V	getValueFromFactory(Tree tree, Node node) Returns the abstract value of a non-leaf tree tree, as computed by the AnnotatedTypeFactory.
protected V	getValueWithSameAnnotations(TypeMirror type, V annotatedValue) Returns an abstract value with the given type and the annotations from annotatedValue.
S	initialStore(UnderlyingAST underlyingAST, @Nullable List<LocalVariableNode> parameters) The initial store maps method formal parameters to their currently most refined type.
protected boolean	isNotFullyInitializedReceiver(MethodTree methodTree) Returns true if the receiver of a method might not yet be fully initialized.
V	moreSpecificValue(V value1, V value2) Returns the abstract value of (value1, value2) that is more specific.
protected void	processCommonAssignment(TransferInput<V,S> in, Node lhs, Node rhs, S info, V rhsValue) Determine abstract value of right-hand side and update the store accordingly to the assignment.
protected void	processConditionalPostconditions(MethodInvocationNode n, ExecutableElement methodElement, Tree tree, S thenStore, S elseStore) Add information based on all conditional postconditions of method n with tree tree and element method to the appropriate store.
protected void	processPostconditions(MethodInvocationNode n, S store, ExecutableElement methodElement, Tree tree) Add information based on all postconditions of method n with tree tree and element method to the store store.
void	setFixedInitialStore(S s) Set a fixed initial Store.
protected List<Node>	splitAssignments(Node node) Takes a node, and either returns the node itself again (as a singleton list), or if the node is an assignment node, returns the lhs and rhs (where splitAssignments is applied recursively to the rhs -- that is, the rhs may not appear in the result, but rather its lhs and rhs may).
protected TransferResult<V,S>	strengthenAnnotationOfEqualTo(TransferResult<V,S> res, Node firstNode, Node secondNode, V firstValue, V secondValue, boolean notEqualTo) Refine the annotation of secondNode if the annotation secondValue is less precise than firstValue.
boolean	usesSequentialSemantics() Returns true if the transfer function uses sequential semantics, false if it uses concurrent semantics.
TransferResult<V,S>	visitArrayAccess(ArrayAccessNode n, TransferInput<V,S> p)
TransferResult<V,S>	visitAssignment(AssignmentNode n, TransferInput<V,S> in)
TransferResult<V,S>	visitCase(CaseNode n, TransferInput<V,S> in) A case produces no value, but it may imply some facts about the argument to the switch statement.
TransferResult<V,S>	visitClassName(ClassNameNode n, TransferInput<V,S> in)
TransferResult<V,S>	visitConditionalNot(ConditionalNotNode n, TransferInput<V,S> p) Reverse the role of the 'thenStore' and 'elseStore'.
TransferResult<V,S>	visitEqualTo(EqualToNode n, TransferInput<V,S> p)
TransferResult<V,S>	visitFieldAccess(FieldAccessNode n, TransferInput<V,S> p)
TransferResult<V,S>	visitInstanceOf(InstanceOfNode node, TransferInput<V,S> in)
TransferResult<V,S>	visitLambdaResultExpression(LambdaResultExpressionNode n, TransferInput<V,S> in)
TransferResult<V,S>	visitLocalVariable(LocalVariableNode n, TransferInput<V,S> in) Use the most specific type information available according to the store.
TransferResult<V,S>	visitMethodInvocation(MethodInvocationNode n, TransferInput<V,S> in)
TransferResult<V,S>	visitNarrowingConversion(NarrowingConversionNode n, TransferInput<V,S> p)
TransferResult<V,S>	visitNode(Node n, TransferInput<V,S> in) The default visitor returns the input information unchanged, or in the case of conditional input information, merged.
TransferResult<V,S>	visitNotEqual(NotEqualNode n, TransferInput<V,S> p)
TransferResult<V,S>	visitObjectCreation(ObjectCreationNode n, TransferInput<V,S> p)
TransferResult<V,S>	visitReturn(ReturnNode n, TransferInput<V,S> p)
TransferResult<V,S>	visitStringConcatenateAssignment(StringConcatenateAssignmentNode n, TransferInput<V,S> in)
TransferResult<V,S>	visitStringConversion(StringConversionNode n, TransferInput<V,S> p)
TransferResult<V,S>	visitTernaryExpression(TernaryExpressionNode n, TransferInput<V,S> p)
TransferResult<V,S>	visitThisLiteral(ThisLiteralNode n, TransferInput<V,S> in)
TransferResult<V,S>	visitVariableDeclaration(VariableDeclarationNode n, TransferInput<V,S> p)
TransferResult<V,S>	visitWideningConversion(WideningConversionNode n, TransferInput<V,S> p)

Methods inherited from class org.checkerframework.dataflow.cfg.node.AbstractNodeVisitor

visitArrayCreation, visitArrayType, visitAssertionError, visitBitwiseAnd, visitBitwiseComplement, visitBitwiseOr, visitBitwiseXor, visitBooleanLiteral, visitCharacterLiteral, visitClassDeclaration, visitConditionalAnd, visitConditionalOr, visitDoubleLiteral, visitExplicitThisLiteral, visitFloatingDivision, visitFloatingRemainder, visitFloatLiteral, visitGreaterThan, visitGreaterThanOrEqual, visitImplicitThisLiteral, visitIntegerDivision, visitIntegerLiteral, visitIntegerRemainder, visitLeftShift, visitLessThan, visitLessThanOrEqual, visitLongLiteral, visitMarker, visitMemberReference, visitMethodAccess, visitNullChk, visitNullLiteral, visitNumericalAddition, visitNumericalMinus, visitNumericalMultiplication, visitNumericalPlus, visitNumericalSubtraction, visitPackageName, visitParameterizedType, visitPrimitiveType, visitShortLiteral, visitSignedRightShift, visitStringConcatenate, visitStringLiteral, visitSuper, visitSynchronized, visitThrow, visitTypeCast, visitUnsignedRightShift, visitValueLiteral

Methods inherited from class java.lang.Object

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

Methods inherited from interface org.checkerframework.dataflow.cfg.node.NodeVisitor

visitArrayCreation, visitArrayType, visitAssertionError, visitBitwiseAnd, visitBitwiseComplement, visitBitwiseOr, visitBitwiseXor, visitBooleanLiteral, visitCharacterLiteral, visitClassDeclaration, visitConditionalAnd, visitConditionalOr, visitDoubleLiteral, visitExplicitThisLiteral, visitFloatingDivision, visitFloatingRemainder, visitFloatLiteral, visitGreaterThan, visitGreaterThanOrEqual, visitImplicitThisLiteral, visitIntegerDivision, visitIntegerLiteral, visitIntegerRemainder, visitLeftShift, visitLessThan, visitLessThanOrEqual, visitLongLiteral, visitMarker, visitMemberReference, visitMethodAccess, visitNullChk, visitNullLiteral, visitNumericalAddition, visitNumericalMinus, visitNumericalMultiplication, visitNumericalPlus, visitNumericalSubtraction, visitPackageName, visitParameterizedType, visitPrimitiveType, visitShortLiteral, visitSignedRightShift, visitStringConcatenate, visitStringLiteral, visitSuper, visitSynchronized, visitThrow, visitTypeCast, visitUnsignedRightShift

Field Detail

analysis

protected final CFAbstractAnalysis<V extends CFAbstractValue<V>,S extends CFAbstractStore<V,S>,T extends CFAbstractTransfer<V,S,T>> analysis

The analysis class this store belongs to.

sequentialSemantics

protected final boolean sequentialSemantics

Should the analysis use sequential Java semantics (i.e., assume that only one thread is running at all times)?

Constructor Detail

CFAbstractTransfer

protected CFAbstractTransfer(CFAbstractAnalysis<V,S,T> analysis)

CFAbstractTransfer

protected CFAbstractTransfer(CFAbstractAnalysis<V,S,T> analysis,
                             boolean forceConcurrentSemantics)

Constructor that allows forcing concurrent semantics to be on for this instance of CFAbstractTransfer.

Parameters:

forceConcurrentSemantics - whether concurrent semantics should be forced to be on. If false, concurrent semantics are turned off by default, but the user can still turn them on via -AconcurrentSemantics. If true, the user cannot turn off concurrent semantics.

Method Detail

usesSequentialSemantics

public boolean usesSequentialSemantics()

Returns true if the transfer function uses sequential semantics, false if it uses concurrent semantics. Useful when creating an empty store, since a store makes different decisions depending on whether sequential or concurrent semantics are used.

Returns:

true if the transfer function uses sequential semantics, false if it uses concurrent semantics

finishValue

protected V finishValue(V value,
                        S store)

This method is called before returning the abstract value value as the result of the transfer function. By default, the value is not changed but subclasses might decide to implement some functionality. The store at this position is also passed.

finishValue

protected V finishValue(V value,
                        S thenStore,
                        S elseStore)

This method is called before returning the abstract value value as the result of the transfer function. By default, the value is not changed but subclasses might decide to implement some functionality. The store at this position is also passed (two stores, as the result is a ConditionalTransferResult.

Parameters:

value - the value to finish

thenStore - the "then" store

elseStore - the "else" store

Returns:

the finished value

getValueFromFactory

protected V getValueFromFactory(Tree tree,
                                Node node)

Returns the abstract value of a non-leaf tree tree, as computed by the AnnotatedTypeFactory.

Returns:

the abstract value of a non-leaf tree tree, as computed by the AnnotatedTypeFactory

getValueWithSameAnnotations

protected V getValueWithSameAnnotations(TypeMirror type,
                                        V annotatedValue)

Returns an abstract value with the given type and the annotations from annotatedValue.

Returns:

an abstract value with the given type and the annotations from annotatedValue

setFixedInitialStore

public void setFixedInitialStore(S s)

Set a fixed initial Store.

initialStore

public S initialStore(UnderlyingAST underlyingAST,
                      @Nullable List<LocalVariableNode> parameters)

The initial store maps method formal parameters to their currently most refined type.

Specified by:

initialStore in interface ForwardTransferFunction<V extends CFAbstractValue<V>,S extends CFAbstractStore<V,S>>

Parameters:

underlyingAST - an abstract syntax tree

parameters - a list of local variable nodes

Returns:

the initial store

isNotFullyInitializedReceiver

protected boolean isNotFullyInitializedReceiver(MethodTree methodTree)

Returns true if the receiver of a method might not yet be fully initialized.

addInformationFromPreconditions

protected void addInformationFromPreconditions(S info,
                                               AnnotatedTypeFactory factory,
                                               UnderlyingAST.CFGMethod method,
                                               MethodTree methodTree,
                                               ExecutableElement methodElement)

Add the information from all the preconditions of the method method with corresponding tree methodTree to the store info.

visitNode

public TransferResult<V,S> visitNode(Node n,
                                     TransferInput<V,S> in)

The default visitor returns the input information unchanged, or in the case of conditional input information, merged.

Specified by:

visitNode in class AbstractNodeVisitor<TransferResult<V extends CFAbstractValue<V>,S extends CFAbstractStore<V,S>>,TransferInput<V extends CFAbstractValue<V>,S extends CFAbstractStore<V,S>>>

visitClassName

public TransferResult<V,S> visitClassName(ClassNameNode n,
                                          TransferInput<V,S> in)

Specified by:

visitClassName in interface NodeVisitor<TransferResult<V extends CFAbstractValue<V>,S extends CFAbstractStore<V,S>>,TransferInput<V extends CFAbstractValue<V>,S extends CFAbstractStore<V,S>>>

Overrides:

visitClassName in class AbstractNodeVisitor<TransferResult<V extends CFAbstractValue<V>,S extends CFAbstractStore<V,S>>,TransferInput<V extends CFAbstractValue<V>,S extends CFAbstractStore<V,S>>>

visitFieldAccess

public TransferResult<V,S> visitFieldAccess(FieldAccessNode n,
                                            TransferInput<V,S> p)

Specified by:

visitFieldAccess in interface NodeVisitor<TransferResult<V extends CFAbstractValue<V>,S extends CFAbstractStore<V,S>>,TransferInput<V extends CFAbstractValue<V>,S extends CFAbstractStore<V,S>>>

Overrides:

visitFieldAccess in class AbstractNodeVisitor<TransferResult<V extends CFAbstractValue<V>,S extends CFAbstractStore<V,S>>,TransferInput<V extends CFAbstractValue<V>,S extends CFAbstractStore<V,S>>>

visitArrayAccess

public TransferResult<V,S> visitArrayAccess(ArrayAccessNode n,
                                            TransferInput<V,S> p)

Specified by:

visitArrayAccess in interface NodeVisitor<TransferResult<V extends CFAbstractValue<V>,S extends CFAbstractStore<V,S>>,TransferInput<V extends CFAbstractValue<V>,S extends CFAbstractStore<V,S>>>

Overrides:

visitArrayAccess in class AbstractNodeVisitor<TransferResult<V extends CFAbstractValue<V>,S extends CFAbstractStore<V,S>>,TransferInput<V extends CFAbstractValue<V>,S extends CFAbstractStore<V,S>>>

visitLocalVariable

public TransferResult<V,S> visitLocalVariable(LocalVariableNode n,
                                              TransferInput<V,S> in)

Use the most specific type information available according to the store.

Specified by:

visitLocalVariable in interface NodeVisitor<TransferResult<V extends CFAbstractValue<V>,S extends CFAbstractStore<V,S>>,TransferInput<V extends CFAbstractValue<V>,S extends CFAbstractStore<V,S>>>

Overrides:

visitLocalVariable in class AbstractNodeVisitor<TransferResult<V extends CFAbstractValue<V>,S extends CFAbstractStore<V,S>>,TransferInput<V extends CFAbstractValue<V>,S extends CFAbstractStore<V,S>>>

visitThisLiteral

public TransferResult<V,S> visitThisLiteral(ThisLiteralNode n,
                                            TransferInput<V,S> in)

Overrides:

visitThisLiteral in class AbstractNodeVisitor<TransferResult<V extends CFAbstractValue<V>,S extends CFAbstractStore<V,S>>,TransferInput<V extends CFAbstractValue<V>,S extends CFAbstractStore<V,S>>>

visitTernaryExpression

public TransferResult<V,S> visitTernaryExpression(TernaryExpressionNode n,
                                                  TransferInput<V,S> p)

Specified by:

visitTernaryExpression in interface NodeVisitor<TransferResult<V extends CFAbstractValue<V>,S extends CFAbstractStore<V,S>>,TransferInput<V extends CFAbstractValue<V>,S extends CFAbstractStore<V,S>>>

Overrides:

visitTernaryExpression in class AbstractNodeVisitor<TransferResult<V extends CFAbstractValue<V>,S extends CFAbstractStore<V,S>>,TransferInput<V extends CFAbstractValue<V>,S extends CFAbstractStore<V,S>>>

visitConditionalNot

public TransferResult<V,S> visitConditionalNot(ConditionalNotNode n,
                                               TransferInput<V,S> p)

Reverse the role of the 'thenStore' and 'elseStore'.

Specified by:

visitConditionalNot in interface NodeVisitor<TransferResult<V extends CFAbstractValue<V>,S extends CFAbstractStore<V,S>>,TransferInput<V extends CFAbstractValue<V>,S extends CFAbstractStore<V,S>>>

Overrides:

visitConditionalNot in class AbstractNodeVisitor<TransferResult<V extends CFAbstractValue<V>,S extends CFAbstractStore<V,S>>,TransferInput<V extends CFAbstractValue<V>,S extends CFAbstractStore<V,S>>>

visitEqualTo

public TransferResult<V,S> visitEqualTo(EqualToNode n,
                                        TransferInput<V,S> p)

Specified by:

visitEqualTo in interface NodeVisitor<TransferResult<V extends CFAbstractValue<V>,S extends CFAbstractStore<V,S>>,TransferInput<V extends CFAbstractValue<V>,S extends CFAbstractStore<V,S>>>

Overrides:

visitEqualTo in class AbstractNodeVisitor<TransferResult<V extends CFAbstractValue<V>,S extends CFAbstractStore<V,S>>,TransferInput<V extends CFAbstractValue<V>,S extends CFAbstractStore<V,S>>>

visitNotEqual

public TransferResult<V,S> visitNotEqual(NotEqualNode n,
                                         TransferInput<V,S> p)

Specified by:

visitNotEqual in interface NodeVisitor<TransferResult<V extends CFAbstractValue<V>,S extends CFAbstractStore<V,S>>,TransferInput<V extends CFAbstractValue<V>,S extends CFAbstractStore<V,S>>>

Overrides:

visitNotEqual in class AbstractNodeVisitor<TransferResult<V extends CFAbstractValue<V>,S extends CFAbstractStore<V,S>>,TransferInput<V extends CFAbstractValue<V>,S extends CFAbstractStore<V,S>>>

strengthenAnnotationOfEqualTo

protected TransferResult<V,S> strengthenAnnotationOfEqualTo(TransferResult<V,S> res,
                                                            Node firstNode,
                                                            Node secondNode,
                                                            V firstValue,
                                                            V secondValue,
                                                            boolean notEqualTo)

Refine the annotation of secondNode if the annotation secondValue is less precise than firstValue. This is possible, if secondNode is an expression that is tracked by the store (e.g., a local variable or a field).

Note that when overriding this method, when a new type is inserted into the store, splitAssignments should be called, and the new type should be inserted into the store for each of the resulting nodes.

Parameters:

res - the previous result

notEqualTo - if true, indicates that the logic is flipped (i.e., the information is added to the elseStore instead of the thenStore) for a not-equal comparison.

Returns:

the conditional transfer result (if information has been added), or null.

splitAssignments

protected List<Node> splitAssignments(Node node)

Takes a node, and either returns the node itself again (as a singleton list), or if the node is an assignment node, returns the lhs and rhs (where splitAssignments is applied recursively to the rhs -- that is, the rhs may not appear in the result, but rather its lhs and rhs may).

visitAssignment

public TransferResult<V,S> visitAssignment(AssignmentNode n,
                                           TransferInput<V,S> in)

Specified by:

visitAssignment in interface NodeVisitor<TransferResult<V extends CFAbstractValue<V>,S extends CFAbstractStore<V,S>>,TransferInput<V extends CFAbstractValue<V>,S extends CFAbstractStore<V,S>>>

Overrides:

visitAssignment in class AbstractNodeVisitor<TransferResult<V extends CFAbstractValue<V>,S extends CFAbstractStore<V,S>>,TransferInput<V extends CFAbstractValue<V>,S extends CFAbstractStore<V,S>>>

visitReturn

public TransferResult<V,S> visitReturn(ReturnNode n,
                                       TransferInput<V,S> p)

Specified by:

visitReturn in interface NodeVisitor<TransferResult<V extends CFAbstractValue<V>,S extends CFAbstractStore<V,S>>,TransferInput<V extends CFAbstractValue<V>,S extends CFAbstractStore<V,S>>>

Overrides:

visitReturn in class AbstractNodeVisitor<TransferResult<V extends CFAbstractValue<V>,S extends CFAbstractStore<V,S>>,TransferInput<V extends CFAbstractValue<V>,S extends CFAbstractStore<V,S>>>

visitLambdaResultExpression

public TransferResult<V,S> visitLambdaResultExpression(LambdaResultExpressionNode n,
                                                       TransferInput<V,S> in)

Specified by:

visitLambdaResultExpression in interface NodeVisitor<TransferResult<V extends CFAbstractValue<V>,S extends CFAbstractStore<V,S>>,TransferInput<V extends CFAbstractValue<V>,S extends CFAbstractStore<V,S>>>

Overrides:

visitLambdaResultExpression in class AbstractNodeVisitor<TransferResult<V extends CFAbstractValue<V>,S extends CFAbstractStore<V,S>>,TransferInput<V extends CFAbstractValue<V>,S extends CFAbstractStore<V,S>>>

visitStringConcatenateAssignment

public TransferResult<V,S> visitStringConcatenateAssignment(StringConcatenateAssignmentNode n,
                                                            TransferInput<V,S> in)

Specified by:

visitStringConcatenateAssignment in interface NodeVisitor<TransferResult<V extends CFAbstractValue<V>,S extends CFAbstractStore<V,S>>,TransferInput<V extends CFAbstractValue<V>,S extends CFAbstractStore<V,S>>>

Overrides:

visitStringConcatenateAssignment in class AbstractNodeVisitor<TransferResult<V extends CFAbstractValue<V>,S extends CFAbstractStore<V,S>>,TransferInput<V extends CFAbstractValue<V>,S extends CFAbstractStore<V,S>>>

processCommonAssignment

protected void processCommonAssignment(TransferInput<V,S> in,
                                       Node lhs,
                                       Node rhs,
                                       S info,
                                       V rhsValue)

Determine abstract value of right-hand side and update the store accordingly to the assignment.

visitObjectCreation

public TransferResult<V,S> visitObjectCreation(ObjectCreationNode n,
                                               TransferInput<V,S> p)

Specified by:

visitObjectCreation in interface NodeVisitor<TransferResult<V extends CFAbstractValue<V>,S extends CFAbstractStore<V,S>>,TransferInput<V extends CFAbstractValue<V>,S extends CFAbstractStore<V,S>>>

Overrides:

visitObjectCreation in class AbstractNodeVisitor<TransferResult<V extends CFAbstractValue<V>,S extends CFAbstractStore<V,S>>,TransferInput<V extends CFAbstractValue<V>,S extends CFAbstractStore<V,S>>>

visitMethodInvocation

public TransferResult<V,S> visitMethodInvocation(MethodInvocationNode n,
                                                 TransferInput<V,S> in)

Specified by:

visitMethodInvocation in interface NodeVisitor<TransferResult<V extends CFAbstractValue<V>,S extends CFAbstractStore<V,S>>,TransferInput<V extends CFAbstractValue<V>,S extends CFAbstractStore<V,S>>>

Overrides:

visitMethodInvocation in class AbstractNodeVisitor<TransferResult<V extends CFAbstractValue<V>,S extends CFAbstractStore<V,S>>,TransferInput<V extends CFAbstractValue<V>,S extends CFAbstractStore<V,S>>>

visitInstanceOf

public TransferResult<V,S> visitInstanceOf(InstanceOfNode node,
                                           TransferInput<V,S> in)

Specified by:

visitInstanceOf in interface NodeVisitor<TransferResult<V extends CFAbstractValue<V>,S extends CFAbstractStore<V,S>>,TransferInput<V extends CFAbstractValue<V>,S extends CFAbstractStore<V,S>>>

Overrides:

visitInstanceOf in class AbstractNodeVisitor<TransferResult<V extends CFAbstractValue<V>,S extends CFAbstractStore<V,S>>,TransferInput<V extends CFAbstractValue<V>,S extends CFAbstractStore<V,S>>>

processPostconditions

protected void processPostconditions(MethodInvocationNode n,
                                     S store,
                                     ExecutableElement methodElement,
                                     Tree tree)

Add information based on all postconditions of method n with tree tree and element method to the store store.

processConditionalPostconditions

protected void processConditionalPostconditions(MethodInvocationNode n,
                                                ExecutableElement methodElement,
                                                Tree tree,
                                                S thenStore,
                                                S elseStore)

Add information based on all conditional postconditions of method n with tree tree and element method to the appropriate store.

visitCase

public TransferResult<V,S> visitCase(CaseNode n,
                                     TransferInput<V,S> in)

A case produces no value, but it may imply some facts about the argument to the switch statement.

Specified by:

visitCase in interface NodeVisitor<TransferResult<V extends CFAbstractValue<V>,S extends CFAbstractStore<V,S>>,TransferInput<V extends CFAbstractValue<V>,S extends CFAbstractStore<V,S>>>

Overrides:

visitCase in class AbstractNodeVisitor<TransferResult<V extends CFAbstractValue<V>,S extends CFAbstractStore<V,S>>,TransferInput<V extends CFAbstractValue<V>,S extends CFAbstractStore<V,S>>>

moreSpecificValue

public V moreSpecificValue(V value1,
                           V value2)

Returns the abstract value of (value1, value2) that is more specific. If the two are incomparable, then value1 is returned.

visitVariableDeclaration

public TransferResult<V,S> visitVariableDeclaration(VariableDeclarationNode n,
                                                    TransferInput<V,S> p)

Specified by:

visitVariableDeclaration in interface NodeVisitor<TransferResult<V extends CFAbstractValue<V>,S extends CFAbstractStore<V,S>>,TransferInput<V extends CFAbstractValue<V>,S extends CFAbstractStore<V,S>>>

Overrides:

visitVariableDeclaration in class AbstractNodeVisitor<TransferResult<V extends CFAbstractValue<V>,S extends CFAbstractStore<V,S>>,TransferInput<V extends CFAbstractValue<V>,S extends CFAbstractStore<V,S>>>

visitNarrowingConversion

public TransferResult<V,S> visitNarrowingConversion(NarrowingConversionNode n,
                                                    TransferInput<V,S> p)

Specified by:

visitNarrowingConversion in interface NodeVisitor<TransferResult<V extends CFAbstractValue<V>,S extends CFAbstractStore<V,S>>,TransferInput<V extends CFAbstractValue<V>,S extends CFAbstractStore<V,S>>>

Overrides:

visitNarrowingConversion in class AbstractNodeVisitor<TransferResult<V extends CFAbstractValue<V>,S extends CFAbstractStore<V,S>>,TransferInput<V extends CFAbstractValue<V>,S extends CFAbstractStore<V,S>>>

visitWideningConversion

public TransferResult<V,S> visitWideningConversion(WideningConversionNode n,
                                                   TransferInput<V,S> p)

Specified by:

visitWideningConversion in interface NodeVisitor<TransferResult<V extends CFAbstractValue<V>,S extends CFAbstractStore<V,S>>,TransferInput<V extends CFAbstractValue<V>,S extends CFAbstractStore<V,S>>>

Overrides:

visitWideningConversion in class AbstractNodeVisitor<TransferResult<V extends CFAbstractValue<V>,S extends CFAbstractStore<V,S>>,TransferInput<V extends CFAbstractValue<V>,S extends CFAbstractStore<V,S>>>

visitStringConversion

public TransferResult<V,S> visitStringConversion(StringConversionNode n,
                                                 TransferInput<V,S> p)

Specified by:

visitStringConversion in interface NodeVisitor<TransferResult<V extends CFAbstractValue<V>,S extends CFAbstractStore<V,S>>,TransferInput<V extends CFAbstractValue<V>,S extends CFAbstractStore<V,S>>>

Overrides:

visitStringConversion in class AbstractNodeVisitor<TransferResult<V extends CFAbstractValue<V>,S extends CFAbstractStore<V,S>>,TransferInput<V extends CFAbstractValue<V>,S extends CFAbstractStore<V,S>>>