Refine the types of literals

Compile the below file with:
javac -g RefineLiteralType.java -processor nullness -ArequirePrefixInWarningSuppressions -AwarnUnneededSuppressions

More warnings are issued when using manifest literals than a constant variable (m5 vs m6). This is a limitation of the implementation of dataflow: literals have no declared type and thus cannot be refined.

Here is the code:

// Compile this file with:
// javac -g RefineLiteralType.java -processor nullness -ArequirePrefixInWarningSuppressions

import java.util.HashMap;
import java.util.Map;
import org.checkerframework.checker.nullness.qual.EnsuresKeyForIf;
import org.checkerframework.checker.nullness.qual.KeyFor;
import org.checkerframework.dataflow.qual.Pure;

public class RefineLiteralType {

  void m5(Aux aux1, Aux aux2) {
    if (aux1.hasValue(Aux.MINIMUM_VALUE) && aux2.hasValue(Aux.MINIMUM_VALUE)) {
      int minA = aux1.getInt(Aux.MINIMUM_VALUE);
      @SuppressWarnings("keyfor:argument.type.incompatible")
      int minB = aux2.getInt(Aux.MINIMUM_VALUE);
    }
  }

  void m6(Aux aux1, Aux aux2) {
    if (aux1.hasValue("minvalue") && aux2.hasValue("minvalue")) {
      @SuppressWarnings("keyfor:argument.type.incompatible")
      int minA = aux1.getInt("minvalue");
      @SuppressWarnings("keyfor:argument.type.incompatible")
      int minB = aux2.getInt("minvalue");
    }
  }

}

class Aux {

  public Map<String, String> map = new HashMap<>();

  public static final String MINIMUM_VALUE = "minvalue";

  @Pure
  @EnsuresKeyForIf(result = true, expression = "#1", map = "map")
  public boolean hasValue(String key) {
    return map.containsKey(key);
  }

  @Pure
  public int getInt(@KeyFor("this.map") String key) {
    return 22;
  }
}

Start by compiling the inline RefineLiteralType.java example with the supplied javac command and compare warnings in m5 and m6. Trace the dataflow implementation responsible for refining literal types. Done means manifest literals receive the same refinement as the equivalent constant variable and the extra warnings no longer occur.