checker/tests/wpi-testchecker/non-annotated/Planet.java

// This test checks that enums with fields and methods are handled correctly

import org.checkerframework.checker.testchecker.wholeprograminference.qual.Sibling1;

@SuppressWarnings(
    "value" // Do not generate Value Checker annotations, because IndexFileParser cannot handle
// scientific notation.
)
public enum Planet {
  MERCURY(3.303e+23, 2.4397e6),
  VENUS(4.869e+24, 6.0518e6),
  EARTH(5.976e+24, 6.37814e6),
  MARS(6.421e+23, 3.3972e6),
  JUPITER(1.9e+27, 7.1492e7),
  SATURN(5.688e+26, 6.0268e7),
  URANUS(8.686e+25, 2.5559e7),
  NEPTUNE(1.024e+26, 2.4746e7);

  public int foo;

  private final double mass; // in kilograms
  private final double radius; // in meters

  Planet(double mass, double radius) {
    this.mass = mass;
    this.radius = radius;
  }

  private double mass() {
    return mass;
  }

  private double radius() {
    return radius;
  }

  // universal gravitational constant  (m3 kg-1 s-2)
  public static final double G = 6.67300E-11;

  double surfaceGravity() {
    return G * mass / (radius * radius);
  }

  double surfaceWeight(double otherMass) {
    return otherMass * surfaceGravity();
  }

  void test(@Sibling1 int x) {
    foo = x;
  }

  void test2() {
    // :: warning: argument
    test(foo);
  }
}