org.checkerframework.checker.initialization

Class InitializationVisitor<Factory extends InitializationAnnotatedTypeFactory<Value,Store,?,?>,Value extends CFAbstractValue<Value>,Store extends InitializationStore<Value,Store>>

java.lang.Object

com.sun.source.util.TreeScanner<R,P>

com.sun.source.util.TreePathScanner<R,P>

org.checkerframework.framework.source.SourceVisitor<java.lang.Void,java.lang.Void>

org.checkerframework.common.basetype.BaseTypeVisitor<Factory>

org.checkerframework.checker.initialization.InitializationVisitor<Factory,Value,Store>

All Implemented Interfaces:

com.sun.source.tree.TreeVisitor<java.lang.Void,java.lang.Void>

Direct Known Subclasses:

NullnessVisitor

public class InitializationVisitor<Factory extends InitializationAnnotatedTypeFactory<Value,Store,?,?>,Value extends CFAbstractValue<Value>,Store extends InitializationStore<Value,Store>>
extends BaseTypeVisitor<Factory>

The visitor for the freedom-before-commitment type-system. The freedom-before-commitment type-system and this class are abstract and need to be combined with another type-system whose safe initialization should be tracked. For an example, see the NullnessChecker. Also supports rawness as a type-system for tracking initialization, though FBC is preferred.

Author:

Stefan Heule

Nested Class Summary

Nested classes/interfaces inherited from class org.checkerframework.common.basetype.BaseTypeVisitor

BaseTypeVisitor.OverrideChecker

Field Summary

Fields

Modifier and Type	Field and Description
protected AnnotationFormatter	annoFormatter
protected java.util.List<com.sun.source.tree.VariableTree>	initializedFields

Fields inherited from class org.checkerframework.common.basetype.BaseTypeVisitor

atypeFactory, checker, contractsUtils, positions, typeValidator, visitorState

Fields inherited from class org.checkerframework.framework.source.SourceVisitor

elements, root, trees, types

Constructor Summary

Constructors

Constructor and Description
InitializationVisitor(BaseTypeChecker checker)

Method Summary

Modifier and Type	Method and Description
protected boolean	checkConstructorInvocation(AnnotatedTypeMirror.AnnotatedDeclaredType dt, AnnotatedTypeMirror.AnnotatedExecutableType constructor, com.sun.source.tree.NewClassTree src)
protected boolean	checkContract(FlowExpressions.Receiver expr, javax.lang.model.element.AnnotationMirror necessaryAnnotation, javax.lang.model.element.AnnotationMirror inferredAnnotation, CFAbstractStore<?,?> store) Returns true if and only if inferredAnnotation is valid for a given expression to match the necessaryAnnotation.
protected void	checkFieldsInitialized(com.sun.source.tree.Tree blockNode, boolean staticFields, Store store, java.util.List<? extends javax.lang.model.element.AnnotationMirror> receiverAnnotations) Checks that all fields (all static fields if staticFields is true) are initialized in the given store.
protected void	commonAssignmentCheck(com.sun.source.tree.Tree varTree, com.sun.source.tree.ExpressionTree valueExp, @CompilerMessageKey java.lang.String errorKey) Checks the validity of an assignment (or pseudo-assignment) from a value to a variable and emits an error message (through the compiler's messaging interface) if it is not valid.
void	processClassTree(com.sun.source.tree.ClassTree node) Type-check classTree.
void	setRoot(com.sun.source.tree.CompilationUnitTree root)
java.lang.Void	visitBlock(com.sun.source.tree.BlockTree node, java.lang.Void p)
java.lang.Void	visitMethod(com.sun.source.tree.MethodTree node, java.lang.Void p) Performs pseudo-assignment check: checks that the method obeys override and subtype rules to all overridden methods.
java.lang.Void	visitTypeCast(com.sun.source.tree.TypeCastTree node, java.lang.Void p)
java.lang.Void	visitVariable(com.sun.source.tree.VariableTree node, java.lang.Void p)

Methods inherited from class org.checkerframework.common.basetype.BaseTypeVisitor

checkAccess, checkArguments, checkArrayInitialization, checkAssignability, checkConditionalPostcondition, checkDefaultConstructor, checkExceptionParameter, checkFieldInvariantDeclarations, checkForAnnotatedJdk, checkMethodInvocability, checkMethodReferenceAsOverride, checkOverride, checkOverride, checkPostcondition, checkPreconditions, checkThrownExpression, checkTypeArguments, checkTypecastRedundancy, checkTypecastSafety, checkVarargs, commonAssignmentCheck, commonAssignmentCheck, createOverrideChecker, createTypeFactory, createTypeValidator, enclosingMemberSelect, enclosingStatement, getExceptionParameterLowerBoundAnnotations, getThrowUpperBoundAnnotations, getTypeFactory, isAccessAllowed, isAssignable, isValidUse, isValidUse, isValidUse, isVectorCopyInto, reportPurityErrors, scan, shouldSkipUses, skipReceiverSubtypeCheck, testTypevarContainment, typeCheckVectorCopyIntoArgument, validateType, validateTypeOf, visitAnnotation, visitArrayAccess, visitAssignment, visitCatch, visitClass, visitCompilationUnit, visitCompoundAssignment, visitConditionalExpression, visitEnhancedForLoop, visitIdentifier, visitInstanceOf, visitLambdaExpression, visitMemberReference, visitMethodInvocation, visitNewArray, visitNewClass, visitParameterizedType, visitReturn, visitThrow, visitTry, visitTypeParameter, visitUnary

Methods inherited from class org.checkerframework.framework.source.SourceVisitor

visit

Methods inherited from class com.sun.source.util.TreePathScanner

getCurrentPath, scan

Methods inherited from class com.sun.source.util.TreeScanner

reduce, scan, visitAnnotatedType, visitArrayType, visitAssert, visitBinary, visitBreak, visitCase, visitContinue, visitDoWhileLoop, visitEmptyStatement, visitErroneous, visitExpressionStatement, visitForLoop, visitIf, visitImport, visitIntersectionType, visitLabeledStatement, visitLiteral, visitMemberSelect, visitModifiers, visitOther, visitParenthesized, visitPrimitiveType, visitSwitch, visitSynchronized, visitUnionType, visitWhileLoop, visitWildcard

Methods inherited from class java.lang.Object

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

Field Detail

annoFormatter

protected final AnnotationFormatter annoFormatter

initializedFields

protected final java.util.List<com.sun.source.tree.VariableTree> initializedFields

Constructor Detail

InitializationVisitor

public InitializationVisitor(BaseTypeChecker checker)

Method Detail

setRoot

public void setRoot(com.sun.source.tree.CompilationUnitTree root)

Overrides:

setRoot in class BaseTypeVisitor<Factory extends InitializationAnnotatedTypeFactory<Value,Store,?,?>>

checkConstructorInvocation

protected boolean checkConstructorInvocation(AnnotatedTypeMirror.AnnotatedDeclaredType dt,
                                             AnnotatedTypeMirror.AnnotatedExecutableType constructor,
                                             com.sun.source.tree.NewClassTree src)

Overrides:

checkConstructorInvocation in class BaseTypeVisitor<Factory extends InitializationAnnotatedTypeFactory<Value,Store,?,?>>

commonAssignmentCheck

protected void commonAssignmentCheck(com.sun.source.tree.Tree varTree,
                                     com.sun.source.tree.ExpressionTree valueExp,
                                     @CompilerMessageKey java.lang.String errorKey)

Description copied from class: BaseTypeVisitor

Checks the validity of an assignment (or pseudo-assignment) from a value to a variable and emits an error message (through the compiler's messaging interface) if it is not valid.

Overrides:

commonAssignmentCheck in class BaseTypeVisitor<Factory extends InitializationAnnotatedTypeFactory<Value,Store,?,?>>

Parameters:

varTree - the AST node for the lvalue (usually a variable)

valueExp - the AST node for the rvalue (the new value)

errorKey - the error message to use if the check fails (must be a compiler message key, see CompilerMessageKey)

visitVariable

public java.lang.Void visitVariable(com.sun.source.tree.VariableTree node,
                                    java.lang.Void p)

Specified by:

visitVariable in interface com.sun.source.tree.TreeVisitor<java.lang.Void,java.lang.Void>

Overrides:

visitVariable in class BaseTypeVisitor<Factory extends InitializationAnnotatedTypeFactory<Value,Store,?,?>>

checkContract

protected boolean checkContract(FlowExpressions.Receiver expr,
                                javax.lang.model.element.AnnotationMirror necessaryAnnotation,
                                javax.lang.model.element.AnnotationMirror inferredAnnotation,
                                CFAbstractStore<?,?> store)

Description copied from class: BaseTypeVisitor

Returns true if and only if inferredAnnotation is valid for a given expression to match the necessaryAnnotation.

By default, inferredAnnotation must be a subtype of necessaryAnnotation, but subclasses might override this behavior.

Overrides:

checkContract in class BaseTypeVisitor<Factory extends InitializationAnnotatedTypeFactory<Value,Store,?,?>>

visitTypeCast

public java.lang.Void visitTypeCast(com.sun.source.tree.TypeCastTree node,
                                    java.lang.Void p)

Specified by:

visitTypeCast in interface com.sun.source.tree.TreeVisitor<java.lang.Void,java.lang.Void>

Overrides:

visitTypeCast in class BaseTypeVisitor<Factory extends InitializationAnnotatedTypeFactory<Value,Store,?,?>>

visitBlock

public java.lang.Void visitBlock(com.sun.source.tree.BlockTree node,
                                 java.lang.Void p)

Specified by:

visitBlock in interface com.sun.source.tree.TreeVisitor<java.lang.Void,java.lang.Void>

Overrides:

visitBlock in class com.sun.source.util.TreeScanner<java.lang.Void,java.lang.Void>

processClassTree

public void processClassTree(com.sun.source.tree.ClassTree node)

Description copied from class: BaseTypeVisitor

Type-check classTree. Subclasses should override this method instead of BaseTypeVisitor.visitClass(ClassTree, Void).

Overrides:

processClassTree in class BaseTypeVisitor<Factory extends InitializationAnnotatedTypeFactory<Value,Store,?,?>>

Parameters:

node - class to check

visitMethod

public java.lang.Void visitMethod(com.sun.source.tree.MethodTree node,
                                  java.lang.Void p)

Description copied from class: BaseTypeVisitor

Performs pseudo-assignment check: checks that the method obeys override and subtype rules to all overridden methods.

The override rule specifies that a method, m1, may override a method m2 only if:

• m1 return type is a subtype of m2
• m1 receiver type is a supertype of m2
• m1 parameters are supertypes of corresponding m2 parameters

Also, it issues a "missing.this" error for static method annotated receivers.

Specified by:

visitMethod in interface com.sun.source.tree.TreeVisitor<java.lang.Void,java.lang.Void>

Overrides:

visitMethod in class BaseTypeVisitor<Factory extends InitializationAnnotatedTypeFactory<Value,Store,?,?>>

checkFieldsInitialized

protected void checkFieldsInitialized(com.sun.source.tree.Tree blockNode,
                                      boolean staticFields,
                                      Store store,
                                      java.util.List<? extends javax.lang.model.element.AnnotationMirror> receiverAnnotations)

Checks that all fields (all static fields if staticFields is true) are initialized in the given store.