Add ignoreDeadCode option

checker/src/main/java/org/checkerframework/checker/nullness/NullnessNoInitVisitor.java

@@ -286,9 +286,9 @@ protected boolean commonAssignmentCheck(
     /** Case 1: Check for null dereferencing. */
     @Override
     public Void visitMemberSelect(MemberSelectTree tree, Void p) {
-        // if (atypeFactory.isUnreachable(tree)) {
-        //     return super.visitMemberSelect(tree, p);
-        // }
+        if (ignoreDeadCode && atypeFactory.isUnreachable(tree)) {
+            return super.visitMemberSelect(tree, p);
+        }
         Element e = TreeUtils.elementFromUse(tree);
         if (e.getKind() == ElementKind.CLASS) {
             if (atypeFactory.containsNullnessAnnotation(null, tree.getExpression())) {

checker/src/test/java/org/checkerframework/checker/test/junit/NullnessIgnoreDeadCodeTest.java

@@ -0,0 +1,33 @@
+package org.checkerframework.checker.test.junit;
+
+import org.checkerframework.framework.test.CheckerFrameworkPerDirectoryTest;
+import org.junit.runners.Parameterized;
+
+import java.io.File;
+import java.util.List;
+
+/** JUnit tests for the Nullness checker when -AignoreDeadCode command-line argument is used. */
+public class NullnessIgnoreDeadCodeTest extends CheckerFrameworkPerDirectoryTest {
+    /**
+     * Create a NullnessNullMarkedTest.
+     *
+     * @param testFiles the files containing test code, which will be type-checked
+     */
+    public NullnessIgnoreDeadCodeTest(List<File> testFiles) {
+        super(
+                testFiles,
+                org.checkerframework.checker.nullness.NullnessChecker.class,
+                "nullness-ignoredeadcode",
+                "-AignoreDeadCode");
+    }
+
+    /**
+     * Returns an array of test directory paths for parameterized testing.
+     *
+     * @return an array containing the test directory names
+     */
+    @Parameterized.Parameters
+    public static String[] getTestDirs() {
+        return new String[] {"nullness-ignoredeadcode"};
+    }
+}

checker/tests/nullness-ignoredeadcode/DeadBranchNPE.java

@@ -0,0 +1,31 @@
+class DeadBranchNPE {
+    void test1() {
+        Object obj = null;
+        if (true) {
+            // :: error: (dereference.of.nullable)
+            obj.toString();
+        } else {
+            // TODO: This is a dead branch should not issue error, the currently it does
+            // obj.toString();
+        }
+    }
+
+    void test2() {
+        Object obj = null;
+        // :: error: (dereference.of.nullable)
+        obj.toString();
+        // The following loop is dead code because the loop condition is false.
+        for (int i = 0; i < 0; i++) {
+            obj.toString();
+        }
+    }
+
+    void test3() {
+        Object obj = null;
+        // :: error: (dereference.of.nullable)
+        obj.toString();
+        while (obj != null) {
+            obj.toString();
+        }
+    }
+}

docs/CHANGELOG.md

@@ -3,6 +3,8 @@ Version 3.42.0-eisop6 (January ??, 2025)
 
 **User-visible changes:**
 
+New command-line option `-AignoreDeadCode` to ignore unreachable code when running checkers.
+
 **Implementation details:**
 
 **Closed issues:**

docs/manual/introduction.tex

@@ -599,6 +599,8 @@
 \item \<-AignoreTargetLocations>
   Disables validating the target locations of qualifiers based on
   `@TargetLocations` meta-annotations. This option is not enabled by default.
+\item \<-AignoreDeadCode>
+Ignore unreachable code when running Checkers.
 \end{itemize}
 
 \label{unsound-by-default}

framework/src/main/java/org/checkerframework/common/basetype/BaseTypeVisitor.java

@@ -290,6 +290,9 @@ public class BaseTypeVisitor<Factory extends GenericAnnotatedTypeFactory<?, ?, ?
     /** True if "-AcheckEnclosingExpr" was passed on the command line. */
     private final boolean checkEnclosingExpr;
 
+    /** True if "-AignoreDeadCode" was passed on the command line. */
+    protected final boolean ignoreDeadCode;
+
     /** The tree of the enclosing method that is currently being visited. */
     protected @Nullable MethodTree methodTree = null;
 
@@ -351,6 +354,7 @@ protected BaseTypeVisitor(BaseTypeChecker checker, @Nullable Factory typeFactory
         checkCastElementType = checker.hasOption("checkCastElementType");
         conservativeUninferredTypeArguments =
                 checker.hasOption("conservativeUninferredTypeArguments");
+        ignoreDeadCode = checker.hasOption("ignoreDeadCode");
     }
 
     /** An array containing just {@code BaseTypeChecker.class}. */
@@ -5198,9 +5202,9 @@ protected TypeValidator createTypeValidator() {
      */
     protected final boolean shouldSkipUses(ExpressionTree exprTree) {
         // System.out.printf("shouldSkipUses: %s: %s%n", exprTree.getClass(), exprTree);
-        // if (atypeFactory.isUnreachable(exprTree)) {
-        //     return true;
-        // }
+        if (ignoreDeadCode && atypeFactory.isUnreachable(exprTree)) {
+            return true;
+        }
         Element elm = TreeUtils.elementFromTree(exprTree);
         return checker.shouldSkipUses(elm);
     }

framework/src/main/java/org/checkerframework/framework/source/SourceChecker.java

@@ -152,6 +152,10 @@
     // org.checkerframework.framework.source.SourceChecker.report
     "warns",
 
+    // Make checker ignore the expression in dead branch
+    // org.checkerframework.framework.common.basetype.BaseTypeVisitor.shouldSkipUses
+    "ignoreDeadCode",
+
     ///
     /// More sound (strict checking): enable errors that are disabled by default
     ///

framework/src/main/java/org/checkerframework/framework/type/GenericAnnotatedTypeFactory.java

@@ -275,6 +275,9 @@ public abstract class GenericAnnotatedTypeFactory<
      */
     public final boolean hasOrIsSubchecker;
 
+    /** True if "-AigoreCheckDeadCode" was passed on the command line. */
+    protected final boolean ignoreDeadCode;
+
     /** An empty store. */
     // Set in postInit only
     protected Store emptyStore;
@@ -396,6 +399,7 @@ protected GenericAnnotatedTypeFactory(BaseTypeChecker checker, boolean useFlow)
         hasOrIsSubchecker =
                 !this.getChecker().getSubcheckers().isEmpty()
                         || this.getChecker().getParentChecker() != null;
+        ignoreDeadCode = checker.hasOption("ignoreDeadCode");
 
         // Every subclass must call postInit, but it must be called after
         // all other initialization is finished.
@@ -470,7 +474,9 @@ public void setRoot(@Nullable CompilationUnitTree root) {
 
         super.setRoot(root);
         this.scannedClasses.clear();
-        // this.reachableNodes.clear();
+        if (ignoreDeadCode) {
+            this.reachableNodes.clear();
+        }
         this.flowResult = null;
         this.regularExitStores.clear();
         this.exceptionalExitStores.clear();
@@ -1081,13 +1087,13 @@ public IPair<JavaExpression, String> getExpressionAndOffsetFromJavaExpressionStr
         return value != null ? value.getAnnotations().iterator().next() : null;
     }
 
-    /*
+    /**
      * Returns true if the {@code exprTree} is unreachable. This is a conservative estimate and may
      * return {@code false} even though the {@code exprTree} is unreachable.
      *
      * @param exprTree an expression tree
      * @return true if the {@code exprTree} is unreachable
-     *
+     */
     public boolean isUnreachable(ExpressionTree exprTree) {
         if (!everUseFlow) {
             return false;
@@ -1106,7 +1112,6 @@ public boolean isUnreachable(ExpressionTree exprTree) {
         // None of the corresponding nodes is reachable, so this tree is dead.
         return true;
     }
-    */
 
     /**
      * Track the state of org.checkerframework.dataflow analysis scanning for each class tree in the
@@ -1122,15 +1127,15 @@ protected enum ScanState {
     /** Map from ClassTree to their dataflow analysis state. */
     protected final Map<ClassTree, ScanState> scannedClasses = new HashMap<>();
 
-    /*
+    /**
      * A set of trees whose corresponding nodes are reachable. This is not an exhaustive set of
      * reachable trees. Use {@link #isUnreachable(ExpressionTree)} instead of this set directly.
      *
      * <p>This cannot be a set of Nodes, because two LocalVariableNodes are equal if they have the
      * same name but represent different uses of the variable. So instead of storing Nodes, it
      * stores the result of {@code Node#getTree}.
      */
-    // private final Set<Tree> reachableNodes = new HashSet<>();
+    private final Set<Tree> reachableNodes = new HashSet<>();
 
     /**
      * The result of the flow analysis. Invariant:
@@ -1609,15 +1614,16 @@ protected void analyze(
             @Nullable Store capturedStore) {
         ControlFlowGraph cfg =
                 CFCFGBuilder.build(this.getRoot(), ast, checker, this, processingEnv);
-        /*
-             cfg.getAllNodes(this::isIgnoredExceptionType)
-                     .forEach(
-                             node -> {
-                                 if (node.getTree() != null) {
-                                     reachableNodes.add(node.getTree());
-                                 }
-                             });
-        */
+        if (ignoreDeadCode) {
+            cfg.getAllNodes(this::isIgnoredExceptionType)
+                    .forEach(
+                            node -> {
+                                if (node.getTree() != null) {
+                                    reachableNodes.add(node.getTree());
+                                }
+                            });
+        }
+
         if (isInitializationCode) {
             Store initStore = !isStatic ? initializationStore : initializationStaticStore;
             if (initStore != null) {