Fix multiple case constants. (#4985)

framework/src/main/java/org/checkerframework/framework/flow/CFAbstractTransfer.java

@@ -1118,18 +1118,20 @@ private void processPostconditionsAndConditionalPostconditions(
     }
   }
 
-  /**
-   * A case produces no value, but it may imply some facts about the argument to the switch
-   * statement.
-   */
+  /** A case produces no value, but it may imply some facts about switch selector expression. */
   @Override
   public TransferResult<V, S> visitCase(CaseNode n, TransferInput<V, S> in) {
     S store = in.getRegularStore();
-    TransferResult<V, S> result =
-        new ConditionalTransferResult<>(
-            finishValue(null, store), in.getThenStore(), in.getElseStore(), false);
-
+    TransferResult<V, S> lubResult = null;
+    // Case operands are the case constants. For example, A, B and C in case A, B, C:.
+    // This method refines the type of the selector expression and the synthetic variable that
+    // represents the selector expression to the type of the case constant if it is more precise.
+    // If there are multiple case constants then a new store is created for each case constant and
+    // then they are lubbed. This method returns the lubbed result.
     for (Node caseOperand : n.getCaseOperands()) {
+      TransferResult<V, S> result =
+          new ConditionalTransferResult<>(
+              finishValue(null, store), in.getThenStore().copy(), in.getElseStore().copy(), false);
       V caseValue = in.getValueOfSubNode(caseOperand);
       AssignmentNode assign = n.getSwitchOperand();
       V switchValue = store.getValue(JavaExpression.fromNode(assign.getTarget()));
@@ -1140,8 +1142,19 @@ public TransferResult<V, S> visitCase(CaseNode n, TransferInput<V, S> in) {
       result =
           strengthenAnnotationOfEqualTo(
               result, caseOperand, assign.getTarget(), caseValue, switchValue, false);
+
+      // Lub the result of one case label constant with the result of the others.
+      if (lubResult == null) {
+        lubResult = result;
+      } else {
+        S thenStore = lubResult.getThenStore().leastUpperBound(result.getThenStore());
+        S elseStore = lubResult.getElseStore().leastUpperBound(result.getElseStore());
+        lubResult =
+            new ConditionalTransferResult<>(
+                null, thenStore, elseStore, lubResult.storeChanged() || result.storeChanged());
+      }
     }
-    return result;
+    return lubResult;
   }
 
   /**

framework/tests/value/java17/MultiCaseConst.java

@@ -0,0 +1,31 @@
+// @below-java17-jdk-skip-test
+import org.checkerframework.common.value.qual.IntVal;
+
+public class MultiCaseConst {
+
+  void method(int selector) {
+    switch (selector) {
+      case 1, 2, 3:
+        // :: error: (assignment)
+        @IntVal(0) int o = selector;
+        @IntVal({1, 2, 3}) int tmp = selector;
+      case 4, 5:
+        // :: error: (assignment)
+        @IntVal({4, 5}) int tmp2 = selector;
+        @IntVal({1, 2, 3, 4, 5}) int tmp3 = selector;
+    }
+  }
+
+  void method2(int selector) {
+    switch (selector) {
+      case 1:
+        // :: error: (assignment)
+        @IntVal(0) int o = selector;
+        @IntVal({1, 2, 3}) int tmp = selector;
+        break;
+      case 4, 5:
+        @IntVal({4, 5}) int tmp2 = selector;
+        @IntVal({1, 2, 3, 4, 5}) int tmp3 = selector;
+    }
+  }
+}