Feature request: WPI should infer conditional postconditions

[jyoo980]

Given the following Java class:

import java.util.Optional;
import org.checkerframework.checker.optional.qual.Present;
import org.checkerframework.framework.qual.EnsuresQualifierIf;
import org.checkerframework.dataflow.qual.Pure;

public class Main {

  public static void main(String[] args) {
    OptStringContainer optStrCont = new OptStringContainer("Hello");
    if (optStrCont.isStringEqTo("Hello")) {
      System.out.println(optStrCont.getOptStr().get());
    }
  }

  private static class OptStringContainer {

    public String str;

    public OptStringContainer(String str) {
      this.str = str;
    }

    public Optional<String> getOptStr() {
      return Optional.of(str);
    }

    public boolean isStringEqTo(String other) {
      return getOptStr().isPresent() && getOptStr().get().equals(other);
    }
  }
}

WPI should be able to infer flow-sensitive type refinement annotations. Specifically, WPI should be able to infer the following annotation for OptStringContainer#isStringEqTo:

@EnsuresQualifierIf(result = true, expression = "getOptStr()", qualifier = Present.class)
public boolean isStringEqTo(String other) {
  return getOptStr().isPresent() && getOptStr().get().equals(other);
} 

Given that @Pure is inferred for OptStringContainer#getOptStr

After WPI is able to infer these annotations, running the Optional Checker on the annotated code should output no errors.