Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Incorrect treatment of @PolyDet("upDet") iteration #180

Open
jwaataja opened this issue Apr 24, 2020 · 1 comment
Open

Incorrect treatment of @PolyDet("upDet") iteration #180

jwaataja opened this issue Apr 24, 2020 · 1 comment

Comments

@jwaataja
Copy link
Collaborator

Iterating through a HashSet should always give @NonDet elements. Consider the following code.

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

public class C {
    void f(@PolyDet List<@PolyDet String> list) {
        @PolyDet("upDet") Set<@PolyDet String> set = new HashSet<>(list);
        for (String elt : set) {
            @PolyDet("up") String s = elt;
        }
    }
}

This code typechecks because the type of elt is @PolyDet("up"). This is unsound because the type of elt should be @NonDet as it's from iterating over a HashSet.

@jwaataja
Copy link
Collaborator Author

jwaataja commented May 1, 2020

Seems to be fixed in e9403e1.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

No branches or pull requests

1 participant