From 3087b6268f8348aaf11f66f9d30b0c6cca257391 Mon Sep 17 00:00:00 2001 From: Catarina Gamboa Date: Tue, 10 Nov 2026 15:10:49 +0000 Subject: [PATCH 1/2] Use found ... but expected ... for refinement errors and declare every entry state Refinement errors now use the same headline frame as state errors, found X but expected Y, instead of "X is not a subtype of Y". An empty found keeps "expected Y but could not prove it", without the general hint to add a refinement or condition, which pointed away from the fix. When a call has several @StateRefinement entry states, the declared-here excerpt marks every from that makes up expected, each with its where line. Each from is located in its own annotation, not at the first annotation that writes the same text. Co-Authored-By: Claude Opus 5.5 --- .../ErrorStateRefinementEveryFrom.java | 20 +++++ .../liquidjava/diagnostics/LJDiagnostic.java | 82 +++++++++++-------- .../diagnostics/errors/RefinementError.java | 6 +- .../errors/StateRefinementError.java | 15 +++- .../refinement_checker/TypeChecker.java | 10 +-- .../refinement_checker/VCChecker.java | 4 +- .../object_checkers/AuxStateHandler.java | 28 +++++-- .../api/tests/TestDeclarationPositions.java | 28 +++++++ .../api/tests/TestFoundBinders.java | 6 +- .../api/tests/TestStaticConstantNames.java | 2 +- .../RefinementErrorCounterexampleTest.java | 13 ++- 11 files changed, 150 insertions(+), 64 deletions(-) create mode 100644 liquidjava-example/src/main/java/testSuite/ErrorStateRefinementEveryFrom.java 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..5b473582 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 the value, as another annotation of the element may write the same text + private static SourcePosition valuePosition(CtExpression value, CtElement element, String written) { + SourcePosition position = Utils.getAnnotationValuePosition(value); + 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")), From 9d1bb1e7c90f1f7d01849cd6178e98a804d4a720 Mon Sep 17 00:00:00 2001 From: Catarina Gamboa Date: Tue, 10 Nov 2026 15:16:08 +0000 Subject: [PATCH 2/2] Locate only a literal state value by its own position A concatenated value falls back to the text search, as before. Co-Authored-By: Claude Opus 5.5 --- .../refinement_checker/object_checkers/AuxStateHandler.java | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) 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 5b473582..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 @@ -433,9 +433,9 @@ private static ObjectState getStates(CtAnnotation ctAnnota return state; } - // Where this annotation writes the value, as another annotation of the element may write the same text + // 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 = Utils.getAnnotationValuePosition(value); + SourcePosition position = value instanceof CtLiteral ? Utils.getAnnotationValuePosition(value) : null; return position != null ? position : Utils.getLJAnnotationPosition(element, written); }