Incorrect unrefinement of Iterator receiver

[t-rasmud]

Consider the following program:

public class TestLegalLoops {
    public void toJSONString(Map map){
        StringBuffer sb = new StringBuffer();
        Iterator iter = map.entrySet().iterator();

        while (iter.hasNext()) {
            sb.append(',');
            Map.Entry entry = (Map.Entry) iter.next();
        }
    }
}

iter.next() is called inside the while loop that checks the condition iter.hasNext() and is therefore safe.
However, running the command javac -processor iteration checker/tests/iteration/TestLegalLoops.java incorrectly results in the following error:

TestLegalLoops.java:32: error: [method.invocation.invalid] call to next() not allowed on the given receiver.
            Map.Entry entry = (Map.Entry) iter.next();
                                                   ^
  found   : @UnknownHasNext Iterator
  required: @HasNext Iterator
1 error

Without the call to sb.append(',');, the above code correctly type checks.

This suggests that the type qualifie of iter is being incorrectly unrefined from @HasNext to @UnknownHasNext after the call to sb.append(',');

[mernst]

append is a side-effecting method. The Checker Framework conservatively assumes that the side effects of append might affect iter, and thus unrefines iter.

It would require additional annotations and reasoning to determine that the side effects of append cannot affect some particular expression (in this case, iter).