Class InitializationParentAnnotatedTypeFactory.CommitmentTreeAnnotator
- java.lang.Object
-
- com.sun.source.util.SimpleTreeVisitor<java.lang.Void,AnnotatedTypeMirror>
-
- org.checkerframework.framework.type.treeannotator.TreeAnnotator
-
- org.checkerframework.framework.type.treeannotator.PropagationTreeAnnotator
-
- org.checkerframework.checker.initialization.InitializationParentAnnotatedTypeFactory.CommitmentTreeAnnotator
-
- All Implemented Interfaces:
com.sun.source.tree.TreeVisitor<java.lang.Void,AnnotatedTypeMirror>
- Enclosing class:
- InitializationParentAnnotatedTypeFactory
protected class InitializationParentAnnotatedTypeFactory.CommitmentTreeAnnotator extends PropagationTreeAnnotator
This tree annotator modifies the propagation tree annotator to add propagation rules for the freedom-before-commitment system.
-
-
Field Summary
-
Fields inherited from class org.checkerframework.framework.type.treeannotator.TreeAnnotator
atypeFactory
-
-
Constructor Summary
Constructors Constructor Description CommitmentTreeAnnotator(InitializationParentAnnotatedTypeFactory initializationAnnotatedTypeFactory)
Creates a new CommitmentTreeAnnotator.
-
Method Summary
All Methods Instance Methods Concrete Methods Modifier and Type Method Description java.lang.Void
visitBinary(com.sun.source.tree.BinaryTree tree, AnnotatedTypeMirror type)
When overriding this method, getAnnotatedType on the left and right operands should only be called when absolutely necessary.java.lang.Void
visitLiteral(com.sun.source.tree.LiteralTree tree, AnnotatedTypeMirror type)
java.lang.Void
visitMemberSelect(com.sun.source.tree.MemberSelectTree tree, AnnotatedTypeMirror annotatedTypeMirror)
java.lang.Void
visitMethod(com.sun.source.tree.MethodTree tree, AnnotatedTypeMirror p)
This method is not called when checking a method invocation against its declaration.java.lang.Void
visitNewArray(com.sun.source.tree.NewArrayTree tree, AnnotatedTypeMirror type)
java.lang.Void
visitNewClass(com.sun.source.tree.NewClassTree tree, AnnotatedTypeMirror p)
java.lang.Void
visitUnary(com.sun.source.tree.UnaryTree tree, AnnotatedTypeMirror type)
-
Methods inherited from class org.checkerframework.framework.type.treeannotator.PropagationTreeAnnotator
visitCompoundAssignment, visitTypeCast
-
Methods inherited from class org.checkerframework.framework.type.treeannotator.TreeAnnotator
log
-
Methods inherited from class com.sun.source.util.SimpleTreeVisitor
defaultAction, visit, visit, visitAnnotatedType, visitAnnotation, visitArrayAccess, visitArrayType, visitAssert, visitAssignment, visitBlock, visitBreak, visitCase, visitCatch, visitClass, visitCompilationUnit, visitConditionalExpression, visitContinue, visitDoWhileLoop, visitEmptyStatement, visitEnhancedForLoop, visitErroneous, visitExports, visitExpressionStatement, visitForLoop, visitIdentifier, visitIf, visitImport, visitInstanceOf, visitIntersectionType, visitLabeledStatement, visitLambdaExpression, visitMemberReference, visitMethodInvocation, visitModifiers, visitModule, visitOpens, visitOther, visitPackage, visitParameterizedType, visitParenthesized, visitPrimitiveType, visitProvides, visitRequires, visitReturn, visitSwitch, visitSynchronized, visitThrow, visitTry, visitTypeParameter, visitUnionType, visitUses, visitVariable, visitWhileLoop, visitWildcard
-
-
-
-
Constructor Detail
-
CommitmentTreeAnnotator
public CommitmentTreeAnnotator(InitializationParentAnnotatedTypeFactory initializationAnnotatedTypeFactory)
Creates a new CommitmentTreeAnnotator.- Parameters:
initializationAnnotatedTypeFactory
- this factory
-
-
Method Detail
-
visitMethod
public java.lang.Void visitMethod(com.sun.source.tree.MethodTree tree, AnnotatedTypeMirror p)
Description copied from class:TreeAnnotator
This method is not called when checking a method invocation against its declaration. So, instead of overriding this method, override TypeAnnotator.visitExecutable. TypeAnnotator.visitExecutable is called both when checking method declarations and method invocations.- Specified by:
visitMethod
in interfacecom.sun.source.tree.TreeVisitor<java.lang.Void,AnnotatedTypeMirror>
- Overrides:
visitMethod
in classTreeAnnotator
- See Also:
TypeAnnotator
-
visitNewClass
public java.lang.Void visitNewClass(com.sun.source.tree.NewClassTree tree, AnnotatedTypeMirror p)
- Specified by:
visitNewClass
in interfacecom.sun.source.tree.TreeVisitor<java.lang.Void,AnnotatedTypeMirror>
- Overrides:
visitNewClass
in classcom.sun.source.util.SimpleTreeVisitor<java.lang.Void,AnnotatedTypeMirror>
-
visitLiteral
public java.lang.Void visitLiteral(com.sun.source.tree.LiteralTree tree, AnnotatedTypeMirror type)
- Specified by:
visitLiteral
in interfacecom.sun.source.tree.TreeVisitor<java.lang.Void,AnnotatedTypeMirror>
- Overrides:
visitLiteral
in classcom.sun.source.util.SimpleTreeVisitor<java.lang.Void,AnnotatedTypeMirror>
-
visitNewArray
public java.lang.Void visitNewArray(com.sun.source.tree.NewArrayTree tree, AnnotatedTypeMirror type)
- Specified by:
visitNewArray
in interfacecom.sun.source.tree.TreeVisitor<java.lang.Void,AnnotatedTypeMirror>
- Overrides:
visitNewArray
in classPropagationTreeAnnotator
-
visitMemberSelect
public java.lang.Void visitMemberSelect(com.sun.source.tree.MemberSelectTree tree, AnnotatedTypeMirror annotatedTypeMirror)
- Specified by:
visitMemberSelect
in interfacecom.sun.source.tree.TreeVisitor<java.lang.Void,AnnotatedTypeMirror>
- Overrides:
visitMemberSelect
in classcom.sun.source.util.SimpleTreeVisitor<java.lang.Void,AnnotatedTypeMirror>
-
visitBinary
public java.lang.Void visitBinary(com.sun.source.tree.BinaryTree tree, AnnotatedTypeMirror type)
Description copied from class:TreeAnnotator
When overriding this method, getAnnotatedType on the left and right operands should only be called when absolutely necessary. Otherwise, the checker will be very slow on heavily nested binary trees. (For example, a + b + c + d + e + f + g + h.)If a checker's performance is still too slow, the types of binary trees could be computed in a subclass of
CFTransfer
. When computing the types in a transfer, look up the value in the store rather than the AnnotatedTypeFactory. Then this method should annotate binary trees with top so that the type applied in the transfer is always a subtype of the type the AnnotatedTypeFactory computes.- Specified by:
visitBinary
in interfacecom.sun.source.tree.TreeVisitor<java.lang.Void,AnnotatedTypeMirror>
- Overrides:
visitBinary
in classPropagationTreeAnnotator
-
visitUnary
public java.lang.Void visitUnary(com.sun.source.tree.UnaryTree tree, AnnotatedTypeMirror type)
- Specified by:
visitUnary
in interfacecom.sun.source.tree.TreeVisitor<java.lang.Void,AnnotatedTypeMirror>
- Overrides:
visitUnary
in classPropagationTreeAnnotator
-
-