| package org.checkerframework.framework.testchecker.testaccumulation; |
| |
| import com.sun.source.tree.MethodInvocationTree; |
| import javax.lang.model.element.AnnotationMirror; |
| import org.checkerframework.common.accumulation.AccumulationAnnotatedTypeFactory; |
| import org.checkerframework.common.basetype.BaseTypeChecker; |
| import org.checkerframework.framework.testchecker.testaccumulation.qual.TestAccumulation; |
| import org.checkerframework.framework.testchecker.testaccumulation.qual.TestAccumulationBottom; |
| import org.checkerframework.framework.testchecker.testaccumulation.qual.TestAccumulationPredicate; |
| import org.checkerframework.framework.type.AnnotatedTypeMirror; |
| import org.checkerframework.framework.type.treeannotator.ListTreeAnnotator; |
| import org.checkerframework.framework.type.treeannotator.TreeAnnotator; |
| import org.checkerframework.javacutil.TreeUtils; |
| |
| /** |
| * The annotated type factory for a test accumulation checker, which implements a basic called |
| * methods checker. |
| */ |
| public class TestAccumulationAnnotatedTypeFactory extends AccumulationAnnotatedTypeFactory { |
| /** |
| * Create a new accumulation checker's annotated type factory. |
| * |
| * @param checker the checker |
| */ |
| public TestAccumulationAnnotatedTypeFactory(BaseTypeChecker checker) { |
| super( |
| checker, |
| TestAccumulation.class, |
| TestAccumulationBottom.class, |
| TestAccumulationPredicate.class); |
| this.postInit(); |
| } |
| |
| @Override |
| protected TreeAnnotator createTreeAnnotator() { |
| return new ListTreeAnnotator( |
| super.createTreeAnnotator(), new TestAccumulationTreeAnnotator(this)); |
| } |
| |
| /** |
| * Necessary for the type rule for called methods described below. A new accumulation analysis |
| * might have other type rules here, or none at all. |
| */ |
| private class TestAccumulationTreeAnnotator extends AccumulationTreeAnnotator { |
| /** |
| * Creates an instance of this tree annotator for the given type factory. |
| * |
| * @param factory the type factory |
| */ |
| public TestAccumulationTreeAnnotator(AccumulationAnnotatedTypeFactory factory) { |
| super(factory); |
| } |
| |
| @Override |
| public Void visitMethodInvocation(MethodInvocationTree tree, AnnotatedTypeMirror type) { |
| // CalledMethods requires special treatment of the return values of methods that return |
| // their receiver: the default return type must include the method being invoked. |
| // |
| // The basic accumulation analysis cannot handle this case - it can use the RR checker to |
| // transfer an annotation from the receiver to the return type, but because accumulation (has |
| // to) happen in dataflow, the correct annotation may not yet be available. The basic |
| // accumulation analysis therefore only supports "pass-through" returns receiver methods; it |
| // does not support automatically accumulating at the same time. |
| if (returnsThis(tree)) { |
| String methodName = TreeUtils.getMethodName(tree.getMethodSelect()); |
| AnnotationMirror oldAnno = type.getAnnotationInHierarchy(top); |
| type.replaceAnnotation( |
| qualHierarchy.greatestLowerBound(oldAnno, createAccumulatorAnnotation(methodName))); |
| } |
| return super.visitMethodInvocation(tree, type); |
| } |
| } |
| } |