org.checkerframework.checker.initialization

Class InitializationTransfer<V extends CFAbstractValue<V>,T extends InitializationTransfer<V,T,S>,S extends InitializationStore<V,S>>

java.lang.Object

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

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

org.checkerframework.checker.initialization.InitializationTransfer<V,T,S>

Type Parameters:

T - the type of the transfer function

All Implemented Interfaces:

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

Direct Known Subclasses:

NullnessTransfer

public class InitializationTransfer<V extends CFAbstractValue<V>,T extends InitializationTransfer<V,T,S>,S extends InitializationStore<V,S>>
extends CFAbstractTransfer<V,S,T>

A transfer function that extends CFAbstractTransfer and tracks InitializationStores. In addition to the features of CFAbstractTransfer, this transfer function also track 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 non-null fields of the current class can safely be considered initialized.
2. After a method call with a postcondition that ensures a field to be non-null, that field can safely be considered initialized (this is done in InitializationStore.insertValue(FlowExpressions.Receiver, CFAbstractValue)).
3. All non-null fields with an initializer can be considered initialized (this is done in InitializationStore.insertValue(FlowExpressions.Receiver, CFAbstractValue)).
4. After the call to a super constructor ("super()" call), all non-null fields of the super class can safely be considered initialized.

Author:

Stefan Heule

See Also:

InitializationStore

Field Summary

Fields

Modifier and Type	Field and Description
protected InitializationAnnotatedTypeFactory<?,?,?,?>	atypeFactory

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

analysis, sequentialSemantics

Constructor Summary

Constructors

Constructor and Description
InitializationTransfer(CFAbstractAnalysis<V,S,T> analysis)

Method Summary

Modifier and Type	Method and Description
protected List<VariableElement>	initializedFieldsAfterCall(MethodInvocationNode node, ConditionalTransferResult<V,S> transferResult) Returns the fields that can safely be considered initialized after the method call node.
protected boolean	isNotFullyInitializedReceiver(MethodTree methodTree) Returns true if the receiver of a method might not yet be fully initialized.
protected void	markInvariantFieldsAsInitialized(List<VariableElement> result, TypeElement clazzElem) Adds all the fields of the class clazzElem that have the 'invariant annotation' to the set of initialized fields result.
TransferResult<V,S>	visitAssignment(AssignmentNode n, TransferInput<V,S> in)
TransferResult<V,S>	visitFieldAccess(FieldAccessNode n, TransferInput<V,S> p) If an invariant field is initialized and has the invariant annotation, than it has at least the invariant annotation.
TransferResult<V,S>	visitMethodInvocation(MethodInvocationNode n, TransferInput<V,S> in)

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

addInformationFromPreconditions, finishValue, finishValue, getTypeFactoryOfSubchecker, getValueFromFactory, getValueWithSameAnnotations, initialStore, moreSpecificValue, processCommonAssignment, processConditionalPostconditions, processPostconditions, setFixedInitialStore, splitAssignments, strengthenAnnotationOfEqualTo, usesSequentialSemantics, visitArrayAccess, visitCase, visitClassName, visitConditionalNot, visitEqualTo, visitLocalVariable, visitNarrowingConversion, visitNode, visitNotEqual, visitObjectCreation, visitReturn, visitStringConcatenateAssignment, visitStringConversion, visitTernaryExpression, visitThisLiteral, visitVariableDeclaration, visitWideningConversion

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

visitArrayCreation, visitArrayType, visitAssertionError, visitBitwiseAnd, visitBitwiseComplement, visitBitwiseOr, visitBitwiseXor, visitBooleanLiteral, visitCharacterLiteral, visitConditionalAnd, visitConditionalOr, visitDoubleLiteral, visitExplicitThisLiteral, visitFloatingDivision, visitFloatingRemainder, visitFloatLiteral, visitGreaterThan, visitGreaterThanOrEqual, visitImplicitThisLiteral, visitInstanceOf, 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, visitConditionalAnd, visitConditionalOr, visitDoubleLiteral, visitExplicitThisLiteral, visitFloatingDivision, visitFloatingRemainder, visitFloatLiteral, visitGreaterThan, visitGreaterThanOrEqual, visitImplicitThisLiteral, visitInstanceOf, 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 InitializationAnnotatedTypeFactory<?,?,?,?> atypeFactory

Constructor Detail

InitializationTransfer

public InitializationTransfer(CFAbstractAnalysis<V,S,T> analysis)

Method Detail

isNotFullyInitializedReceiver

protected boolean isNotFullyInitializedReceiver(MethodTree methodTree)

Description copied from class: CFAbstractTransfer

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

Overrides:

isNotFullyInitializedReceiver in class CFAbstractTransfer<V extends CFAbstractValue<V>,S extends InitializationStore<V,S>,T extends InitializationTransfer<V,T,S>>

initializedFieldsAfterCall

protected List<VariableElement> initializedFieldsAfterCall(MethodInvocationNode node,
                                                           ConditionalTransferResult<V,S> transferResult)

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

markInvariantFieldsAsInitialized

protected void markInvariantFieldsAsInitialized(List<VariableElement> result,
                                                TypeElement clazzElem)

Adds all the fields of the class clazzElem that have the 'invariant annotation' to the set of initialized fields result.

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 InitializationStore<V,S>>,TransferInput<V extends CFAbstractValue<V>,S extends InitializationStore<V,S>>>

Overrides:

visitAssignment in class CFAbstractTransfer<V extends CFAbstractValue<V>,S extends InitializationStore<V,S>,T extends InitializationTransfer<V,T,S>>

visitFieldAccess

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

If an invariant field is initialized and has the invariant annotation, than it has at least the invariant annotation. Note that only field of the 'this' receiver are tracked for initialization.

Specified by:

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

Overrides:

visitFieldAccess in class CFAbstractTransfer<V extends CFAbstractValue<V>,S extends InitializationStore<V,S>,T extends InitializationTransfer<V,T,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 InitializationStore<V,S>>,TransferInput<V extends CFAbstractValue<V>,S extends InitializationStore<V,S>>>

Overrides:

visitMethodInvocation in class CFAbstractTransfer<V extends CFAbstractValue<V>,S extends InitializationStore<V,S>,T extends InitializationTransfer<V,T,S>>