From 618c5b58df9d68fa8c071cf23fe3ea378eae0a5f Mon Sep 17 00:00:00 2001 From: Ricardo Costa Date: Thu, 5 Feb 2026 15:38:47 +0000 Subject: [PATCH 1/3] Add Custom Messages --- .../liquidjava/specification/Refinement.java | 2 ++ .../specification/StateRefinement.java | 6 ++-- .../liquidjava/diagnostics/LJDiagnostic.java | 19 +++++++++-- .../diagnostics/errors/LJError.java | 7 +++- .../diagnostics/errors/RefinementError.java | 4 +-- .../errors/StateRefinementError.java | 4 +-- .../diagnostics/warnings/LJWarning.java | 2 +- .../processor/context/ObjectState.java | 17 +++++++++- .../liquidjava/processor/context/Refined.java | 9 +++++ .../RefinementTypeChecker.java | 9 ++--- .../refinement_checker/TypeChecker.java | 34 ++++++++++++++----- .../refinement_checker/VCChecker.java | 21 +++++++----- .../MethodsFunctionsChecker.java | 6 ++-- .../AuxHierarchyRefinementsPassage.java | 2 +- .../object_checkers/AuxStateHandler.java | 18 +++++++--- 15 files changed, 121 insertions(+), 39 deletions(-) diff --git a/liquidjava-api/src/main/java/liquidjava/specification/Refinement.java b/liquidjava-api/src/main/java/liquidjava/specification/Refinement.java index ce3dc20a..85aff527 100644 --- a/liquidjava-api/src/main/java/liquidjava/specification/Refinement.java +++ b/liquidjava-api/src/main/java/liquidjava/specification/Refinement.java @@ -16,4 +16,6 @@ public @interface Refinement { public String value(); + + public String msg() default ""; } diff --git a/liquidjava-api/src/main/java/liquidjava/specification/StateRefinement.java b/liquidjava-api/src/main/java/liquidjava/specification/StateRefinement.java index b652944b..18a57fe3 100644 --- a/liquidjava-api/src/main/java/liquidjava/specification/StateRefinement.java +++ b/liquidjava-api/src/main/java/liquidjava/specification/StateRefinement.java @@ -7,9 +7,9 @@ import java.lang.annotation.Target; /** - * Annotation to create state transitions in a method. The annotation has two arguments: from : the + * Annotation to create state transitions in a method. The annotation has three arguments: from : the * state in which the object needs to be for the method to be invoked correctly to : the state in - * which the object will be after the execution of the method + * which the object will be after the execution of the method msg : optional custom error message to display when refinement is violated * e.g. @StateRefinement(from="open(this)", to="closed(this)") * * @author catarina gamboa @@ -21,4 +21,6 @@ public String from() default ""; public String to() default ""; + + public String msg() default ""; } diff --git a/liquidjava-verifier/src/main/java/liquidjava/diagnostics/LJDiagnostic.java b/liquidjava-verifier/src/main/java/liquidjava/diagnostics/LJDiagnostic.java index 245c53d8..0b22de75 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/diagnostics/LJDiagnostic.java +++ b/liquidjava-verifier/src/main/java/liquidjava/diagnostics/LJDiagnostic.java @@ -11,15 +11,17 @@ public class LJDiagnostic extends RuntimeException { private final String title; private final String message; private final String accentColor; + private final String customMessage; private String file; private ErrorPosition position; - public LJDiagnostic(String title, String message, SourcePosition pos, String accentColor) { + public LJDiagnostic(String title, String message, SourcePosition pos, String accentColor, String customMessage) { this.title = title; this.message = message; this.file = (pos != null && pos.getFile() != null) ? pos.getFile().getPath() : null; this.position = ErrorPosition.fromSpoonPosition(pos); this.accentColor = accentColor; + this.customMessage = customMessage; } public String getTitle() { @@ -30,6 +32,10 @@ public String getMessage() { return message; } + public String getCustomMessage() { + return customMessage; + } + public String getDetails() { return ""; // to be overridden by subclasses } @@ -115,8 +121,15 @@ public String getSnippet() { // line number padding + " | " + column offset String indent = " ".repeat(padding) + Colors.GREY + " | " + Colors.RESET + " ".repeat(colStart - 1); - String markers = accentColor + "^".repeat(Math.max(1, colEnd - colStart + 1)) + Colors.RESET; - sb.append(indent).append(markers).append("\n"); + String markers = accentColor + "^".repeat(Math.max(1, colEnd - colStart + 1)); + sb.append(indent).append(markers); + + // custom message + if (customMessage != null && !customMessage.isBlank()) { + sb.append(" " + customMessage); + } + + sb.append(Colors.RESET).append("\n"); } } } diff --git a/liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/LJError.java b/liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/LJError.java index e3fd5599..66ff9fd2 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/LJError.java +++ b/liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/LJError.java @@ -13,7 +13,12 @@ public abstract class LJError extends LJDiagnostic { private final TranslationTable translationTable; public LJError(String title, String message, SourcePosition pos, TranslationTable translationTable) { - super(title, message, pos, Colors.BOLD_RED); + this(title, message, pos, translationTable, null); + } + + public LJError(String title, String message, SourcePosition pos, TranslationTable translationTable, + String customMessage) { + super(title, message, pos, Colors.BOLD_RED, customMessage); this.translationTable = translationTable != null ? translationTable : new TranslationTable(); } 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 93a8a447..de40bd7f 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/RefinementError.java +++ b/liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/RefinementError.java @@ -16,9 +16,9 @@ public class RefinementError extends LJError { private final ValDerivationNode found; public RefinementError(SourcePosition position, ValDerivationNode expected, ValDerivationNode found, - TranslationTable translationTable) { + TranslationTable translationTable, String customMessage) { super("Refinement Error", String.format("%s is not a subtype of %s", found.getValue(), expected.getValue()), - position, translationTable); + position, translationTable, customMessage); this.expected = expected; this.found = found; } 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 508e6087..df7a54c4 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/StateRefinementError.java +++ b/liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/StateRefinementError.java @@ -15,9 +15,9 @@ public class StateRefinementError extends LJError { private final String found; public StateRefinementError(SourcePosition position, Expression expected, Expression found, - TranslationTable translationTable) { + TranslationTable translationTable, String customMessage) { super("State Refinement Error", String.format("Expected state %s but found %s", expected.toSimplifiedString(), - found.toSimplifiedString()), position, translationTable); + found.toSimplifiedString()), position, translationTable, customMessage); this.expected = expected.toSimplifiedString(); this.found = found.toSimplifiedString(); } diff --git a/liquidjava-verifier/src/main/java/liquidjava/diagnostics/warnings/LJWarning.java b/liquidjava-verifier/src/main/java/liquidjava/diagnostics/warnings/LJWarning.java index 29d65479..5f5f0633 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/diagnostics/warnings/LJWarning.java +++ b/liquidjava-verifier/src/main/java/liquidjava/diagnostics/warnings/LJWarning.java @@ -10,6 +10,6 @@ public abstract class LJWarning extends LJDiagnostic { public LJWarning(String message, SourcePosition pos) { - super("Warning", message, pos, Colors.BOLD_YELLOW); + super("Warning", message, pos, Colors.BOLD_YELLOW, null); } } diff --git a/liquidjava-verifier/src/main/java/liquidjava/processor/context/ObjectState.java b/liquidjava-verifier/src/main/java/liquidjava/processor/context/ObjectState.java index 795e9815..45ac6c68 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/processor/context/ObjectState.java +++ b/liquidjava-verifier/src/main/java/liquidjava/processor/context/ObjectState.java @@ -6,6 +6,7 @@ public class ObjectState { Predicate from; Predicate to; + String message; public ObjectState() { } @@ -15,6 +16,12 @@ public ObjectState(Predicate from, Predicate to) { this.to = to; } + public ObjectState(Predicate from, Predicate to, String message) { + this.from = from; + this.to = to; + this.message = message; + } + public void setFrom(Predicate from) { this.from = from; } @@ -39,8 +46,16 @@ public Predicate getTo() { return to != null ? to : new Predicate(); } + public String getMessage() { + return message; + } + + public void setMessage(String message) { + this.message = message; + } + public ObjectState clone() { - return new ObjectState(from.clone(), to.clone()); + return new ObjectState(from.clone(), to.clone(), message); } @Override diff --git a/liquidjava-verifier/src/main/java/liquidjava/processor/context/Refined.java b/liquidjava-verifier/src/main/java/liquidjava/processor/context/Refined.java index 6028d521..2aa03989 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/processor/context/Refined.java +++ b/liquidjava-verifier/src/main/java/liquidjava/processor/context/Refined.java @@ -8,6 +8,7 @@ public abstract class Refined { private String name; // y private CtTypeReference type; // int private Predicate refinement; // 9 <= y && y <= 100 + private String message; public Refined() { } @@ -44,6 +45,14 @@ public Predicate getRefinement() { return new Predicate(); } + public String getMessage() { + return message; + } + + public void setMessage(String message) { + this.message = message; + } + public Predicate getRenamedRefinements(String toReplace) { return refinement.substituteVariable(name, toReplace); } diff --git a/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/RefinementTypeChecker.java b/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/RefinementTypeChecker.java index 43791ccd..d4d6f89e 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/RefinementTypeChecker.java +++ b/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/RefinementTypeChecker.java @@ -124,10 +124,10 @@ public void visitCtLocalVariable(CtLocalVariable localVariable) { super.visitCtLocalVariable(localVariable); // only declaration, no assignment if (localVariable.getAssignment() == null) { - Optional a; - a = getRefinementFromAnnotation(localVariable); - context.addVarToContext(localVariable.getSimpleName(), localVariable.getType(), a.orElse(new Predicate()), - localVariable); + Optional a = getRefinementFromAnnotation(localVariable); + RefinedVariable v = context.addVarToContext(localVariable.getSimpleName(), localVariable.getType(), + a.orElse(new Predicate()), localVariable); + getMessageFromAnnotation(localVariable).ifPresent(v::setMessage); } else { String varName = localVariable.getSimpleName(); CtExpression e = localVariable.getAssignment(); @@ -238,6 +238,7 @@ public void visitCtField(CtField f) { ret = c.get().substituteVariable(Keys.WILDCARD, name).substituteVariable(f.getSimpleName(), name); } RefinedVariable v = context.addVarToContext(name, f.getType(), ret, f); + getMessageFromAnnotation(f).ifPresent(v::setMessage); if (v instanceof Variable) { ((Variable) v).setLocation("this"); } 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 e154a3dc..73d68e25 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 @@ -89,6 +89,19 @@ public Optional getRefinementFromAnnotation(CtElement element) throws return constr; } + public Optional getMessageFromAnnotation(CtElement element) { + for (CtAnnotation ann : element.getAnnotations()) { + String an = ann.getActualAnnotation().annotationType().getCanonicalName(); + if (an.contentEquals("liquidjava.specification.Refinement")) { + String msg = getStringFromAnnotation(ann.getValue("msg")); + if (msg != null && !msg.isEmpty()) { + return Optional.of(msg); + } + } + } + return Optional.empty(); + } + @SuppressWarnings("unchecked") public void handleStateSetsFromAnnotation(CtElement element) throws LJError { int set = 0; @@ -277,13 +290,17 @@ public void checkVariableRefinements(Predicate refinementFound, String simpleNam for (CtTypeReference t : mainRV.getSuperTypes()) rv.addSuperType(t); context.addRefinementInstanceToVariable(simpleName, newName); - // smt check - checkSMT(cEt, usage); // TODO CHANGE + String customMessage = getMessageFromAnnotation(variable).orElse(mainRV != null ? mainRV.getMessage() : null); + checkSMT(cEt, usage, customMessage); // TODO CHANGE context.addRefinementToVariableInContext(simpleName, type, cet, usage); } public void checkSMT(Predicate expectedType, CtElement element) throws LJError { - vcChecker.processSubtyping(expectedType, context.getGhostState(), element, factory); + checkSMT(expectedType, element, null); + } + + public void checkSMT(Predicate expectedType, CtElement element, String customMessage) throws LJError { + vcChecker.processSubtyping(expectedType, context.getGhostState(), element, factory, customMessage); element.putMetadata(Keys.REFINEMENT, expectedType); } @@ -296,13 +313,14 @@ public boolean checksStateSMT(Predicate prevState, Predicate expectedState, Sour return vcChecker.canProcessSubtyping(prevState, expectedState, context.getGhostState(), p, factory); } - public void throwRefinementError(SourcePosition position, Predicate expectedType, Predicate foundType) - throws LJError { - vcChecker.throwRefinementError(position, expectedType, foundType); + public void throwRefinementError(SourcePosition position, Predicate expectedType, Predicate foundType, + String customMessage) throws LJError { + vcChecker.throwRefinementError(position, expectedType, foundType, customMessage); } - public void throwStateRefinementError(SourcePosition position, Predicate found, Predicate expected) throws LJError { - vcChecker.throwStateRefinementError(position, found, expected); + public void throwStateRefinementError(SourcePosition position, Predicate found, Predicate expected, + String customMessage) throws LJError { + vcChecker.throwStateRefinementError(position, found, expected, customMessage); } public void throwStateConflictError(SourcePosition position, Predicate expectedType) throws LJError { 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 0c2fba5e..6a0fe977 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 @@ -31,6 +31,11 @@ public VCChecker() { public void processSubtyping(Predicate expectedType, List list, CtElement element, Factory f) throws LJError { + processSubtyping(expectedType, list, element, f, null); + } + + public void processSubtyping(Predicate expectedType, List list, CtElement element, Factory f, + String customMessage) throws LJError { List lrv = new ArrayList<>(), mainVars = new ArrayList<>(); gatherVariables(expectedType, lrv, mainVars); if (expectedType.isBooleanTrue()) @@ -53,7 +58,7 @@ public void processSubtyping(Predicate expectedType, List list, CtEl boolean isSubtype = smtChecks(expected, premises, element.getPosition()); if (!isSubtype) throw new RefinementError(element.getPosition(), expectedType.simplify(), premisesBeforeChange.simplify(), - map); + map, customMessage); } /** @@ -71,7 +76,7 @@ public void processSubtyping(Predicate type, Predicate expectedType, List lrv = new ArrayList<>(), mainVars = new ArrayList<>(); gatherVariables(expected, lrv, mainVars); gatherVariables(found, lrv, mainVars); TranslationTable map = new TranslationTable(); Predicate premises = joinPredicates(expected, mainVars, lrv, map).toConjunctions(); - throw new RefinementError(position, expected.simplify(), premises.simplify(), map); + throw new RefinementError(position, expected.simplify(), premises.simplify(), map, customMessage); } - protected void throwStateRefinementError(SourcePosition position, Predicate found, Predicate expected) - throws StateRefinementError { + protected void throwStateRefinementError(SourcePosition position, Predicate found, Predicate expected, + String customMessage) throws StateRefinementError { List lrv = new ArrayList<>(), mainVars = new ArrayList<>(); gatherVariables(found, lrv, mainVars); TranslationTable map = new TranslationTable(); VCImplication foundState = joinPredicates(found, mainVars, lrv, map); throw new StateRefinementError(position, expected.getExpression(), - foundState.toConjunctions().simplify().getValue(), map); + foundState.toConjunctions().simplify().getValue(), map, customMessage); } protected void throwStateConflictError(SourcePosition position, Predicate expected) throws StateConflictError { diff --git a/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/general_checkers/MethodsFunctionsChecker.java b/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/general_checkers/MethodsFunctionsChecker.java index 815e8e6c..ebf908a3 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/general_checkers/MethodsFunctionsChecker.java +++ b/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/general_checkers/MethodsFunctionsChecker.java @@ -154,6 +154,7 @@ private Predicate handleFunctionRefinements(RefinedFunction f, CtElement method, c = oc.get().substituteVariable(Keys.WILDCARD, paramName); param.putMetadata(Keys.REFINEMENT, c); RefinedVariable v = rtc.getContext().addVarToContext(param.getSimpleName(), param.getType(), c, param); + rtc.getMessageFromAnnotation(param).ifPresent(v::setMessage); if (v instanceof Variable) f.addArgRefinements((Variable) v); joint = Predicate.createConjunction(joint, c); @@ -162,6 +163,7 @@ private Predicate handleFunctionRefinements(RefinedFunction f, CtElement method, Predicate ret = oret.orElse(new Predicate()); ret = ret.substituteVariable("return", Keys.WILDCARD); f.setRefReturn(ret); + rtc.getMessageFromAnnotation(method).ifPresent(f::setMessage); return Predicate.createConjunction(joint, ret); } @@ -196,7 +198,7 @@ public void getReturnRefinements(CtReturn ret) throws LJError { .substituteVariable(Keys.THIS, returnVarName); rtc.getContext().addVarToContext(returnVarName, method.getType(), cretRef, ret); - rtc.checkSMT(cexpectedType, ret); + rtc.checkSMT(cexpectedType, ret, fi.getMessage()); rtc.getContext().newRefinementToVariableInContext(returnVarName, cexpectedType); } } @@ -367,7 +369,7 @@ private void checkParameters(CtElement invocation, List> argumen VariableInstance vi = (VariableInstance) invocation.getMetadata(Keys.TARGET); c = c.substituteVariable(Keys.THIS, vi.getName()); } - rtc.checkSMT(c, invocation); + rtc.checkSMT(c, invocation, fArg.getMessage()); } } diff --git a/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/object_checkers/AuxHierarchyRefinementsPassage.java b/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/object_checkers/AuxHierarchyRefinementsPassage.java index 88dcf683..455e8276 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/object_checkers/AuxHierarchyRefinementsPassage.java +++ b/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/object_checkers/AuxHierarchyRefinementsPassage.java @@ -83,7 +83,7 @@ static void transferArgumentsRefinements(RefinedFunction superFunction, RefinedF } else { boolean ok = tc.checksStateSMT(superArgRef, argRef, params.get(i).getPosition()); if (!ok) { - tc.throwRefinementError(method.getPosition(), argRef, superArgRef); + tc.throwRefinementError(method.getPosition(), argRef, superArgRef, function.getMessage()); } } } 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 bd76950b..69102543 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 @@ -61,7 +61,11 @@ private static void setConstructorStates(RefinedFunction f, List an : anns) { Map m = an.getAllValues(); String to = TypeCheckingUtils.getStringFromAnnotation(m.get("to")); + String msg = TypeCheckingUtils.getStringFromAnnotation(m.get("msg")); ObjectState state = new ObjectState(); + if (msg != null && !msg.isEmpty()) + state.setMessage(msg); + if (to != null) { Predicate p = new Predicate(to, element); if (!p.getExpression().isBooleanExpression()) { @@ -163,7 +167,10 @@ private static ObjectState getStates(CtAnnotation ctAnnota Map m = ctAnnotation.getAllValues(); String from = TypeCheckingUtils.getStringFromAnnotation(m.get("from")); String to = TypeCheckingUtils.getStringFromAnnotation(m.get("to")); + String msg = TypeCheckingUtils.getStringFromAnnotation(m.get("msg")); ObjectState state = new ObjectState(); + if (msg != null && !msg.isEmpty()) + state.setMessage(msg); // has from if (from != null) @@ -407,7 +414,7 @@ public static void updateGhostField(CtFieldWrite fw, TypeChecker tc) throws L .changeOldMentions(vi.getName(), instanceName); if (!tc.checksStateSMT(prevState, expectState, fw.getPosition())) { // Invalid field transition - tc.throwStateRefinementError(fw.getPosition(), prevState, stateChange.getFrom()); + tc.throwStateRefinementError(fw.getPosition(), prevState, stateChange.getFrom(), stateChange.getMessage()); return; } @@ -480,7 +487,7 @@ private static void changeState(TypeChecker tc, VariableInstance vi, List msg != null && !msg.isBlank()).distinct().collect(Collectors.joining(" || ")); + tc.throwStateRefinementError(invocation.getPosition(), prevState, expectedStatesDisjunction, message); } } From 15c99dadf593ae4394e4cefe4791f29180b55fbe Mon Sep 17 00:00:00 2001 From: Ricardo Costa Date: Thu, 5 Feb 2026 16:19:31 +0000 Subject: [PATCH 2/3] Separate Multiple Messages by Line --- .../src/main/java/liquidjava/diagnostics/LJDiagnostic.java | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/liquidjava-verifier/src/main/java/liquidjava/diagnostics/LJDiagnostic.java b/liquidjava-verifier/src/main/java/liquidjava/diagnostics/LJDiagnostic.java index 0b22de75..71cd755a 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/diagnostics/LJDiagnostic.java +++ b/liquidjava-verifier/src/main/java/liquidjava/diagnostics/LJDiagnostic.java @@ -126,9 +126,9 @@ public String getSnippet() { // custom message if (customMessage != null && !customMessage.isBlank()) { - sb.append(" " + customMessage); + String sep = " || "; + sb.append(" " + customMessage.replace(sep, "\n" + " ".repeat(padding + colEnd + sep.length()))); } - sb.append(Colors.RESET).append("\n"); } } From 520ef850cf383c6697c721cfde3fbb5946c330c4 Mon Sep 17 00:00:00 2001 From: Ricardo Costa Date: Thu, 5 Feb 2026 19:58:38 +0000 Subject: [PATCH 3/3] Minor Changes --- .../java/liquidjava/diagnostics/LJDiagnostic.java | 11 ++++++----- .../object_checkers/AuxStateHandler.java | 2 +- 2 files changed, 7 insertions(+), 6 deletions(-) diff --git a/liquidjava-verifier/src/main/java/liquidjava/diagnostics/LJDiagnostic.java b/liquidjava-verifier/src/main/java/liquidjava/diagnostics/LJDiagnostic.java index 71cd755a..a8147aff 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/diagnostics/LJDiagnostic.java +++ b/liquidjava-verifier/src/main/java/liquidjava/diagnostics/LJDiagnostic.java @@ -104,13 +104,14 @@ public String getSnippet() { // calculate padding for line numbers int padding = String.valueOf(endLine).length(); + String pipe = " | "; for (int i = startLine; i <= endLine; i++) { String lineNumStr = String.format("%" + padding + "d", i); String line = lines.get(i - 1); // add line - sb.append(Colors.GREY).append(lineNumStr).append(" | ").append(line).append(Colors.RESET).append("\n"); + 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 >= position.lineStart() && i <= position.lineEnd()) { @@ -118,16 +119,16 @@ public String getSnippet() { int colEnd = (i == position.lineEnd()) ? position.colEnd() : line.length(); if (colStart > 0 && colEnd > 0) { - // line number padding + " | " + column offset - String indent = " ".repeat(padding) + Colors.GREY + " | " + Colors.RESET + // line number padding + pipe + column offset + String indent = " ".repeat(padding) + Colors.GREY + pipe + Colors.RESET + " ".repeat(colStart - 1); String markers = accentColor + "^".repeat(Math.max(1, colEnd - colStart + 1)); sb.append(indent).append(markers); // custom message if (customMessage != null && !customMessage.isBlank()) { - String sep = " || "; - sb.append(" " + customMessage.replace(sep, "\n" + " ".repeat(padding + colEnd + sep.length()))); + String offset = " ".repeat(padding + colEnd + pipe.length() + 1); + sb.append(" " + customMessage.replace("\n", "\n" + offset)); } sb.append(Colors.RESET).append("\n"); } 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 69102543..facbd2c1 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 @@ -499,7 +499,7 @@ private static void changeState(TypeChecker tc, VariableInstance vi, List msg != null && !msg.isBlank()).distinct().collect(Collectors.joining(" || ")); + .filter(msg -> msg != null && !msg.isBlank()).distinct().collect(Collectors.joining("\n")); tc.throwStateRefinementError(invocation.getPosition(), prevState, expectedStatesDisjunction, message); } }