| package org.checkerframework.checker.index; |
| |
| import com.sun.source.tree.MemberSelectTree; |
| import org.checkerframework.checker.nullness.qual.Nullable; |
| import org.checkerframework.common.value.ValueCheckerUtils; |
| import org.checkerframework.dataflow.expression.JavaExpression; |
| import org.checkerframework.framework.type.AnnotatedTypeFactory; |
| import org.checkerframework.framework.type.AnnotatedTypeMirror; |
| import org.checkerframework.framework.type.treeannotator.TreeAnnotator; |
| import org.checkerframework.framework.util.dependenttypes.DependentTypesHelper; |
| import org.checkerframework.framework.util.dependenttypes.DependentTypesTreeAnnotator; |
| import org.checkerframework.javacutil.TreeUtils; |
| |
| /** |
| * Dependent type helper for array offset expressions. Each array offset expression may be the |
| * addition or subtraction of several Java expressions. For example, {@code array.length - 1}. |
| */ |
| public class OffsetDependentTypesHelper extends DependentTypesHelper { |
| public OffsetDependentTypesHelper(AnnotatedTypeFactory factory) { |
| super(factory); |
| } |
| |
| @Override |
| protected @Nullable JavaExpression transform(JavaExpression javaExpr) { |
| return ValueCheckerUtils.optimize(javaExpr, factory); |
| } |
| |
| @Override |
| public TreeAnnotator createDependentTypesTreeAnnotator() { |
| return new DependentTypesTreeAnnotator(factory, this) { |
| @Override |
| public Void visitMemberSelect(MemberSelectTree tree, AnnotatedTypeMirror type) { |
| // UpperBoundTreeAnnotator changes the type of array.length to @LTEL("array"). |
| // If the DependentTypesTreeAnnotator tries to viewpoint-adapt it based on the |
| // declaration of length, it will fail. |
| if (TreeUtils.isArrayLengthAccess(tree)) { |
| return null; |
| } |
| return super.visitMemberSelect(tree, type); |
| } |
| }; |
| } |
| } |