Skip to content

Loop variable doesn't get type refined correctly. #201

@t-rasmud

Description

@t-rasmud

Consider the test case:

import org.checkerframework.checker.determinism.qual.PolyDet;

public class TestLoopVar {
    static void test(@PolyDet int cnt) {
        for (int i = 0; i < cnt; i++) {
            @PolyDet String s1 = String.format("Instruction %d:\n", i);
        }
        for (@PolyDet int j = 0; j < cnt; j++) {
            @PolyDet String s1 = String.format("Instruction %d:\n", j);
        }
    }
}

Running the determinism checker with the command 'javac -processor determinism checker/tests/determinism/TestLoopVar' results in the following error incorrectly:

checker/tests/determinism/TestLoopVar.java:6: error: [assignment.type.incompatible] incompatible types in assignment.
            @PolyDet String s1 = String.format("Instruction %d:\n", i);
                                              ^
  found   : @NonDet String
  required: @PolyDet String
1 error

However, the checker doesn't show the error in the second for loop (Notice that the type of variable j is explicitly annotated as @PolyDet).

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