org.checkerframework.checker.initialization

Class InitializationVisitor<Factory extends InitializationAnnotatedTypeFactory<Value,Store,?,?>,Value extends org.checkerframework.framework.flow.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:

TreeVisitor<java.lang.Void,java.lang.Void>

Direct Known Subclasses:

NullnessVisitor

public class InitializationVisitor<Factory extends InitializationAnnotatedTypeFactory<Value,Store,?,?>,Value extends org.checkerframework.framework.flow.CFAbstractValue<Value>,Store extends InitializationStore<Value,Store>>
extends org.checkerframework.common.basetype.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.

Nested Class Summary

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

org.checkerframework.common.basetype.BaseTypeVisitor.OverrideChecker

Field Summary

Fields

Modifier and Type	Field and Description
protected org.checkerframework.framework.util.AnnotationFormatter	annoFormatter
protected java.util.List<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, treesWithSuppressWarnings, types

Constructor Summary

Constructors

Constructor and Description
InitializationVisitor(org.checkerframework.common.basetype.BaseTypeChecker checker)

Method Summary

Modifier and Type	Method and Description
protected boolean	checkConstructorInvocation(org.checkerframework.framework.type.AnnotatedTypeMirror.AnnotatedDeclaredType dt, org.checkerframework.framework.type.AnnotatedTypeMirror.AnnotatedExecutableType constructor, NewClassTree src)
protected boolean	checkContract(org.checkerframework.dataflow.analysis.FlowExpressions.Receiver expr, javax.lang.model.element.AnnotationMirror necessaryAnnotation, javax.lang.model.element.AnnotationMirror inferredAnnotation, org.checkerframework.framework.flow.CFAbstractStore<?,?> store)
protected void	checkFieldsInitialized(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(Tree varTree, ExpressionTree valueExp, @CompilerMessageKey java.lang.String errorKey)
void	processClassTree(ClassTree node)
void	setRoot(CompilationUnitTree root)
java.lang.Void	visitMethod(MethodTree node, java.lang.Void p)
java.lang.Void	visitTypeCast(TypeCastTree node, java.lang.Void p)
java.lang.Void	visitVariable(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, 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, visitExpressionStatement, visitForLoop, visitIf, visitImport, visitIntersectionType, visitLabeledStatement, visitLiteral, visitMemberSelect, visitModifiers, visitOther, visitParenthesized, visitPrimitiveType, visitSwitch, visitSynchronized, visitTry, 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 org.checkerframework.framework.util.AnnotationFormatter annoFormatter

initializedFields

protected final java.util.List<VariableTree> initializedFields

Constructor Detail

InitializationVisitor

public InitializationVisitor(org.checkerframework.common.basetype.BaseTypeChecker checker)

Method Detail

setRoot

public void setRoot(CompilationUnitTree root)

Overrides:

setRoot in class org.checkerframework.common.basetype.BaseTypeVisitor<Factory extends InitializationAnnotatedTypeFactory<Value,Store,?,?>>

checkConstructorInvocation

protected boolean checkConstructorInvocation(org.checkerframework.framework.type.AnnotatedTypeMirror.AnnotatedDeclaredType dt,
                                             org.checkerframework.framework.type.AnnotatedTypeMirror.AnnotatedExecutableType constructor,
                                             NewClassTree src)

Overrides:

checkConstructorInvocation in class org.checkerframework.common.basetype.BaseTypeVisitor<Factory extends InitializationAnnotatedTypeFactory<Value,Store,?,?>>

commonAssignmentCheck

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

Overrides:

commonAssignmentCheck in class org.checkerframework.common.basetype.BaseTypeVisitor<Factory extends InitializationAnnotatedTypeFactory<Value,Store,?,?>>

visitVariable

public java.lang.Void visitVariable(VariableTree node,
                                    java.lang.Void p)

Specified by:

visitVariable in interface TreeVisitor<java.lang.Void,java.lang.Void>

Overrides:

visitVariable in class org.checkerframework.common.basetype.BaseTypeVisitor<Factory extends InitializationAnnotatedTypeFactory<Value,Store,?,?>>

checkContract

protected boolean checkContract(org.checkerframework.dataflow.analysis.FlowExpressions.Receiver expr,
                                javax.lang.model.element.AnnotationMirror necessaryAnnotation,
                                javax.lang.model.element.AnnotationMirror inferredAnnotation,
                                org.checkerframework.framework.flow.CFAbstractStore<?,?> store)

Overrides:

checkContract in class org.checkerframework.common.basetype.BaseTypeVisitor<Factory extends InitializationAnnotatedTypeFactory<Value,Store,?,?>>

visitTypeCast

public java.lang.Void visitTypeCast(TypeCastTree node,
                                    java.lang.Void p)

Specified by:

visitTypeCast in interface TreeVisitor<java.lang.Void,java.lang.Void>

Overrides:

visitTypeCast in class org.checkerframework.common.basetype.BaseTypeVisitor<Factory extends InitializationAnnotatedTypeFactory<Value,Store,?,?>>

processClassTree

public void processClassTree(ClassTree node)

Overrides:

processClassTree in class org.checkerframework.common.basetype.BaseTypeVisitor<Factory extends InitializationAnnotatedTypeFactory<Value,Store,?,?>>

visitMethod

public java.lang.Void visitMethod(MethodTree node,
                                  java.lang.Void p)

Specified by:

visitMethod in interface TreeVisitor<java.lang.Void,java.lang.Void>

Overrides:

visitMethod in class org.checkerframework.common.basetype.BaseTypeVisitor<Factory extends InitializationAnnotatedTypeFactory<Value,Store,?,?>>

checkFieldsInitialized

protected void checkFieldsInitialized(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.