Refine the types of literals

[mernst]

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;
  }
}