https://checkerframework.org/determinism-checker-manual/manual.html#determinism-qualifiers indicates that @OrderNonDet may be written on a map, but this test case indicates it is not permitted.
import java.util.HashMap;
import org.checkerframework.checker.determinism.qual.*;
public class OrderNonDetMap {
@OrderNonDet HashMap<String, String> primitiveToFieldDescriptor = new @OrderNonDet HashMap<>(8);
}
The Determinism Checker output is:
OrderNonDetMap.java:6: error: [ordernondet.on.noncollection.and.nonarray] @OrderNonDet annotation is invalid for non-collections and non-arrays
@OrderNonDet HashMap<String, String> primitiveToFieldDescriptor = new @OrderNonDet HashMap<>(8);
^
1 error
Also, the caret that indicates a code location appears in a funny place, on the variable name instead of the offending annotation.
https://checkerframework.org/determinism-checker-manual/manual.html#determinism-qualifiers indicates that
@OrderNonDetmay be written on a map, but this test case indicates it is not permitted.The Determinism Checker output is:
Also, the caret that indicates a code location appears in a funny place, on the variable name instead of the offending annotation.