Package org.checkerframework.checker.initialization

Class InitializationTransfer

java.lang.Object

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

org.checkerframework.framework.flow.CFAbstractTransfer<CFValue,InitializationStore,InitializationTransfer>

org.checkerframework.checker.initialization.InitializationTransfer

All Implemented Interfaces:

ForwardTransferFunction<CFValue,InitializationStore>, TransferFunction<CFValue,InitializationStore>, NodeVisitor<TransferResult<CFValue,InitializationStore>,TransferInput<CFValue,InitializationStore>>

public class InitializationTransfer
extends CFAbstractTransfer<CFValue,InitializationStore,InitializationTransfer>

A transfer function that extends CFAbstractTransfer and tracks InitializationStores. In addition to the features of CFAbstractTransfer, this transfer function also tracks which fields of the current class ('self' receiver) have been initialized.

More precisely, the following refinements are performed:

1. After the call to a constructor ("this()" call), all fields of the current class can safely be considered initialized.
2. After the call to a super constructor ("super()" call), all fields of the super class can safely be considered initialized.

Field Summary

Fields

Modifier and Type	Field	Description
protected InitializationParentAnnotatedTypeFactory	atypeFactory	The initialization type factory

Fields inherited from class org.checkerframework.framework.flow.CFAbstractTransfer

analysis, sequentialSemantics

Constructor Summary

Constructors

Constructor	Description
InitializationTransfer(InitializationAnalysis analysis)	Create a new InitializationTransfer for the given analysis.

Method Summary

Modifier and Type	Method	Description
protected java.util.List<javax.lang.model.element.VariableElement>	initializedFieldsAfterCall(MethodInvocationNode node)	Returns the fields that can safely be considered initialized after the method call node.
protected void	markFieldsAsInitialized(java.util.List<javax.lang.model.element.VariableElement> result, javax.lang.model.element.TypeElement clazzElem)	Adds all the fields of the class clazzElem to the list of initialized fields result.
TransferResult<CFValue,InitializationStore>	visitAssignment(AssignmentNode n, TransferInput<CFValue,InitializationStore> in)
TransferResult<CFValue,InitializationStore>	visitMethodInvocation(MethodInvocationNode n, TransferInput<CFValue,InitializationStore> in)

Methods inherited from class org.checkerframework.framework.flow.CFAbstractTransfer

addInformationFromPreconditions, createTransferResult, finishValue, finishValue, getNarrowedValue, getValueFromFactory, getWidenedValue, initialStore, insertIntoStores, isNotFullyInitializedReceiver, moreSpecificValue, processCommonAssignment, processConditionalPostconditions, processPostconditions, recreateTransferResult, setFixedInitialStore, splitAssignments, strengthenAnnotationOfEqualTo, usesSequentialSemantics, visitArrayAccess, visitCase, visitClassName, visitConditionalNot, visitDeconstructorPattern, visitEqualTo, visitExpressionStatement, visitFieldAccess, visitInstanceOf, visitLambdaResultExpression, visitLocalVariable, visitNarrowingConversion, visitNode, visitNotEqual, visitObjectCreation, visitReturn, visitStringConversion, visitSwitchExpressionNode, visitTernaryExpression, visitThis, visitVariableDeclaration, visitWideningConversion

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 Detail

atypeFactory

protected final InitializationParentAnnotatedTypeFactory atypeFactory

The initialization type factory

Constructor Detail

InitializationTransfer

public InitializationTransfer(InitializationAnalysis analysis)

Create a new InitializationTransfer for the given analysis.

Parameters:

analysis - init analysi.s

Method Detail

initializedFieldsAfterCall

protected java.util.List<javax.lang.model.element.VariableElement> initializedFieldsAfterCall(MethodInvocationNode node)

Returns the fields that can safely be considered initialized after the method call node.

Parameters:

node - a method call

Returns:

the fields that are initialized after the method call

markFieldsAsInitialized

protected void markFieldsAsInitialized(java.util.List<javax.lang.model.element.VariableElement> result,
                                       javax.lang.model.element.TypeElement clazzElem)

Adds all the fields of the class clazzElem to the list of initialized fields result.

Parameters:

result - the list of initialized fields

clazzElem - the class whose fields to add

visitAssignment

public TransferResult<CFValue,InitializationStore> visitAssignment(AssignmentNode n,
                                                                         TransferInput<CFValue,InitializationStore> in)

Specified by:

visitAssignment in interface NodeVisitor<TransferResult<CFValue,InitializationStore>,TransferInput<CFValue,InitializationStore>>

Overrides:

visitAssignment in class CFAbstractTransfer<CFValue,InitializationStore,InitializationTransfer>

visitMethodInvocation

public TransferResult<CFValue,InitializationStore> visitMethodInvocation(MethodInvocationNode n,
                                                                               TransferInput<CFValue,InitializationStore> in)

Specified by:

visitMethodInvocation in interface NodeVisitor<TransferResult<CFValue,InitializationStore>,TransferInput<CFValue,InitializationStore>>

Overrides:

visitMethodInvocation in class CFAbstractTransfer<CFValue,InitializationStore,InitializationTransfer>