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

// various tests about keeping information in the store about pure method calls
public class StorePure {

  String f1, f2;

  // various pure methods

  @Pure
  String pure1() {
    return null;
  }

  @Pure
  String pure1b() {
    return null;
  }

  @Deterministic
  String pure1c() {
    return null;
  }

  @Pure
  String pure2(int i) {
    return null;
  }

  @Pure
  String pure3(boolean b) {
    return null;
  }

  @Pure
  String pure4(String o) {
    return null;
  }

  void nonpure() {}

  void t1(@Odd String p1, String p2, boolean b1) {
    String l0 = "";
    if (pure1() == p1) {
      @Odd String l1 = pure1();
      l0 = "a"; // does not remove information
      @Odd String l1b = pure1();
      // :: error: (assignment)
      @Odd String l2 = pure1b();
      nonpure(); // non-pure method call might change the return value of pure1
      // :: error: (assignment)
      @Odd String l3 = pure1();
    }
  }

  // check that it only works for deterministic methods
  void t1b(@Odd String p1, String p2, boolean b1) {
    if (pure1c() == p1) {
      @Odd String l1 = pure1c();
    }
  }

  void t2(@Odd String p1, String p2, boolean b1) {
    String l0 = "";
    if (pure1() == p1) {
      @Odd String l1 = pure1();
      l0 = "a"; // does not remove information
      @Odd String l1b = pure1();
      // :: error: (assignment)
      @Odd String l2 = pure1b();
      f1 = ""; // field update might change the return value of pure1
      // :: error: (assignment)
      @Odd String l3 = pure1();
    }
  }

  void t3(@Odd String p1, String p2, boolean b1) {
    String l0 = "";
    if (pure2(1) == p1) {
      // :: error: (assignment)
      @Odd String l4 = pure2(0);
      @Odd String l1 = pure2(1);
      l0 = "a"; // does not remove information
      @Odd String l1b = pure2(1);
      nonpure(); // non-pure method call might change the return value of pure2
      // :: error: (assignment)
      @Odd String l3 = pure2(1);
    }
  }

  void t4(@Odd String p1, String p2, boolean b1) {
    String l0 = "";
    if (pure2(1) == p1) {
      // :: error: (assignment)
      @Odd String l4 = pure2(0);
      @Odd String l1 = pure2(1);
      l0 = "a"; // does not remove information
      @Odd String l1b = pure2(1);
      f1 = ""; // field update might change the return value of pure2
      // :: error: (assignment)
      @Odd String l3 = pure2(1);
    }
  }

  void t5(@Odd String p1, String p2, boolean b1) {
    String l0 = "";
    if (pure3(true) == p1) {
      // :: error: (assignment)
      @Odd String l4 = pure3(false);
      @Odd String l1 = pure3(true);
      l0 = "a"; // does not remove information
      @Odd String l1b = pure3(true);
      nonpure(); // non-pure method call might change the return value of pure2
      // :: error: (assignment)
      @Odd String l3 = pure3(true);
    }
  }

  void t6(@Odd String p1, String p2, boolean b1) {
    String l0 = "";
    if (pure3(true) == p1) {
      // :: error: (assignment)
      @Odd String l4 = pure3(false);
      @Odd String l1 = pure3(true);
      l0 = "a"; // does not remove information
      @Odd String l1b = pure3(true);
      f1 = ""; // field update might change the return value of pure2
      // :: error: (assignment)
      @Odd String l3 = pure3(true);
    }
  }

  // local variable as argument
  void t7(@Odd String p1, String p2, boolean b1) {
    String l0 = "";
    if (pure4(l0) == p1) {
      // :: error: (assignment)
      @Odd String l4 = pure4("jk");
      @Odd String l1 = pure4(l0);
      l0 = "a"; // remove information (!)
      // :: error: (assignment)
      @Odd String l1b = pure4(l0);
    }
  }
}