diff --git a/checker/tests/nullness/java17/NullnessSwitchArrows.java b/checker/tests/nullness/java17/NullnessSwitchArrows.java index 2be1bec12c1..08983be671d 100644 --- a/checker/tests/nullness/java17/NullnessSwitchArrows.java +++ b/checker/tests/nullness/java17/NullnessSwitchArrows.java @@ -36,8 +36,6 @@ void method2() { default -> throw new IllegalStateException("Invalid day: " + day); } - // TODO: this is a false positive. It works for case: statements; see below. - // :: error: (dereference.of.nullable) o.toString(); } diff --git a/checker/tests/nullness/java17/NullnessSwitchStatementRules.java b/checker/tests/nullness/java17/NullnessSwitchStatementRules.java new file mode 100644 index 00000000000..9c375f64cbb --- /dev/null +++ b/checker/tests/nullness/java17/NullnessSwitchStatementRules.java @@ -0,0 +1,43 @@ +// @below-java17-jdk-skip-test +import org.checkerframework.checker.nullness.qual.Nullable; + +public class NullnessSwitchStatementRules { + @Nullable Object field = null; + + void method(int selector) { + field = new Object(); + switch (selector) { + case 1 -> field = null; + case 2 -> field.toString(); + } + + field = new Object(); + switch (selector) { + case 1 -> { + field = null; + } + case 2 -> { + field.toString(); + } + } + + field = new Object(); + switch (selector) { + case 1 -> { + field = null; + } + case 2 -> { + field.toString(); + } + } + + field = new Object(); + switch (selector) { + case 1: + field = null; + case 2: + // :: error: (dereference.of.nullable) + field.toString(); + } + } +} diff --git a/dataflow/src/main/java/org/checkerframework/dataflow/cfg/builder/CFGTranslationPhaseOne.java b/dataflow/src/main/java/org/checkerframework/dataflow/cfg/builder/CFGTranslationPhaseOne.java index 28c849dcdae..53e11178e71 100644 --- a/dataflow/src/main/java/org/checkerframework/dataflow/cfg/builder/CFGTranslationPhaseOne.java +++ b/dataflow/src/main/java/org/checkerframework/dataflow/cfg/builder/CFGTranslationPhaseOne.java @@ -2342,18 +2342,25 @@ private void buildCase(CaseTree tree, int index) { } addLabelForNextNode(thisBodyL); if (tree.getStatements() != null) { + // This is a switch labeled statement groups. for (StatementTree stmt : tree.getStatements()) { scan(stmt, null); } + // Handle possible fall through by adding jump to next body. + extendWithExtendedNode(new UnconditionalJump(nextBodyL)); } else { + // This is a switch rule. Tree bodyTree = TreeUtils.caseTreeGetBody(tree); if (switchTree.getKind() != Tree.Kind.SWITCH && bodyTree instanceof ExpressionTree) { buildSwitchExpressionResult((ExpressionTree) bodyTree); } else { scan(bodyTree, null); + // Switch rules never fall through so add jump to the break target. + assert breakTargetL != null : "no target for case statement"; + extendWithExtendedNode(new UnconditionalJump(breakTargetL.accessLabel())); } } - extendWithExtendedNode(new UnconditionalJump(nextBodyL)); + addLabelForNextNode(nextCaseL); } @@ -2388,8 +2395,8 @@ void buildSwitchExpressionResult(ExpressionTree resultExpression) { new AssignmentNode(assign, switchExprVarUseNode, resultExprNode); assignmentNode.setInSource(false); extendWithNode(assignmentNode); - - assert breakTargetL != null : "no target for yield statement"; + // Switch rules never fall through so add jump to the break target. + assert breakTargetL != null : "no target for case statement"; extendWithExtendedNode(new UnconditionalJump(breakTargetL.accessLabel())); } } diff --git a/framework/tests/value/java17/MultiCaseConst.java b/framework/tests/value/java17/MultiCaseConst.java index 6b5d0825b3d..0362299984a 100644 --- a/framework/tests/value/java17/MultiCaseConst.java +++ b/framework/tests/value/java17/MultiCaseConst.java @@ -28,4 +28,18 @@ void method2(int selector) { @IntVal({1, 2, 3, 4, 5}) int tmp3 = selector; } } + + void method3(int selector) { + switch (selector) { + case 1 -> { + // :: error: (assignment) + @IntVal(0) int o = selector; + @IntVal({1, 2, 3}) int tmp = selector; + } + case 4, 5 -> { + @IntVal({4, 5}) int tmp2 = selector; + @IntVal({1, 2, 3, 4, 5}) int tmp3 = selector; + } + } + } } diff --git a/framework/tests/value/java17/ValueSwitchStatementRules.java b/framework/tests/value/java17/ValueSwitchStatementRules.java new file mode 100644 index 00000000000..cf78c973e00 --- /dev/null +++ b/framework/tests/value/java17/ValueSwitchStatementRules.java @@ -0,0 +1,29 @@ +// @below-java17-jdk-skip-test +import org.checkerframework.common.value.qual.IntVal; + +public class ValueSwitchStatementRules { + private int field; + + void method(int selector) { + field = 300; + switch (selector) { + case 1: + field = 42; + @IntVal(42) int copyField = field; + case 2: + // :: error: (assignment) + @IntVal(300) int copyField2 = field; + } + + field = 300; + switch (selector) { + case 1 -> { + field = 42; + @IntVal(42) int copyField = field; + } + case 2 -> { + @IntVal(300) int copyField = field; + } + } + } +}