Repository navigation
Only the first error in a method is reported; later errors in the same method are hidden #428
Description
Impact: real bugs are hidden (false negatives): after the first error in a method, later errors in the same method are not reported, so fixing one bug and re-running is the only way to see the next.
Description
Errors in different methods are all reported, but within one method verification stops at the first error. In one of our benchmark exercises (E_A2_07_PortPairBinder, modelled on a real port-binding bug), two ServerSockets created already bound are bound again in the same method (bulk.bind(...) and health.bind(...)); only the first is reported.
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 twoBugs(Reader a, Reader b) throws IOException {
BufferedReader first = new BufferedReader(a);
first.close();
first.readLine(); // error 1: reported
BufferedReader second = new BufferedReader(b);
second.reset(); // error 2: never marked, not reported
}
}Expected: two State Refinement Errors, at first.readLine() and at second.reset().
Actual: only the first:
State Refinement Error: found closed(first²¹) but expected open(first²¹) || marked(first²¹)
9 | first.readLine(); // error 1: reported
Control: with the two calls in two methods, both are reported.
Suggestion: after reporting a refused call, continue as if the call had succeeded (assume its to state, or the precondition), so later calls are checked against a sensible state rather than cascading errors from the first.
Activity