import org.checkerframework.checker.calledmethods.qual.*;

// basic subtyping checks
public class Subtyping {
  @CalledMethods({}) Object top_top(@CalledMethods({}) Object o) {
    return o;
  }

  @CalledMethods({}) Object top_a(@CalledMethods({"a"}) Object o) {
    return o;
  }

  @CalledMethods({}) Object top_ab(@CalledMethods({"a", "b"}) Object o) {
    return o;
  }

  @CalledMethods({}) Object top_bot(@CalledMethodsBottom Object o) {
    return o;
  }

  @CalledMethods({"a"}) Object a_top(@CalledMethods({}) Object o) {
    // :: error: return
    return o;
  }

  @CalledMethods({"a"}) Object a_a(@CalledMethods({"a"}) Object o) {
    return o;
  }

  @CalledMethods({"a"}) Object a_ab(@CalledMethods({"a", "b"}) Object o) {
    return o;
  }

  @CalledMethods({"a"}) Object a_bot(@CalledMethodsBottom Object o) {
    return o;
  }

  @CalledMethods({"a", "b"}) Object ab_top(@CalledMethods({}) Object o) {
    // :: error: return
    return o;
  }

  @CalledMethods({"a", "b"}) Object ab_a(@CalledMethods({"a"}) Object o) {
    // :: error: return
    return o;
  }

  @CalledMethods({"a", "b"}) Object ab_ab(@CalledMethods({"a", "b"}) Object o) {
    return o;
  }

  @CalledMethods({"a", "b"}) Object ab_bot(@CalledMethodsBottom Object o) {
    return o;
  }

  @CalledMethodsBottom Object bot_top(@CalledMethods({}) Object o) {
    // :: error: return
    return o;
  }

  @CalledMethodsBottom Object bot_a(@CalledMethods({"a"}) Object o) {
    // :: error: return
    return o;
  }

  @CalledMethodsBottom Object bot_ab(@CalledMethods({"a", "b"}) Object o) {
    // :: error: return
    return o;
  }

  @CalledMethodsBottom Object bot_bot(@CalledMethodsBottom Object o) {
    return o;
  }
}