Repository navigation
Unannotated methods of the same class: a parameter's state is unknown inside, and the method's effect is lost at the call site #429
Description
Impact: a false error inside a helper, and a missed bug at its call site.
Description
A private (or otherwise unannotated) method of the same class that takes a typestate object as a parameter is checked as if the parameter could be in any state, and its effect on the argument is not applied at the call site. In the reproducer:
- inside
rewind,r.reset()is reported ("found true but expected marked(r)") although its only caller marks the reader first; - at the call site,
bris still taken to bemarkedafterrewind(br), so the secondbr.reset(), which throws at run time, is not reported.
The same applies to objects that reach a method by other ways the file shows, e.g. an exception thrown by a method of the same class and caught by its caller: the catch parameter's state is unknown, so every initCause on it is reported, whether or not the thrower had set a cause.
Minimal reproducer (two files)
import liquidjava.specification.ExternalRefinementsFor;
import liquidjava.specification.StateRefinement;
import liquidjava.specification.StateSet;
@ExternalRefinementsFor("java.io.BufferedReader")
@StateSet({"open", "marked", "closed"})
interface BufferedReaderRefinements {
@StateRefinement(to = "open(this)")
void BufferedReader(java.io.Reader in);
@StateRefinement(from = "open(this)")
@StateRefinement(from = "marked(this)")
String readLine();
@StateRefinement(from = "open(this)", to = "marked(this)")
@StateRefinement(from = "marked(this)")
void mark(int readAheadLimit);
@StateRefinement(from = "marked(this)", to = "open(this)")
void reset();
@StateRefinement(from = "!closed(this)", to = "closed(this)")
void close();
}import java.io.BufferedReader;
import java.io.IOException;
import java.io.Reader;
public class Repro {
static void read(Reader in) throws IOException {
BufferedReader br = new BufferedReader(in);
br.mark(100);
rewind(br);
br.reset(); // rewind() already reset br, so it is no longer marked: not reported
}
private static void rewind(BufferedReader r) throws IOException {
r.reset(); // reported: "found true but expected marked(r)", though every caller here marks r first
}
}Expected: no error inside rewind (every caller passes a marked reader), and an error at the second br.reset() in read.
Actual:
State Refinement Error: found true but expected marked(r²⁴)
14 | r.reset(); // reported: "found true but expected marked(r)", though every caller here marks r first
and nothing at line 10.
Possible directions: a way to write the state a parameter needs and leaves (e.g. @StateRefinement(from = "marked(r)", to = "open(r)") on the method), and/or inferring it for private methods of the same class from their bodies and call sites.
Activity