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.

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, TARGET, targetValueElement, typeValidator, visitorState

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

elements, root, trees, treesWithSuppressWarnings, types

Constructor Summary

Constructors

Constructor and Description
InitializationVisitor(BaseTypeChecker checker)

Method Summary

Modifier and Type	Method and Description
protected void	checkConstructorInvocation(AnnotatedTypeMirror.AnnotatedDeclaredType dt, AnnotatedTypeMirror.AnnotatedExecutableType constructor, com.sun.source.tree.NewClassTree src) Check that the (explicit) annotations on a new class tree are comparable to the result type of the constructor.
protected void	checkConstructorResult(AnnotatedTypeMirror.AnnotatedExecutableType constructorType, javax.lang.model.element.ExecutableElement constructorElement) Issue a warning if the result type of the constructor is not top.
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	checkThisOrSuperConstructorCall(com.sun.source.tree.MethodInvocationTree superCall, @CompilerMessageKey java.lang.String errorKey) Checks that the following rule is satisfied: The type on a constructor declaration must be a supertype of the return type of "this()" or "super()" invocation within that constructor.
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) Set the CompilationUnitTree to be used during any visits.
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, checkConditionalPostcondition, checkDefaultConstructor, checkExceptionParameter, checkExtendsImplements, checkFieldInvariantDeclarations, checkForAnnotatedJdk, checkMethodInvocability, checkMethodReferenceAsOverride, checkOverride, checkOverride, checkPostcondition, checkPreconditions, checkSuperConstructorCall, checkThisConstructorCall, checkThrownExpression, checkTypeArguments, checkTypecastRedundancy, checkTypecastSafety, checkVarargs, commonAssignmentCheck, commonAssignmentCheck, commonAssignmentCheckEndDiagnostic, commonAssignmentCheckStartDiagnostic, createOverrideChecker, createTypeFactory, createTypeValidator, enclosingMemberSelect, enclosingStatement, getExceptionParameterLowerBoundAnnotations, getThrowUpperBoundAnnotations, getTypeFactory, isAccessAllowed, isTypeCastSafe, isValidUse, isValidUse, isValidUse, reportPurityErrors, scan, shouldSkipUses, skipReceiverSubtypeCheck, testTypevarContainment, typeCheckVectorCopyIntoArgument, validateType, validateTypeOf, visitAnnotation, visitArrayAccess, visitAssignment, visitCatch, visitClass, visitCompilationUnit, visitCompoundAssignment, visitConditionalExpression, visitEnhancedForLoop, visitIdentifier, visitInstanceOf, visitLambdaExpression, visitMemberReference, visitMethodInvocation, visitNewArray, visitNewClass, visitReturn, visitThrow, 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, visitBlock, visitBreak, visitCase, visitContinue, visitDoWhileLoop, visitEmptyStatement, visitErroneous, visitExports, visitExpressionStatement, visitForLoop, visitIf, visitImport, visitIntersectionType, visitLabeledStatement, visitLiteral, visitMemberSelect, visitModifiers, visitModule, visitOpens, visitOther, visitPackage, visitParameterizedType, visitParenthesized, visitPrimitiveType, visitProvides, visitRequires, visitSwitch, visitSynchronized, visitTry, visitUnionType, visitUses, 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)

Description copied from class: SourceVisitor

Set the CompilationUnitTree to be used during any visits. For any later calls of com.sun.source.util.TreePathScanner.scan(TreePath, P), the CompilationUnitTree of the TreePath has to be equal to root.

Overrides:

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

checkConstructorInvocation

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

Description copied from class: BaseTypeVisitor

Check that the (explicit) annotations on a new class tree are comparable to the result type of the constructor. Issue an error if not.

Issue a warning if the annotations on the constructor invocation is a subtype of the constructor result type. This is equivalent to down-casting.

Overrides:

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

checkConstructorResult

protected void checkConstructorResult(AnnotatedTypeMirror.AnnotatedExecutableType constructorType,
                                      javax.lang.model.element.ExecutableElement constructorElement)

Description copied from class: BaseTypeVisitor

Issue a warning if the result type of the constructor is not top. If it is a supertype of the class, then a type.invalid.conflicting.annos error will also be issued by BaseTypeVisitor.isValidUse(AnnotatedTypeMirror.AnnotatedDeclaredType,AnnotatedTypeMirror.AnnotatedDeclaredType,Tree).

Overrides:

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

Parameters:

constructorType - AnnotatedExecutableType for the constructor

constructorElement - element that declares the constructor

checkThisOrSuperConstructorCall

protected void checkThisOrSuperConstructorCall(com.sun.source.tree.MethodInvocationTree superCall,
                                               @CompilerMessageKey java.lang.String errorKey)

Description copied from class: BaseTypeVisitor

Checks that the following rule is satisfied: The type on a constructor declaration must be a supertype of the return type of "this()" or "super()" invocation within that constructor.

Overrides:

checkThisOrSuperConstructorCall 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,?,?>>

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.