Skip to content

get on Map with @NonDet key is not permitted #197

@mernst

Description

@mernst

I expected it to be legal to call Map.get with a @NonDet key. I expected it to return a @NonDet result. However, it is forbidden.

Here is a test case:

import java.util.*;
import org.checkerframework.checker.determinism.qual.*;

public class Issue197 {
    public @Det Integer getDet(
            @OrderNonDet HashMap<@Det String, @Det Integer> map, @Det String key) {
        return map.get(key);
    }

    public @NonDet Integer getNonDet(
            @OrderNonDet HashMap<@Det String, @Det Integer> map, @NonDet String key) {
        return map.get(key);
    }

    public @PolyDet Integer getPolyDet(
            @OrderNonDet HashMap<@Det String, @Det Integer> map, @PolyDet String key) {
        return map.get(key);
    }
}

The Determinism Checker produces these error messages:

Issue197.java:12: error: [method.invocation.invalid] call to get(java.lang.Object) not allowed on the given receiver.
        return map.get(key);
                      ^
  found   : @OrderNonDet HashMap
  required: @NonDet HashMap
Issue197.java:17: error: [return.type.incompatible] incompatible types in return.
        return map.get(key);
                      ^
  type of expression: @NonDet Integer
  method return type: @PolyDet Integer
Issue197.java:17: error: [method.invocation.invalid] call to get(java.lang.Object) not allowed on the given receiver.
        return map.get(key);
                      ^
  found   : @OrderNonDet HashMap
  required: @NonDet HashMap
3 errors

Possibly related: #193.

Metadata

Metadata

Assignees

No one assigned

    Labels

    No labels
    No labels

    Projects

    No projects

    Milestone

    No milestone

    Relationships

    None yet

    Development

    No branches or pull requests

    Issue actions