framework/tests/value/Switch.java

import org.checkerframework.common.value.qual.*;

// Test case for switch statements. Not really about the value checker (more about
// whether the semantics of switch are correct in general), but I needed some
// checker to try it out on.
public class Switch {
  void test1(@IntVal({1, 2, 3, 4, 5}) int x) {

    // easy version, no fall through
    switch (x) {
      case 1:
        @IntVal({1}) int y = x;
        break;
      case 2:
        @IntVal({2}) int w = x;
        // :: error: (assignment)
        @IntVal({1}) int z = x;
        break;
      default:
        @IntVal({3, 4, 5}) int q = x;
        break;
    }
  }

  void test2(@IntVal({1, 2, 3, 4, 5}) int x) {

    // harder version, fall through
    switch (x) {
      case 1:
        @IntVal({1}) int y = x;
      case 2:
      case 3:
        @IntVal({1, 2, 3}) int w = x;
        // :: error: (assignment)
        @IntVal({2, 3}) int z = x;
        // :: error: (assignment)
        @IntVal({3}) int z1 = x;
        break;
      default:
        @IntVal({4, 5}) int q = x;

        // :: error: (assignment)
        @IntVal(5) int q2 = x;
        break;
    }
  }

  void test3(@IntVal({1, 2, 3, 4, 5}) int x) {

    // harder version, fall through
    switch (x) {
      case 1:
        @IntVal({1}) int y = x;
      case 2:
      case 3:
        @IntVal({1, 2, 3}) int w = x;
        // :: error: (assignment)
        @IntVal({2, 3}) int z = x;
        // :: error: (assignment)
        @IntVal({3}) int z1 = x;
        break;
      case 4:
      default:
        @IntVal({4, 5}) int q = x;

        // :: error: (assignment)
        @IntVal(5) int q2 = x;
        break;
    }
  }

  void test4(int x) {
    switch (x) {
      case 1:
        @IntVal({1}) int y = x;
        break;
      case 2:
      case 3:
        @IntVal({2, 3}) int z = x;
        break;
      case 4:
      default:
        return;
    }
    @IntVal({1, 2, 3}) int y = x;
    // :: error: (assignment)
    @IntVal(4) int y2 = x;
  }

  void test5(@IntVal({0, 1, 2, 3, 4}) int x) {
    @IntVal({0, 1, 2, 3, 4, 5}) int y = x;
    switch (y = y + 1) {
      case 1:
        @IntVal({1}) int a = y;
        // :: error: (assignment)
        @IntVal({2}) int b = y;
      case 2:
      case 3:
        @IntVal({1, 2, 3}) int c = y;
        break;
      default:
        // :: error: (assignment)
        @IntVal({4}) int d = y;
        // :: error: (assignment)
        @IntVal({5}) int e = y;
        @IntVal({4, 5}) int f = y;
        break;
    }
  }

  void testInts1(@IntRange(from = 0, to = 100) int x) {
    switch (x) {
      case 0:
      case 1:
      case 2:
        @IntVal({0, 1, 2}) int z = x;
        return;
      default:
    }

    @IntRange(from = 3, to = 100) int z = x;
  }

  void testInts2(@IntRange(from = 0, to = 100) int x) {

    // harder version, fall through
    switch (x) {
      case 0:
        @IntVal(0) int a = x;
        break;
      case 1:
        @IntVal(1) int b = x;
        break;
      case 2:
        @IntVal(2) int c = x;
      default:
        @IntRange(from = 2, to = 100) int d = x;
        break;
    }
  }

  void testChars(char x) {
    switch (x) {
      case 'a':
      case 2:
        @IntVal({'a', 2}) int z = x;
        break;
      case 'b':
        @IntVal('b') int v = x;
        break;
      default:
        return;
    }
    @IntVal({'a', 2, 'b'}) int y = x;
  }

  void testStrings1(String s) {
    switch (s) {
      case "Good":
        @StringVal("Good") String x = s;
      case "Bye":
        @StringVal({"Good", "Bye"}) String y = s;
        break;
      case "Hello":
        @StringVal("Hello") String z = s;
        break;
      default:
        return;
    }
    @StringVal({"Good", "Bye", "Hello"}) String q = s;
  }

  void testStrings2(String s) {
    String a;
    switch (a = s) {
      case "Good":
        @StringVal("Good") String x1 = a;
        @StringVal("Good") String x2 = s;
      case "Bye":
        @StringVal({"Good", "Bye"}) String y1 = a;
        @StringVal({"Good", "Bye"}) String y2 = s;
        break;
      case "Hello":
        @StringVal("Hello") String z1 = a;
        @StringVal("Hello") String z2 = s;
        break;
      default:
        return;
    }
    @StringVal({"Good", "Bye", "Hello"}) String q1 = a;
    @StringVal({"Good", "Bye", "Hello"}) String q2 = s;
  }
}