From f66823e2dc4d7e2d67da97561537eed0ed2963bc Mon Sep 17 00:00:00 2001 From: Michael Ernst Date: Mon, 20 May 2024 07:46:10 -0700 Subject: [PATCH] Minor improvements --- .../dataflow/analysis/AbstractAnalysis.java | 4 ++-- .../dataflow/analysis/AnalysisResult.java | 11 +++++++---- docs/manual/creating-a-checker.tex | 4 ++-- .../common/basetype/BaseTypeVisitor.java | 10 ++++------ .../framework/type/AnnotatedTypeFactory.java | 5 +++-- 5 files changed, 18 insertions(+), 16 deletions(-) diff --git a/dataflow/src/main/java/org/checkerframework/dataflow/analysis/AbstractAnalysis.java b/dataflow/src/main/java/org/checkerframework/dataflow/analysis/AbstractAnalysis.java index 42b26be81ab..b15473c6d4e 100644 --- a/dataflow/src/main/java/org/checkerframework/dataflow/analysis/AbstractAnalysis.java +++ b/dataflow/src/main/java/org/checkerframework/dataflow/analysis/AbstractAnalysis.java @@ -431,8 +431,8 @@ protected void initFields(ControlFlowGraph cfg) { } /** - * Updates the value of node {@code node} to the value of the {@code transferResult}. Returns true - * if the node's value changed, or a store was updated. + * Updates the value of node {@code node} in {@link #nodeValues} to the value of the {@code + * transferResult}. Returns true if the node's value changed, or a store was updated. * * @param node the node to update * @param transferResult the transfer result being updated diff --git a/dataflow/src/main/java/org/checkerframework/dataflow/analysis/AnalysisResult.java b/dataflow/src/main/java/org/checkerframework/dataflow/analysis/AnalysisResult.java index 3575031de94..1d38de32396 100644 --- a/dataflow/src/main/java/org/checkerframework/dataflow/analysis/AnalysisResult.java +++ b/dataflow/src/main/java/org/checkerframework/dataflow/analysis/AnalysisResult.java @@ -213,6 +213,7 @@ public Map getFinalLocalValues() { * available */ public @Nullable V getValue(Tree t) { + // This is a set because one Tree might correspond to multiple Nodes. Set nodes = treeLookup.get(t); if (nodes == null) { @@ -221,10 +222,12 @@ public Map getFinalLocalValues() { V merged = null; for (Node aNode : nodes) { V a = getValue(aNode); - if (merged == null) { - merged = a; - } else if (a != null) { - merged = merged.leastUpperBound(a); + if (a != null) { + if (merged == null) { + merged = a; + } else { + merged = merged.leastUpperBound(a); + } } } return merged; diff --git a/docs/manual/creating-a-checker.tex b/docs/manual/creating-a-checker.tex index 16ff86fb68b..be51749eb30 100644 --- a/docs/manual/creating-a-checker.tex +++ b/docs/manual/creating-a-checker.tex @@ -1645,8 +1645,8 @@ relevant to your run-time check or run-time operation. Leave the body of the overriding method empty for now. -For example, the Regex Checker refines the type of a run-time test method -call. A method call is represented by a +For example, the Regex Checker refines the type based on a call to the +\ method. A method call is represented by a \refclass{dataflow/cfg/node}{MethodInvocationNode}. Therefore, \refclass{checker/regex}{RegexTransfer} overrides the \code{visitMethodInvocation} method: diff --git a/framework/src/main/java/org/checkerframework/common/basetype/BaseTypeVisitor.java b/framework/src/main/java/org/checkerframework/common/basetype/BaseTypeVisitor.java index 70741b94fc3..342d8366227 100644 --- a/framework/src/main/java/org/checkerframework/common/basetype/BaseTypeVisitor.java +++ b/framework/src/main/java/org/checkerframework/common/basetype/BaseTypeVisitor.java @@ -2361,12 +2361,6 @@ public Void visitAnnotation(AnnotationTree tree, Void p) { return null; } - /** - * If the computation of the type of the ConditionalExpressionTree in - * org.checkerframework.framework.type.TypeFromTree.TypeFromExpression.visitConditionalExpression(ConditionalExpressionTree, - * AnnotatedTypeFactory) is correct, the following checks are redundant. However, let's add - * another failsafe guard and do the checks. - */ @Override public Void visitConditionalExpression(ConditionalExpressionTree tree, Void p) { if (TreeUtils.isPolyExpression(tree)) { @@ -2377,6 +2371,10 @@ public Void visitConditionalExpression(ConditionalExpressionTree tree, Void p) { return super.visitConditionalExpression(tree, p); } + // If the computation of the type of the ConditionalExpressionTree in + // org.checkerframework.framework.type.TypeFromTree.TypeFromExpression.visitConditionalExpression(ConditionalExpressionTree, + // AnnotatedTypeFactory) is correct, the following checks are redundant. However, let's add + // another failsafe guard and do the checks. AnnotatedTypeMirror cond = atypeFactory.getAnnotatedType(tree); this.commonAssignmentCheck(cond, tree.getTrueExpression(), "conditional"); this.commonAssignmentCheck(cond, tree.getFalseExpression(), "conditional"); diff --git a/framework/src/main/java/org/checkerframework/framework/type/AnnotatedTypeFactory.java b/framework/src/main/java/org/checkerframework/framework/type/AnnotatedTypeFactory.java index ceea08b48ff..2e15a9a39a2 100644 --- a/framework/src/main/java/org/checkerframework/framework/type/AnnotatedTypeFactory.java +++ b/framework/src/main/java/org/checkerframework/framework/type/AnnotatedTypeFactory.java @@ -1691,8 +1691,9 @@ protected AnnotatedTypeMirror mergeAnnotationFileAnnosIntoType( * Creates an AnnotatedTypeMirror for an ExpressionTree. The AnnotatedTypeMirror contains explicit * annotations written on the expression and for some expressions, annotations from * sub-expressions that could have been explicitly written, defaulted, refined, or otherwise - * computed. (Expression whose type include annotations from sub-expressions are: ArrayAccessTree, - * ConditionalExpressionTree, IdentifierTree, MemberSelectTree, and MethodInvocationTree.) + * computed. (Expressions whose type include annotations from sub-expressions are: + * ArrayAccessTree, ConditionalExpressionTree, IdentifierTree, MemberSelectTree, and + * MethodInvocationTree.) * *

For example, the AnnotatedTypeMirror returned for an array access expression is the fully * annotated type of the array component of the array being accessed.