"no such method" message when method exists but is private

[mernst]

The Checker Framework issues a "no such method" message when a method exists but is not visible.
It would be better to permit private methods to be used in specifications.

Running the Nullness Checker on the below file yields

NoSuchMethodVisibility.java:15: error: [flowexpr.parse.error] cannot parse the expression [error for expression: privateMap(); error: Invalid 'privateMap' because no such method]
  public boolean isMapped(final String name) {
                 ^
1 error

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

@SuppressWarnings("contracts.conditional.postcondition")
public final class NoSuchMethodVisibility {

  @Pure
  private @Nullable Map<String, Integer> privateMap() {
    return null;
  }

  @EnsuresKeyForIf(expression = "#1", map = "privateMap()", result = true)
  public boolean isMapped(final String name) {
    return true;
  }

  @Pure
  public @Nullable Map<String, Integer> publicMap() {
    return null;
  }

  @EnsuresKeyForIf(expression = "#1", map = "publicMap()", result = true)
  public boolean isMapped2(final String name) {
    return true;
  }
}

[vivek-0509]

Hi @mernst , I investigated this issue and found that it has already been fixed in the current codebase. I verified this by creating a test case that uses a private method in @EnsuresKeyForIf(map = "privateMap()"), and it passes without any errors. This issue can be closed as fixed.

[mernst]

@vivek-0509 Thank you for pointing this out! I have created a pull request with the previously-failing test case, and this issue will be closed when that pull request is merged.

Thanks again for looking into this and noticing that the issue is no longer a problem.