diff --git a/liquidjava-example/src/main/java/testSuite/ErrorStateRefinementEveryFrom.java b/liquidjava-example/src/main/java/testSuite/ErrorStateRefinementEveryFrom.java new file mode 100644 index 00000000..6a01b7d3 --- /dev/null +++ b/liquidjava-example/src/main/java/testSuite/ErrorStateRefinementEveryFrom.java @@ -0,0 +1,20 @@ +package testSuite; + +import liquidjava.specification.StateRefinement; +import liquidjava.specification.StateSet; + +// the call needs either entry state: the error declares both, each where its annotation writes it +@StateSet(name = "door", value = {"shut", "ajar", "wide"}) +public class ErrorStateRefinementEveryFrom { + + @StateRefinement(to = "wide(this)") + public ErrorStateRefinementEveryFrom() {} + + @StateRefinement(from = "shut(this)", to = "ajar(this)") + @StateRefinement(from = "ajar(this)", to = "ajar(this)") + public void push() {} + + public static void main(String[] args) { + new ErrorStateRefinementEveryFrom().push(); // Expect: State Refinement Error + } +} diff --git a/liquidjava-verifier/src/main/java/liquidjava/diagnostics/LJDiagnostic.java b/liquidjava-verifier/src/main/java/liquidjava/diagnostics/LJDiagnostic.java index 6224bb67..632096ab 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/diagnostics/LJDiagnostic.java +++ b/liquidjava-verifier/src/main/java/liquidjava/diagnostics/LJDiagnostic.java @@ -70,6 +70,12 @@ public SourcePosition getDeclarationPosition() { return null; } + /** Where each part of the refinement is declared, the first being {@link #getDeclarationPosition()} */ + public List getDeclarationPositions() { + SourcePosition declarationPosition = getDeclarationPosition(); + return declarationPosition == null ? List.of() : List.of(declarationPosition); + } + /** Lines printed under the message that explain it, such as what the names it uses mean */ public List getMessageNotes() { return List.of(); @@ -149,7 +155,7 @@ public String toString() { SourcePosition declPos = getDeclarationPosition(); if (declPos != null && declPos.getFile() != null && !declPos.equals(position)) { sb.append(Colors.CYAN).append("\n--> Refinement declared here:\n").append(Colors.RESET); - String declarationSnippet = getSnippet(declPos, 1, 1, Colors.CYAN, null, true); + String declarationSnippet = getSnippet(getDeclarationPositions(), 1, 1, Colors.CYAN, null, true); if (declarationSnippet != null) { sb.append(declarationSnippet); for (String note : getDeclarationNotes()) @@ -164,22 +170,27 @@ public String toString() { } public String getSnippet() { - return getSnippet(position, 2, 2, accentColor, customMessage, false); + return position == null ? null : getSnippet(List.of(position), 2, 2, accentColor, customMessage, false); } - private String getSnippet(SourcePosition snippetPosition, int contextBefore, int contextAfter, String markerColor, + // One excerpt of the file of the first position, marking each position in that file + private String getSnippet(List positions, int contextBefore, int contextAfter, String markerColor, String markerMessage, boolean firstLineOnly) { - if (snippetPosition == null || snippetPosition.getFile() == null) + if (positions.isEmpty() || positions.get(0).getFile() == null) return null; - Path path = snippetPosition.getFile().toPath(); + Path path = positions.get(0).getFile().toPath(); + List marked = positions.stream() + .filter(p -> p.getFile() != null && p.getFile().toPath().equals(path)).toList(); try { List lines = Files.readAllLines(path); StringBuilder sb = new StringBuilder(); - int startLine = Math.max(1, snippetPosition.getLine() - contextBefore); - int highlightedEndLine = firstLineOnly ? snippetPosition.getLine() : snippetPosition.getEndLine(); - int endLine = Math.min(lines.size(), highlightedEndLine + contextAfter); + int startLine = Math.max(1, + marked.stream().mapToInt(SourcePosition::getLine).min().getAsInt() - contextBefore); + int endLine = Math.min(lines.size(), + marked.stream().mapToInt(p -> highlightedEndLine(p, firstLineOnly)).max().getAsInt() + + contextAfter); // calculate padding for line numbers int padding = String.valueOf(endLine).length(); @@ -193,31 +204,34 @@ private String getSnippet(SourcePosition snippetPosition, int contextBefore, int sb.append(Colors.GREY).append(lineNumStr).append(PIPE).append(line).append(Colors.RESET).append("\n"); // add error markers on the line(s) with the error - if (i >= snippetPosition.getLine() && i <= highlightedEndLine) { - int colStart = (i == snippetPosition.getLine()) ? snippetPosition.getColumn() : 1; - int colEnd = (i == snippetPosition.getEndLine()) ? snippetPosition.getEndColumn() - : rawLine.length(); - - if (colStart > 0 && colEnd > 0) { - int tabsBeforeStart = (int) rawLine.substring(0, Math.max(0, colStart - 1)).chars() - .filter(ch -> ch == '\t').count(); - int tabsBeforeEnd = (int) rawLine.substring(0, Math.max(0, colEnd)).chars() - .filter(ch -> ch == '\t').count(); - int visualColStart = colStart + tabsBeforeStart * 3; - int visualColEnd = colEnd + tabsBeforeEnd * 3; - - // line number padding + pipe + column offset - String indent = " ".repeat(padding) + Colors.GREY + PIPE + Colors.RESET - + " ".repeat(visualColStart - 1); - String markers = markerColor + "^".repeat(Math.max(1, visualColEnd - visualColStart + 1)); - sb.append(indent).append(markers); - - // custom message - if (markerMessage != null && !markerMessage.isBlank()) { - String offset = " ".repeat(padding + visualColEnd + PIPE.length() + 1); - sb.append(" " + markerMessage.replace("\n", "\n" + offset)); + for (SourcePosition snippetPosition : marked) { + int highlightedEndLine = highlightedEndLine(snippetPosition, firstLineOnly); + if (i >= snippetPosition.getLine() && i <= highlightedEndLine) { + int colStart = (i == snippetPosition.getLine()) ? snippetPosition.getColumn() : 1; + int colEnd = (i == snippetPosition.getEndLine()) ? snippetPosition.getEndColumn() + : rawLine.length(); + + if (colStart > 0 && colEnd > 0) { + int tabsBeforeStart = (int) rawLine.substring(0, Math.max(0, colStart - 1)).chars() + .filter(ch -> ch == '\t').count(); + int tabsBeforeEnd = (int) rawLine.substring(0, Math.max(0, colEnd)).chars() + .filter(ch -> ch == '\t').count(); + int visualColStart = colStart + tabsBeforeStart * 3; + int visualColEnd = colEnd + tabsBeforeEnd * 3; + + // line number padding + pipe + column offset + String indent = " ".repeat(padding) + Colors.GREY + PIPE + Colors.RESET + + " ".repeat(visualColStart - 1); + String markers = markerColor + "^".repeat(Math.max(1, visualColEnd - visualColStart + 1)); + sb.append(indent).append(markers); + + // custom message + if (markerMessage != null && !markerMessage.isBlank()) { + String offset = " ".repeat(padding + visualColEnd + PIPE.length() + 1); + sb.append(" " + markerMessage.replace("\n", "\n" + offset)); + } + sb.append(Colors.RESET).append("\n"); } - sb.append(Colors.RESET).append("\n"); } } } @@ -227,6 +241,10 @@ private String getSnippet(SourcePosition snippetPosition, int contextBefore, int } } + private static int highlightedEndLine(SourcePosition position, boolean firstLineOnly) { + return firstLineOnly ? position.getLine() : position.getEndLine(); + } + @Override public boolean equals(Object obj) { if (this == obj) diff --git a/liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/RefinementError.java b/liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/RefinementError.java index 775c740b..8d936d0b 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/RefinementError.java +++ b/liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/RefinementError.java @@ -13,7 +13,6 @@ import liquidjava.diagnostics.AliasExpansion; import liquidjava.diagnostics.TranslationTable; import liquidjava.diagnostics.categories.ErrorCategory; -import liquidjava.diagnostics.hints.Hint; import liquidjava.processor.context.AliasWrapper; import liquidjava.rj_language.Predicate; import liquidjava.rj_language.ast.BinaryExpression; @@ -54,7 +53,7 @@ public RefinementError(SourcePosition position, SourcePosition declarationPositi String customMessage, List aliases) { super("Refinement Error", ErrorMessage.of(expected.getExpression(), found, translationTable, shown -> !isTrue(shown), - "%s is not a subtype of %s", UnaryOperator.identity()), + "found %s but expected %s", UnaryOperator.identity()), position, translationTable, customMessage); this.expected = expected; this.found = found; @@ -72,9 +71,6 @@ public RefinementError(SourcePosition position, SourcePosition declarationPositi setCounterexampleStr("Counterexample: " + counterexampleString); } setCategory(categoryOf(expected, found)); - if (isTrue(found.getImplication().toPredicate().getExpression())) - addHint(Hint.general( - "Not enough information to prove the expected refinement. Add a refinement or condition to constrain it.")); } // Each alias the message uses once, with those their definitions use, as declared diff --git a/liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/StateRefinementError.java b/liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/StateRefinementError.java index 139ebba9..9bfd22f3 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/StateRefinementError.java +++ b/liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/StateRefinementError.java @@ -24,25 +24,27 @@ public class StateRefinementError extends LJError { private final Predicate expected; private final VCSimplificationResult found; - private final SourcePosition declarationPosition; + private final List declarationPositions; private final StateErrorContext context; private final List declarationNotes; /** + * @param declarationPositions + * where each entry state that makes up expected is declared * @param display * rewrites expected and found as the error shows them, here and to the IDE, after the facts to show are * chosen on them as given * @param declarationNotes * lines that explain the declaration, printed under its excerpt */ - public StateRefinementError(SourcePosition position, SourcePosition declarationPosition, Predicate expected, + public StateRefinementError(SourcePosition position, List declarationPositions, Predicate expected, VCSimplificationResult found, TranslationTable translationTable, String customMessage, List hints, ErrorCategory category, StateErrorContext context, UnaryOperator display, List declarationNotes) { super("State Refinement Error", ErrorMessage.of(expected.getExpression(), found, translationTable, StateRefinementError::appliesGhost, "found %s but expected %s", display), position, translationTable, customMessage); - this.declarationPosition = declarationPosition; + this.declarationPositions = declarationPositions; this.expected = new Predicate(display.apply(expected.getExpression())); this.found = found.map(display); this.context = context; @@ -68,7 +70,12 @@ public List getDeclarationNotes() { @Override public SourcePosition getDeclarationPosition() { - return declarationPosition; + return declarationPositions.isEmpty() ? null : declarationPositions.get(0); + } + + @Override + public List getDeclarationPositions() { + return declarationPositions; } public Predicate getExpected() { diff --git a/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/TypeChecker.java b/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/TypeChecker.java index 44af4d58..7d53e0d1 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/TypeChecker.java +++ b/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/TypeChecker.java @@ -613,14 +613,14 @@ public void throwRefinementError(SourcePosition position, SourcePosition declara public void throwStateRefinementError(SourcePosition position, SourcePosition declarationPosition, Predicate found, Predicate expected, String customMessage) throws LJError { - throwStateRefinementError(position, declarationPosition, found, expected, customMessage, List.of(), null, null, - List.of()); + throwStateRefinementError(position, List.of(declarationPosition), found, expected, customMessage, List.of(), + null, null, List.of()); } - public void throwStateRefinementError(SourcePosition position, SourcePosition declarationPosition, Predicate found, - Predicate expected, String customMessage, List hints, ErrorCategory category, + public void throwStateRefinementError(SourcePosition position, List declarationPositions, + Predicate found, Predicate expected, String customMessage, List hints, ErrorCategory category, StateErrorContext context, List declarationNotes) throws LJError { - vcChecker.throwStateRefinementError(position, declarationPosition, found, expected, customMessage, hints, + vcChecker.throwStateRefinementError(position, declarationPositions, found, expected, customMessage, hints, category, context, declarationNotes); } diff --git a/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/VCChecker.java b/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/VCChecker.java index 84d285e4..c9e2dc53 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/VCChecker.java +++ b/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/VCChecker.java @@ -455,7 +455,7 @@ protected Predicate shownFound(Predicate found, Predicate expected) { return buildPremiseChain(new TranslationTable(), expected, found).simplify().getImplication().toPredicate(); } - protected void throwStateRefinementError(SourcePosition position, SourcePosition declarationPosition, + protected void throwStateRefinementError(SourcePosition position, List declarationPositions, Predicate found, Predicate expected, String customMessage, List hints, ErrorCategory category, StateErrorContext context, List declarationNotes) throws StateRefinementError { TranslationTable map = new TranslationTable(); @@ -463,7 +463,7 @@ protected void throwStateRefinementError(SourcePosition position, SourcePosition VCSimplificationResult simplified = foundState.simplify(NeededVariables.forStateError(expected)); VCSimplificationResult shown = VCSimplification.simplifyOnce(simplified, new VCRelevantFacts(expected.getExpression(), this::ghostFunctionsOf)); - throw new StateRefinementError(position, declarationPosition, expected, shown, map, customMessage, hints, + throw new StateRefinementError(position, declarationPositions, expected, shown, map, customMessage, hints, category, context, e -> StateValues.toSetForm(e, this.context.getGhostStates(), this.context.getGhosts()), declarationNotes); diff --git a/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/object_checkers/AuxStateHandler.java b/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/object_checkers/AuxStateHandler.java index 6c1d7167..b7497657 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/object_checkers/AuxStateHandler.java +++ b/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/object_checkers/AuxStateHandler.java @@ -417,13 +417,13 @@ private static ObjectState getStates(CtAnnotation ctAnnota Predicate written = new Predicate(from, e, prefix); state.setWrittenFrom(written); state.setFrom(createStatePredicate(written, from, f.getTargetClass(), tc, e, false)); - state.setFromPosition(Utils.getLJAnnotationPosition(e, from)); + state.setFromPosition(valuePosition(m.get("from"), e, from)); } // has to if (to != null) { state.setTo(createStatePredicate(new Predicate(to, e, prefix), to, f.getTargetClass(), tc, e, true)); - state.setToPosition(Utils.getLJAnnotationPosition(e, to)); + state.setToPosition(valuePosition(m.get("to"), e, to)); } // has to but not from, state enters with true @@ -433,6 +433,12 @@ private static ObjectState getStates(CtAnnotation ctAnnota return state; } + // Where this annotation writes a literal value, since another annotation of the element may write the same text + private static SourcePosition valuePosition(CtExpression value, CtElement element, String written) { + SourcePosition position = value instanceof CtLiteral ? Utils.getAnnotationValuePosition(value) : null; + return position != null ? position : Utils.getLJAnnotationPosition(element, written); + } + /** * Creates the predicate for state transition * @@ -796,12 +802,16 @@ private static void changeState(TypeChecker tc, VariableInstance vi, RefinedFunc // combine messages of all state changes String message = stateChanges.stream().map(ObjectState::getMessage) .filter(msg -> msg != null && !msg.isBlank()).distinct().collect(Collectors.joining("\n")); - Optional declaration = stateChanges.stream().filter(ObjectState::hasFrom) - .filter(s -> s.getFromPosition() != null).findFirst(); - SourcePosition declarationPosition = declaration.map(ObjectState::getFromPosition) - .orElse(function.getPlacementInCode().getPosition()); - List declarationNotes = declaration.map(ObjectState::getWrittenFrom).filter(Objects::nonNull) - .map(written -> declarationNotes(written.getExpression(), tc.getContext())).orElse(List.of()); + // every entry state that makes up expected, each with what its states mean + List declarations = stateChanges.stream().filter(ObjectState::hasFrom) + .filter(s -> s.getFromPosition() != null).toList(); + List declarationPositions = declarations.isEmpty() + ? List.of(function.getPlacementInCode().getPosition()) + : declarations.stream().map(ObjectState::getFromPosition).toList(); + List declarationNotes = declarations.stream().map(ObjectState::getWrittenFrom) + .filter(Objects::nonNull) + .flatMap(written -> declarationNotes(written.getExpression(), tc.getContext()).stream()).distinct() + .toList(); List ghostStates = getGhostStatesFor(function.getTargetClass(), tc); Optional deciding = decidingArgument(tc, vi, function, ghostStates, invocation); Optional states = receiverStates(tc, function, vi, prevState, invocation); @@ -817,7 +827,7 @@ private static void changeState(TypeChecker tc, VariableInstance vi, RefinedFunc StateErrorContext context = states .map(r -> StateErrorContext.of(r.machine(), function, r.current(), writtenReceiver(invocation))) .orElse(null); - tc.throwStateRefinementError(invocation.getPosition(), declarationPosition, prevState, + tc.throwStateRefinementError(invocation.getPosition(), declarationPositions, prevState, expectedStatesDisjunction, message, hints, category, context, declarationNotes); } } diff --git a/liquidjava-verifier/src/test/java/liquidjava/api/tests/TestDeclarationPositions.java b/liquidjava-verifier/src/test/java/liquidjava/api/tests/TestDeclarationPositions.java index fde8bdd5..8fc733d9 100644 --- a/liquidjava-verifier/src/test/java/liquidjava/api/tests/TestDeclarationPositions.java +++ b/liquidjava-verifier/src/test/java/liquidjava/api/tests/TestDeclarationPositions.java @@ -41,6 +41,29 @@ void declarationsCoverReturnsParametersLocalsAndFields() throws IOException { assertDeclarations("ErrorRefinementDeclarationPositions.java", "_ > 20", "_ > 30", "_ > 40", "_ > 10"); } + @Test + void stateErrorPointsToEveryEntryStateWithWhatItMeans() throws IOException { + Path path = Path.of("../liquidjava-example/src/main/java/testSuite/ErrorStateRefinementEveryFrom.java") + .toRealPath(); + String source = Files.readString(path); + CommandLineLauncher.launch(path.toString()); + List errors = List.copyOf(Diagnostics.getInstance().getErrors()); + + assertEquals(1, errors.size()); + List positions = errors.get(0).getDeclarationPositions(); + assertEquals(2, positions.size()); + assertPosition(positions.get(0), path, fromStart(source, "shut(this)"), "shut(this)"); + // the second annotation's from, not the same text the first writes as its to + assertPosition(positions.get(1), path, fromStart(source, "ajar(this)"), "ajar(this)"); + String notes = " where shut(this) means door(this) == shut\n where ajar(this) means door(this) == ajar\n"; + assertTrue(errors.get(0).toString().contains(notes)); + } + + private static int fromStart(String source, String from) { + String written = "from = \""; + return source.indexOf(written + from + "\"") + written.length(); + } + private static void assertDeclarations(String file, String... predicates) throws IOException { Path path = Path.of("../liquidjava-example/src/main/java/testSuite/", file).toRealPath(); String source = Files.readString(path); @@ -61,6 +84,11 @@ private static void assertPredicatePosition(SourcePosition position, Path file, assertTrue(position.isValidPosition(), "Invalid refinement declaration position"); int start = source.indexOf("\"" + predicate + "\"") + 1; assertTrue(start > 0, "Predicate not found in fixture: " + predicate); + assertPosition(position, file, start, predicate); + } + + private static void assertPosition(SourcePosition position, Path file, int start, String predicate) + throws IOException { assertEquals(start, position.getSourceStart()); assertEquals(start + predicate.length() - 1, position.getSourceEnd()); assertEquals(file, position.getFile().toPath().toRealPath()); diff --git a/liquidjava-verifier/src/test/java/liquidjava/api/tests/TestFoundBinders.java b/liquidjava-verifier/src/test/java/liquidjava/api/tests/TestFoundBinders.java index ae883369..bd9e2ea9 100644 --- a/liquidjava-verifier/src/test/java/liquidjava/api/tests/TestFoundBinders.java +++ b/liquidjava-verifier/src/test/java/liquidjava/api/tests/TestFoundBinders.java @@ -63,7 +63,7 @@ void issueReproducerDropsTheTrueFieldRow() { @Test void callArgumentIsWrittenAsTheCallerWroteIt() { Shown shown = ERRORS.get(79); - assertEquals("count() >= 0 is not a subtype of count() > 0", shown.message()); + assertEquals("found count() >= 0 but expected count() > 0", shown.message()); assertEquals("Counterexample: count() == 0", shown.counterexample()); } @@ -100,7 +100,7 @@ void variableOnlyExpectedNamesKeepsItsTrueRow() { @Test void writeToAnotherObjectsFieldIsNamedAfterThatObject() { - assertEquals("other.level == -1 is not a subtype of other.level >= 0", ERRORS.get(36).message()); + assertEquals("found other.level == -1 but expected other.level >= 0", ERRORS.get(36).message()); assertEquals(List.of("∀this.level this.level >= 0", "∀other.level other.level == this.level - 1"), ERRORS.get(48).rows()); } @@ -108,7 +108,7 @@ void writeToAnotherObjectsFieldIsNamedAfterThatObject() { @Test void earlierValuesOfAVariableAreWrittenWithTheirLine() { Shown shown = ERRORS.get(86); - assertEquals("b@86 == 8 && b@86 > 0 && b == -b@86 is not a subtype of b > 0", shown.message()); + assertEquals("found b@86 == 8 && b@86 > 0 && b == -b@86 but expected b > 0", shown.message()); assertEquals("Counterexample: b == -8", shown.counterexample()); assertEquals(List.of("∀b@85 b@85 == 8", "∀b@86 b@86 == b@85 && b@86 > 0", "∀b b == -b@86"), shown.originalRows()); diff --git a/liquidjava-verifier/src/test/java/liquidjava/api/tests/TestStaticConstantNames.java b/liquidjava-verifier/src/test/java/liquidjava/api/tests/TestStaticConstantNames.java index c5aaaf92..627b09c5 100644 --- a/liquidjava-verifier/src/test/java/liquidjava/api/tests/TestStaticConstantNames.java +++ b/liquidjava-verifier/src/test/java/liquidjava/api/tests/TestStaticConstantNames.java @@ -36,7 +36,7 @@ void constantPassedThroughLocalKeepsItsName() { } private static void assertShowsName(RefinementError error) { - assertEquals("mode == ImageWriteParam.MODE_EXPLICIT is not a subtype of mode != ImageWriteParam.MODE_EXPLICIT", + assertEquals("found mode == ImageWriteParam.MODE_EXPLICIT but expected mode != ImageWriteParam.MODE_EXPLICIT", error.getMessage().replaceAll("[⁰¹²³⁴⁵⁶⁷⁸⁹]", "")); assertTrue(error.getCounterexample().isEmpty()); } diff --git a/liquidjava-verifier/src/test/java/liquidjava/diagnostics/errors/RefinementErrorCounterexampleTest.java b/liquidjava-verifier/src/test/java/liquidjava/diagnostics/errors/RefinementErrorCounterexampleTest.java index ffb487cc..7a764efe 100644 --- a/liquidjava-verifier/src/test/java/liquidjava/diagnostics/errors/RefinementErrorCounterexampleTest.java +++ b/liquidjava-verifier/src/test/java/liquidjava/diagnostics/errors/RefinementErrorCounterexampleTest.java @@ -123,24 +123,31 @@ void messageSaysExpectedCouldNotBeProvedWhenFoundOnlyGuardsOtherVariables() { assertEquals("expected timeout >= 0 but could not prove it", error.getMessage()); } + @Test + void messageWithNothingFoundGivesNoHint() { + RefinementError error = error("timeout >= 0", vc("∀timeout:int. true", "true"), "timeout=-1"); + assertEquals("expected timeout >= 0 but could not prove it", error.getMessage()); + assertTrue(error.getHints().isEmpty()); + } + @Test void messageKeepsOnlyTheGuardsLinkedToExpected() { RefinementError error = error("t >= 0", vc("∀port:int. true", "∀retries:int. true", "∀t:int. true", "∀##if_condition_1:boolean. !(port < 0 || retries > t)", "true"), "port=0", "retries=-2", "t=-1"); - assertEquals("!(retries > t) is not a subtype of t >= 0", error.getMessage()); + assertEquals("found !(retries > t) but expected t >= 0", error.getMessage()); } @Test void messageKeepsFoundAsWrittenWhenEveryFactIsLinked() { RefinementError error = error("x >= 0", vc("∀x:int. !(x < 0 || x > 5)", "true"), "x=-1"); - assertEquals("!(x < 0 || x > 5) is not a subtype of x >= 0", error.getMessage()); + assertEquals("found !(x < 0 || x > 5) but expected x >= 0", error.getMessage()); } @Test void stateMessageKeepsAStateReachingExpectedThroughAnAlias() { - StateRefinementError error = new StateRefinementError(null, null, + StateRefinementError error = new StateRefinementError(null, List.of(), new Predicate(RefinementsParser.createAST("full(box)", "")), new VCSimplificationResult( vc("∀b1:Object. empty(b1)", "∀x:int. x > 0", "∀box:Object. box == b1", "true")),