checker/tests/nullness/KeyForLocalSideEffect.java

import java.util.HashMap;
import org.checkerframework.checker.nullness.qual.*;

public class KeyForLocalSideEffect {

  String k = "key";
  HashMap<String, Integer> m = new HashMap<>();

  void testContainsKeyForFieldKeyAndLocalMap() {
    HashMap<String, Integer> m_local = m;

    if (m_local.containsKey(k)) {
      @KeyFor("m_local") String s = k;
      havoc();
      // TODO: This should be an error, because s is no longer a key for m_local.
      @NonNull Integer val = m_local.get(s);
    }
  }

  void havoc() {
    m = new HashMap<>();
  }
}