import org.checkerframework.dataflow.qual.Deterministic;
import org.checkerframework.dataflow.qual.Pure;
import org.checkerframework.dataflow.qual.SideEffectFree;
import org.checkerframework.framework.test.*;
import org.checkerframework.framework.testchecker.util.*;

// various tests for the @Pure annotation
public class Purity {

  String f1, f2, f3;
  String[] a;

  // class with a (potentially) non-pure constructor
  private static class NonPureClass {}

  // class with a pure constructor
  private static class PureClass {
    @Pure
    // :: warning: (purity.deterministic.constructor)
    public PureClass() {}
  }

  // class with a side-effect-free constructor
  private static class SEClass {
    @SideEffectFree
    public SEClass() {}
  }

  // a method that is not pure (no annotation)
  void nonpure() {}

  @Pure
  String pure() {
    return "";
  }

  @Pure
  // :: warning: (purity.deterministic.void.method)
  void t1() {}

  @SideEffectFree
  void t1b() {}

  @Deterministic
  // :: warning: (purity.deterministic.void.method)
  void t1c() {}

  @Pure
  String t2() {
    return "";
  }

  @Pure
  String t3() {
    // :: error: (purity.not.deterministic.not.sideeffectfree.call)
    nonpure();
    // :: error: (purity.not.deterministic.call)
    t16b(); // Calling a @SideEffectFree method
    // :: error: (purity.not.sideeffectfree.call)
    t16c(); // Calling a @Deterministic method
    return "";
  }

  @Pure
  String t4() {
    pure();
    return "";
  }

  @Pure
  int t5() {
    int i = 1;
    return i;
  }

  @Pure
  int t6() {
    int j = 0;
    for (int i = 0; i < 10; i++) {
      j = j - i;
    }
    return j;
  }

  @Pure
  String t7() {
    if (true) {
      return "a";
    }
    return "";
  }

  @Pure
  int t8() {
    return 1 - 2 / 3 * 2 % 2;
  }

  @Pure
  String t9() {
    return "b" + "a";
  }

  @Pure
  String t10() {
    // :: error: (purity.not.deterministic.not.sideeffectfree.assign.field)
    f1 = "";
    // :: error: (purity.not.deterministic.not.sideeffectfree.assign.field)
    f2 = "";
    return "";
  }

  @Pure
  String t11(Purity l) {
    // :: error: (purity.not.deterministic.not.sideeffectfree.assign.array)
    l.a[0] = "";
    return "";
  }

  @Pure
  String t12(String[] s) {
    // :: error: (purity.not.deterministic.not.sideeffectfree.assign.array)
    s[0] = "";
    return "";
  }

  @Pure
  String t13() {
    // :: error: (purity.not.deterministic.object.creation)
    PureClass p = new PureClass();
    return "";
  }

  @SideEffectFree
  String t13b() {
    PureClass p = new PureClass();
    return "";
  }

  @SideEffectFree
  String t13d() {
    SEClass p = new SEClass();
    return "";
  }

  @Deterministic
  String t13c() {
    // :: error: (purity.not.deterministic.object.creation)
    PureClass p = new PureClass();
    return "";
  }

  @Pure
  String t14() {
    String i = "";
    i = "a";
    return i;
  }

  @Pure
  String t15() {
    String[] s = new String[1];
    return s[0];
  }

  @Pure
  String t16() {
    try {
      int i = 1 / 0;
      // :: error: (purity.not.deterministic.catch)
    } catch (Throwable t) {
      // ...
    }
    return "";
  }

  @SideEffectFree
  String t16b() {
    try {
      int i = 1 / 0;
    } catch (Throwable t) {
      // ...
    }
    return "";
  }

  @Deterministic
  String t16c() {
    try {
      int i = 1 / 0;
      // :: error: (purity.not.deterministic.catch)
    } catch (Throwable t) {
      // ...
    }
    return "";
  }

  @Pure
  String t12() {
    // :: error: (purity.not.sideeffectfree.call)
    // :: error: (purity.not.deterministic.object.creation)
    NonPureClass p = new NonPureClass();
    return "";
  }

  @Deterministic
  String t17a(Purity l) {
    // :: error: (purity.not.deterministic.assign.field)
    f1 = "";
    // :: error: (purity.not.deterministic.assign.array)
    l.a[0] = "";
    // :: error: (purity.not.deterministic.call)
    nonpure();
    // :: error: (purity.not.deterministic.call)
    return t16b(); // Calling a @SideEffectFree method
  }

  @SideEffectFree
  String t17b() {
    // :: error: (purity.not.sideeffectfree.assign.field)
    f1 = "";
    // :: error: (purity.not.sideeffectfree.call)
    NonPureClass p = new NonPureClass();
    // :: error: (purity.not.sideeffectfree.call)
    nonpure();
    // :: error: (purity.not.sideeffectfree.call)
    return t16c(); // Calling a @Deterministic method
  }

  // @Pure annotations on the overridden implementation.
  class Super {
    @Pure
    int m1(int arg) {
      return 0;
    }

    @Pure
    int m2(int arg) {
      return 0;
    }

    int m3(int arg) {
      return 0;
    }

    int m4(int arg) {
      return 0;
    }
  }

  class Sub extends Super {
    @Pure
    int m1(int arg) {
      return 0;
    }

    int m2(int arg) {
      return 0;
    }

    @Pure
    int m3(int arg) {
      return 0;
    }

    int m4(int arg) {
      return 0;
    }
  }

  class MyClass extends Object {
    public int hashCode() {
      return 42;
    }
  }
}