org.checkerframework.checker.javari

Class JavariVisitor

java.lang.Object

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

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

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

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

org.checkerframework.checker.javari.JavariVisitor

All Implemented Interfaces:

TreeVisitor<Void,Void>

public class JavariVisitor
extends BaseTypeVisitor<JavariAnnotatedTypeFactory>

A type-checking visitor for the Javari mutability annotations (@ReadOnly, @Mutable and @Assignable) that extends BaseTypeVisitor.

See Also:

BaseTypeVisitor

Field Summary

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
JavariVisitor(BaseTypeChecker checker) Creates a new visitor for type-checking the Javari mutability annotations.

Method Summary

Modifier and Type	Method and Description
protected void	checkAssignability(AnnotatedTypeMirror varType, Tree varTree) Checks whether the variable represented by the given type and tree can be assigned, causing a checker error otherwise.
protected Set<? extends AnnotationMirror>	getExceptionParameterLowerBoundAnnotations() Returns a set of AnnotationMirrors that is a lower bound for exception parameters.
boolean	isValidUse(AnnotatedTypeMirror.AnnotatedDeclaredType elemType, AnnotatedTypeMirror.AnnotatedDeclaredType useType, Tree tree) Always true; no type validity checking is made by the BaseTypeVisitor.
boolean	isValidUse(AnnotatedTypeMirror.AnnotatedPrimitiveType useType, Tree tree) Tests that the qualifiers present on the primitive type are valid.
Void	visitClass(ClassTree node, Void p) Ensures the class type is not @PolyRead outside a @PolyRead context.

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

checkAccess, checkAccess, checkArguments, checkArrayInitialization, checkConditionalPostconditions, checkConditionalPostconditionsConsistency, checkConstructorInvocation, checkContract, checkDefaultConstructor, checkExceptionParameter, checkFlowExprParameters, checkForAnnotatedJdk, checkMethodInvocability, checkMethodReferenceAsOverride, checkOverride, checkPostconditions, checkPostconditionsConsistency, checkPreconditions, checkPreconditions, checkPreconditionsConsistency, checkThrownExpression, checkTypeArguments, checkTypecastRedundancy, checkTypecastSafety, commonAssignmentCheck, commonAssignmentCheck, commonAssignmentCheck, createTypeFactory, createTypeValidator, enclosingMemberSelect, enclosingStatement, getThrowUpperBoundAnnotations, getTypeFactory, isAccessAllowed, isAssignable, isValidUse, isVectorCopyInto, reportPurityErrors, scan, setRoot, shouldSkipUses, skipContractCheck, skipReceiverSubtypeCheck, testTypevarContainment, typeCheckVectorCopyIntoArgument, validateType, validateTypeOf, visitAnnotation, visitArrayAccess, visitAssignment, visitCatch, visitCompilationUnit, visitCompoundAssignment, visitConditionalExpression, visitEnhancedForLoop, visitIdentifier, visitInstanceOf, visitLambdaExpression, visitMemberReference, visitMethod, visitMethodInvocation, visitNewArray, visitNewClass, visitParameterizedType, visitReturn, visitThrow, visitTypeCast, visitTypeParameter, visitUnary, visitVariable

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

Constructor Detail

JavariVisitor

public JavariVisitor(BaseTypeChecker checker)

Creates a new visitor for type-checking the Javari mutability annotations.

Parameters:

checker - the JavariChecker to use

Method Detail

visitClass

public Void visitClass(ClassTree node,
                       Void p)

Ensures the class type is not @PolyRead outside a @PolyRead context.

Specified by:

visitClass in interface TreeVisitor<Void,Void>

Overrides:

visitClass in class BaseTypeVisitor<JavariAnnotatedTypeFactory>

checkAssignability

protected void checkAssignability(AnnotatedTypeMirror varType,
                                  Tree varTree)

Checks whether the variable represented by the given type and tree can be assigned, causing a checker error otherwise.

Overrides:

checkAssignability in class BaseTypeVisitor<JavariAnnotatedTypeFactory>

Parameters:

varType - the type of the variable being re-assigned

varTree - the tree used to access the variable in the assignment

getExceptionParameterLowerBoundAnnotations

protected Set<? extends AnnotationMirror> getExceptionParameterLowerBoundAnnotations()

Description copied from class: BaseTypeVisitor

Returns a set of AnnotationMirrors that is a lower bound for exception parameters. Note: by default this method is called by getThrowUpperBoundAnnotations(), so that this annotation is enforced. (Default is top)

Overrides:

getExceptionParameterLowerBoundAnnotations in class BaseTypeVisitor<JavariAnnotatedTypeFactory>

Returns:

Set of annotation mirrors, one per hierarchy, that from a lower bound of annotations that can be written on an exception parameter

isValidUse

public boolean isValidUse(AnnotatedTypeMirror.AnnotatedDeclaredType elemType,
                          AnnotatedTypeMirror.AnnotatedDeclaredType useType,
                          Tree tree)

Always true; no type validity checking is made by the BaseTypeVisitor.

Overrides:

isValidUse in class BaseTypeVisitor<JavariAnnotatedTypeFactory>

Parameters:

elemType - the type of the class (TypeElement)

useType - the use of the class (instance type)

tree - the tree where the type is used

Returns:

true if the useType is a valid use of elemType

See Also:

BaseTypeVisitor

isValidUse

public boolean isValidUse(AnnotatedTypeMirror.AnnotatedPrimitiveType useType,
                          Tree tree)

Description copied from class: BaseTypeVisitor

Tests that the qualifiers present on the primitive type are valid. The default implementation always returns true. Subclasses should override this method to limit what annotations are allowed on primitive types.

Overrides:

isValidUse in class BaseTypeVisitor<JavariAnnotatedTypeFactory>

Parameters:

useType - the use of the primitive type

tree - the tree where the type is used

Returns:

true if the type is a valid use of the primitive type