Skip to content

@RequiresDetToString cannot specify that the receiver must have deterministic toString #224

@t-rasmud

Description

@t-rasmud

Consider the test case below:

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

public class RequiresDetToStringThis {

    public void testPositional() {
        receiverRequired();
    }

    @RequiresDetToString(0)
    public void receiverRequired() {}

    @Override
    public @NonDet String toString(@PolyDet RequiresDetToStringThis this) {
        return this.toString();
    }
}

The method receiverRequired is annotated with @RequiresDetToString(0) which should ideally mean that the receiver
must have a deterministic toString(). In the above code, the class RequiresDetToStringThis has an implementation of toString() that returns @NonDet. Therefore, the above code shouldn't type check.
However, running the command javac -processor determinism checker/tests/determinism/RequiresDetToStringThis.java doesn't report any warning.
It appears that the current implementation of @RequiresDetToString incorrectly uses 0-based indexing for formal parameters and doesn't consider the receiver in its checking.

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