Skip to content

map.get(@PolyDet) should return @PolyDet, for @Det or @OrderNonDet map #212

@mernst

Description

@mernst

I expect the following code to type-check:

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

public class MapGetPoly {

    private static @Det LinkedHashMap<String, Integer> map1 = new @Det LinkedHashMap<>(8);

    private static @OrderNonDet HashMap<String, Integer> map2 = new @OrderNonDet HashMap<>(8);

    public static @PolyDet Integer myGet1(@PolyDet String key) {
        return map1.get(key);
    }

    public static @PolyDet Integer myGet2(@PolyDet String key) {
        return map2.get(key);
    }
}

However, the Determinism Checker issues the following errors:

MapGetPoly.java:9: error: [ordernondet.on.noncollection.and.nonarray] @OrderNonDet annotation is invalid for non-collections and non-arrays
    private static @OrderNonDet HashMap<String, Integer> map2 = new @OrderNonDet HashMap<>(8);
                                                         ^
MapGetPoly.java:12: error: [argument.type.incompatible] incompatible argument for parameter arg0 of get.
        return map1.get(key);
                        ^
  found   : @PolyDet String
  required: @Det Object
MapGetPoly.java:16: error: [argument.type.incompatible] incompatible argument for parameter arg0 of get.
        return map2.get(key);
                        ^
  found   : @PolyDet String
  required: @Det Object
MapGetPoly.java:16: error: [method.invocation.invalid] call to get(java.lang.Object) not allowed on the given receiver.
        return map2.get(key);
                       ^
  found   : @OrderNonDet HashMap
  required: @Det HashMap
4 errors

The error on line 9 is tracked in #211; this issue is about the three errors at the invocations of Map.get.

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