checker/tests/interning/Enumerations.java

public class Enumerations {

  // All enumeration instances are interned; there should be no need for an annotation.
  enum StudentYear {
    FRESHMAN,
    SOPHOMORE,
    JUNIOR,
    SENIOR;

    // check that receiver is OK
    @org.checkerframework.dataflow.qual.Pure
    public String toString() {
      return "StudentYear: ...";
    }
  }

  public boolean isSophomore(StudentYear sy) {
    return sy == StudentYear.SOPHOMORE;
  }

  public boolean flow(StudentYear s) {
    StudentYear m = StudentYear.SOPHOMORE;
    return s == m;
  }

  StudentYear cast(Object o) {
    return (StudentYear) o;
  }
}