Package 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	Description
protected final CFAbstractAnalysis<V,S,T>	analysis	The analysis used by this transfer function.
protected final 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	Description
protected	CFAbstractTransfer(CFAbstractAnalysis<V,S,T> analysis)	Create a CFAbstractTransfer.
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	Description
protected void	addInformationFromPreconditions(S initialStore, AnnotatedTypeFactory factory, UnderlyingAST.CFGMethod methodAst, MethodTree methodDeclTree, ExecutableElement methodElement)	Add the information from all the preconditions of a method to the initial store in the method body.
protected TransferResult<V,S>	createTransferResult(@Nullable V value, TransferInput<V,S> in)	Creates a TransferResult.
protected @Nullable V	finishValue(@Nullable V value, S store)	A hook for subclasses to modify the result of the transfer function.
protected @Nullable V	finishValue(@Nullable V value, S thenStore, S elseStore)	A hook for subclasses to modify the result of the transfer function.
protected V	getNarrowedValue(TypeMirror type, V annotatedValue)	Returns an abstract value with the given type and the annotations from annotatedValue, adapted for narrowing.
protected V	getValueFromFactory(Tree tree, Node node)	Returns the abstract value of a non-leaf tree tree, as computed by the AnnotatedTypeFactory.
protected V	getWidenedValue(TypeMirror type, V annotatedValue)	Returns an abstract value with the given type and the annotations from annotatedValue, adapted for widening.
S	initialStore(UnderlyingAST underlyingAST, List<LocalVariableNode> parameters)	The initial store maps method formal parameters to their currently most refined type.
static void	insertIntoStores(TransferResult<CFValue,CFStore> result, JavaExpression target, AnnotationMirror newAnno)	Inserts newAnno as the value into all stores (conditional or not) in the result for node.
protected boolean	isNotFullyInitializedReceiver(MethodTree methodDeclTree)	Returns true if the receiver of a method or constructor 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 store, V rhsValue)	Determine abstract value of right-hand side and update the store accordingly.
protected void	processConditionalPostconditions(MethodInvocationNode invocationNode, ExecutableElement methodElement, ExpressionTree invocationTree, S thenStore, S elseStore)	Add information from the conditional postconditions of a method to the stores after an invocation.
protected void	processPostconditions(Node invocationNode, S store, ExecutableElement executableElement, ExpressionTree invocationTree)	Add information from the postconditions of a method to the store after an invocation.
protected TransferResult<V,S>	recreateTransferResult(@Nullable V value, TransferResult<V,S> in)	Creates a TransferResult just like the given one, but with the given value.
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, it is possible that the rhs does not appear in the result, but rather its lhs and rhs do).
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 switch selector expression.
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>	visitSwitchExpressionNode(SwitchExpressionNode n, TransferInput<V,S> vsTransferInput)
TransferResult<V,S>	visitTernaryExpression(TernaryExpressionNode n, TransferInput<V,S> p)
TransferResult<V,S>	visitThis(ThisNode 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, visitExplicitThis, visitFloatingDivision, visitFloatingRemainder, visitFloatLiteral, visitGreaterThan, visitGreaterThanOrEqual, visitImplicitThis, 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, visitExplicitThis, visitFloatingDivision, visitFloatingRemainder, visitFloatLiteral, visitGreaterThan, visitGreaterThanOrEqual, visitImplicitThis, 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 Details

analysis

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

The analysis used by this transfer function.

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 Details

CFAbstractTransfer

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

Create a CFAbstractTransfer.

Parameters:

analysis - the analysis used by this transfer function

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:

analysis - the analysis used by this transfer function

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 Details

usesSequentialSemantics

@Pure
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

@SideEffectFree
protected @Nullable V finishValue(@Nullable V value,
 S store)

A hook for subclasses to modify the result of the transfer function. This method is called before returning the abstract value value as the result of the transfer function.

If a subclass overrides this method, the subclass should also override finishValue(CFAbstractValue,CFAbstractStore,CFAbstractStore).

Parameters:

value - a value to possibly modify

store - the store

Returns:

the possibly-modified value

finishValue

@SideEffectFree
protected @Nullable V finishValue(@Nullable V value,
 S thenStore,
 S elseStore)

A hook for subclasses to modify the result of the transfer function. This method is called before returning the abstract value value as the result of the transfer function.

If a subclass overrides this method, the subclass should also override finishValue(CFAbstractValue,CFAbstractStore).

Parameters:

value - the value to finish

thenStore - the "then" store

elseStore - the "else" store

Returns:

the possibly-modified 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

setFixedInitialStore

public void setFixedInitialStore(S s)

Set a fixed initial Store.

initialStore

public S initialStore(UnderlyingAST underlyingAST,
 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 representing formal parameters (if any)

Returns:

the initial store

isNotFullyInitializedReceiver

protected boolean isNotFullyInitializedReceiver(MethodTree methodDeclTree)

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

Parameters:

methodDeclTree - the declaration of the method or constructor

Returns:

true if the receiver of a method or constructor might not yet be fully initialized

addInformationFromPreconditions

protected void addInformationFromPreconditions(S initialStore,
 AnnotatedTypeFactory factory,
 UnderlyingAST.CFGMethod methodAst,
 MethodTree methodDeclTree,
 ExecutableElement methodElement)

Add the information from all the preconditions of a method to the initial store in the method body.

Parameters:

initialStore - the initial store for the method body

factory - the type factory

methodAst - the AST for a method declaration

methodDeclTree - the declaration of the method; is a field of methodAst

methodElement - the element for the method

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

createTransferResult

protected TransferResult<V,S> createTransferResult(@Nullable V value,
 TransferInput<V,S> in)

Creates a TransferResult.

This default implementation returns the input information unchanged, or in the case of conditional input information, merged.

Parameters:

value - the value; possibly null

in - the transfer input

Returns:

the input information, as a TransferResult

recreateTransferResult

protected TransferResult<V,S> recreateTransferResult(@Nullable V value,
 TransferResult<V,S> in)

Creates a TransferResult just like the given one, but with the given value.

This default implementation returns the input information unchanged, or in the case of conditional input information, merged.

Parameters:

value - the value; possibly null

in - the TransferResult to copy

Returns:

the input informatio

visitClassName

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

Specified by:

visitClassName in interface NodeVisitor<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<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<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<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>>>

visitThis

public TransferResult<V,S> visitThis(ThisNode n,
 TransferInput<V,S> in)

Overrides:

visitThis 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<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>>>

visitSwitchExpressionNode

public TransferResult<V,S> visitSwitchExpressionNode(SwitchExpressionNode n,
 TransferInput<V,S> vsTransferInput)

Specified by:

visitSwitchExpressionNode in interface NodeVisitor<V extends CFAbstractValue<V>,S extends CFAbstractStore<V,S>>

Overrides:

visitSwitchExpressionNode 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<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<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<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). Clients usually call this twice with firstNode and secondNode reversed, to refine each of them.

Note that when overriding this method, when a new type is inserted into the store, splitAssignments(org.checkerframework.dataflow.cfg.node.Node) should be called, and the new type should be inserted into the store for each of the resulting nodes.

Parameters:

firstNode - the node that might be more precise

secondNode - the node whose type to possibly refine

firstValue - the abstract value that might be more precise

secondValue - the abstract value that might be less precise

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, it is possible that the rhs does not appear in the result, but rather its lhs and rhs do).

Parameters:

node - possibly an assignment node

Returns:

a list containing all the right- and left-hand sides in the given assignment node; it contains just the node itself if it is not an assignment)

visitAssignment

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

Specified by:

visitAssignment in interface NodeVisitor<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<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<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<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 store,
 V rhsValue)

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

Parameters:

in - the store(s) before the assignment

lhs - the left-hand side of the assignment

rhs - the right-hand side of the assignment

store - the regular input store (from in)

rhsValue - the value of the right-hand side of the assignment

visitObjectCreation

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

Specified by:

visitObjectCreation in interface NodeVisitor<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<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<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(Node invocationNode,
 S store,
 ExecutableElement executableElement,
 ExpressionTree invocationTree)

Add information from the postconditions of a method to the store after an invocation.

Parameters:

invocationNode - a method call or an object creation

store - a store; is side-effected by this method

executableElement - the method or constructor being called

invocationTree - the tree for the method call or the object creation

processConditionalPostconditions

protected void processConditionalPostconditions(MethodInvocationNode invocationNode,
 ExecutableElement methodElement,
 ExpressionTree invocationTree,
 S thenStore,
 S elseStore)

Add information from the conditional postconditions of a method to the stores after an invocation.

Parameters:

invocationNode - a method call

methodElement - the method being called

invocationTree - the tree for the method call

thenStore - the "then" store; is side-effected by this method

elseStore - the "else" store; is side-effected by this method

visitCase

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

A case produces no value, but it may imply some facts about switch selector expression.

Specified by:

visitCase in interface NodeVisitor<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<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>>>

visitWideningConversion

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

Specified by:

visitWideningConversion in interface NodeVisitor<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>>>

getNarrowedValue

protected V getNarrowedValue(TypeMirror type,
 V annotatedValue)

Returns an abstract value with the given type and the annotations from annotatedValue, adapted for narrowing. This is only called at a narrowing conversion.

Parameters:

type - the type to narrow to

annotatedValue - the type to narrow from

Returns:

an abstract value with the given type and the annotations from annotatedValue; returns null if annotatedValue is null

getWidenedValue

protected V getWidenedValue(TypeMirror type,
 V annotatedValue)

Returns an abstract value with the given type and the annotations from annotatedValue, adapted for widening. This is only called at a widening conversion.

Parameters:

type - the type to widen to

annotatedValue - the type to widen from

Returns:

an abstract value with the given type and the annotations from annotatedValue; returns null if annotatedValue is null

visitNarrowingConversion

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

Specified by:

visitNarrowingConversion in interface NodeVisitor<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>>>

visitStringConversion

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

Specified by:

visitStringConversion in interface NodeVisitor<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>>>

insertIntoStores

public static void insertIntoStores(TransferResult<CFValue,CFStore> result,
 JavaExpression target,
 AnnotationMirror newAnno)

Inserts newAnno as the value into all stores (conditional or not) in the result for node. This is a utility method for subclasses.

Parameters:

result - the TransferResult holding the stores to modify

target - the receiver whose value should be modified

newAnno - the new value