Package 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:
ForwardTransferFunction<V,S>, 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 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 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 CFAbstractStore.insertValue(JavaExpression, CFAbstractValue)).
  3. All non-null fields with an initializer can be considered initialized (this is done in CFAbstractStore.insertValue(JavaExpression, CFAbstractValue)).
  4. After the call to a super constructor ("super()" call), all non-null fields of the super class can safely be considered initialized.
See Also: