From 370c4054693251dbdf8b85dc86b2ea9278fc5454 Mon Sep 17 00:00:00 2001 From: Ricardo Costa Date: Wed, 5 Nov 2025 10:30:08 +0000 Subject: [PATCH 1/4] Add Diagnostic Classes --- .../java/liquidjava/errors/ErrorPosition.java | 19 ++-- .../java/liquidjava/errors/LJDiagnostics.java | 93 +++++++++++++++++++ .../liquidjava/errors/errors/CustomError.java | 13 +++ .../errors/errors/GhostInvocationError.java | 26 ++++++ .../IllegalConstructorTransitionError.java | 17 ++++ .../errors/errors/InvalidRefinementError.java | 25 +++++ .../liquidjava/errors/errors/LJError.java | 65 +++++++++++++ .../errors/errors/NotFoundError.java | 16 ++++ .../errors/errors/RefinementError.java | 27 ++++++ .../errors/errors/StateConflictError.java | 33 +++++++ .../errors/errors/StateRefinementError.java | 43 +++++++++ .../liquidjava/errors/errors/SyntaxError.java | 29 ++++++ .../ExternalClassNotFoundWarning.java | 25 +++++ .../ExternalMethodNotFoundWarning.java | 32 +++++++ .../liquidjava/errors/warnings/LJWarning.java | 60 ++++++++++++ .../src/main/java/liquidjava/utils/Utils.java | 4 + 16 files changed, 521 insertions(+), 6 deletions(-) create mode 100644 liquidjava-verifier/src/main/java/liquidjava/errors/LJDiagnostics.java create mode 100644 liquidjava-verifier/src/main/java/liquidjava/errors/errors/CustomError.java create mode 100644 liquidjava-verifier/src/main/java/liquidjava/errors/errors/GhostInvocationError.java create mode 100644 liquidjava-verifier/src/main/java/liquidjava/errors/errors/IllegalConstructorTransitionError.java create mode 100644 liquidjava-verifier/src/main/java/liquidjava/errors/errors/InvalidRefinementError.java create mode 100644 liquidjava-verifier/src/main/java/liquidjava/errors/errors/LJError.java create mode 100644 liquidjava-verifier/src/main/java/liquidjava/errors/errors/NotFoundError.java create mode 100644 liquidjava-verifier/src/main/java/liquidjava/errors/errors/RefinementError.java create mode 100644 liquidjava-verifier/src/main/java/liquidjava/errors/errors/StateConflictError.java create mode 100644 liquidjava-verifier/src/main/java/liquidjava/errors/errors/StateRefinementError.java create mode 100644 liquidjava-verifier/src/main/java/liquidjava/errors/errors/SyntaxError.java create mode 100644 liquidjava-verifier/src/main/java/liquidjava/errors/warnings/ExternalClassNotFoundWarning.java create mode 100644 liquidjava-verifier/src/main/java/liquidjava/errors/warnings/ExternalMethodNotFoundWarning.java create mode 100644 liquidjava-verifier/src/main/java/liquidjava/errors/warnings/LJWarning.java diff --git a/liquidjava-verifier/src/main/java/liquidjava/errors/ErrorPosition.java b/liquidjava-verifier/src/main/java/liquidjava/errors/ErrorPosition.java index a7afd433..5b09c42a 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/errors/ErrorPosition.java +++ b/liquidjava-verifier/src/main/java/liquidjava/errors/ErrorPosition.java @@ -1,18 +1,19 @@ package liquidjava.errors; +import spoon.reflect.cu.SourcePosition; + public class ErrorPosition { private int lineStart; private int colStart; - private int lineEnd; private int colEnd; - public ErrorPosition(int line1, int col1, int line2, int col2) { - lineStart = line1; - colStart = col1; - lineEnd = line2; - colEnd = col2; + public ErrorPosition(int lineStart, int colStart, int lineEnd, int colEnd) { + this.lineStart = lineStart; + this.colStart = colStart; + this.lineEnd = lineEnd; + this.colEnd = colEnd; } public int getLineStart() { @@ -30,4 +31,10 @@ public int getLineEnd() { public int getColEnd() { return colEnd; } + + public static ErrorPosition fromSpoonPosition(SourcePosition pos) { + if (pos == null || !pos.isValidPosition()) + return null; + return new ErrorPosition(pos.getLine(), pos.getColumn(), pos.getEndLine(), pos.getEndColumn()); + } } diff --git a/liquidjava-verifier/src/main/java/liquidjava/errors/LJDiagnostics.java b/liquidjava-verifier/src/main/java/liquidjava/errors/LJDiagnostics.java new file mode 100644 index 00000000..2a63ed44 --- /dev/null +++ b/liquidjava-verifier/src/main/java/liquidjava/errors/LJDiagnostics.java @@ -0,0 +1,93 @@ +package liquidjava.errors; + +import java.util.ArrayList; +import java.util.HashMap; + +import liquidjava.errors.errors.LJError; +import liquidjava.errors.warnings.LJWarning; +import liquidjava.processor.context.PlacementInCode; + +public class LJDiagnostics { + private static LJDiagnostics instance; + + private ArrayList errors; + private ArrayList warnings; + private HashMap translationMap; + + private LJDiagnostics() { + this.errors = new ArrayList<>(); + this.warnings = new ArrayList<>(); + this.translationMap = new HashMap<>(); + } + + public static LJDiagnostics getInstance() { + if (instance == null) + instance = new LJDiagnostics(); + return instance; + } + + public void addError(LJError error) { + this.errors.add(error); + } + + public void addWarning(LJWarning warning) { + this.warnings.add(warning); + } + + public void setTranslationMap(HashMap map) { + this.translationMap = map; + } + + public boolean foundError() { + return !this.errors.isEmpty(); + } + + public boolean foundWarning() { + return !this.warnings.isEmpty(); + } + + public ArrayList getErrors() { + return this.errors; + } + + public ArrayList getWarnings() { + return this.warnings; + } + + public HashMap getTranslationMap() { + return this.translationMap; + } + + public LJError getError() { + return foundError() ? this.errors.get(0) : null; + } + + public LJWarning getWarning() { + return foundWarning() ? this.warnings.get(0) : null; + } + + public void clear() { + this.errors.clear(); + this.warnings.clear(); + this.translationMap.clear(); + } + + @Override + public String toString() { + StringBuilder sb = new StringBuilder(); + if (foundError()) { + for (LJError error : errors) { + sb.append(error.toString()).append("\n"); + } + } else { + if (foundWarning()) { + sb.append("Warnings:\n"); + for (LJWarning warning : warnings) { + sb.append(warning.getMessage()).append("\n"); + } + sb.append("Passed Verification!\n"); + } + } + return sb.toString(); + } +} diff --git a/liquidjava-verifier/src/main/java/liquidjava/errors/errors/CustomError.java b/liquidjava-verifier/src/main/java/liquidjava/errors/errors/CustomError.java new file mode 100644 index 00000000..2c8fee11 --- /dev/null +++ b/liquidjava-verifier/src/main/java/liquidjava/errors/errors/CustomError.java @@ -0,0 +1,13 @@ +package liquidjava.errors.errors; + +public class CustomError extends LJError { + + public CustomError(String message) { + super("Found Error", message, null); + } + + @Override + public String toString() { + return super.toString(null); + } +} diff --git a/liquidjava-verifier/src/main/java/liquidjava/errors/errors/GhostInvocationError.java b/liquidjava-verifier/src/main/java/liquidjava/errors/errors/GhostInvocationError.java new file mode 100644 index 00000000..ecb2b009 --- /dev/null +++ b/liquidjava-verifier/src/main/java/liquidjava/errors/errors/GhostInvocationError.java @@ -0,0 +1,26 @@ +package liquidjava.errors.errors; + +import liquidjava.rj_language.Predicate; +import spoon.reflect.declaration.CtElement; + +// when a ghost call has wrong types or number of arguments +public class GhostInvocationError extends LJError { + + private Predicate expected; + + public GhostInvocationError(CtElement element, Predicate expected) { + super("Ghost Invocation Error", "Invalid types or number of arguments in ghost invocation", element); + this.expected = expected; + } + + public Predicate getExpected() { + return expected; + } + + @Override + public String toString() { + StringBuilder sb = new StringBuilder(); + sb.append("Expected: ").append(expected.toString()).append("\n"); + return super.toString(sb.toString()); + } +} diff --git a/liquidjava-verifier/src/main/java/liquidjava/errors/errors/IllegalConstructorTransitionError.java b/liquidjava-verifier/src/main/java/liquidjava/errors/errors/IllegalConstructorTransitionError.java new file mode 100644 index 00000000..585d46c1 --- /dev/null +++ b/liquidjava-verifier/src/main/java/liquidjava/errors/errors/IllegalConstructorTransitionError.java @@ -0,0 +1,17 @@ +package liquidjava.errors.errors; + +import spoon.reflect.declaration.CtElement; + +// when a constructor contains a @StateRefinement with a from state +public class IllegalConstructorTransitionError extends LJError { + + public IllegalConstructorTransitionError(CtElement element) { + super("Illegal Constructor Transition Error", + "Found constructor with 'from' state (should only have a 'to' state)", element); + } + + @Override + public String toString() { + return super.toString(null); + } +} diff --git a/liquidjava-verifier/src/main/java/liquidjava/errors/errors/InvalidRefinementError.java b/liquidjava-verifier/src/main/java/liquidjava/errors/errors/InvalidRefinementError.java new file mode 100644 index 00000000..8c974383 --- /dev/null +++ b/liquidjava-verifier/src/main/java/liquidjava/errors/errors/InvalidRefinementError.java @@ -0,0 +1,25 @@ +package liquidjava.errors.errors; + +import spoon.reflect.declaration.CtElement; + +// when a refinement is invalid, e.g. is not a boolean expression +public class InvalidRefinementError extends LJError { + + private String refinement; + + public InvalidRefinementError(String message, CtElement element, String refinement) { + super("Invalid Refinement", message, element); + this.refinement = refinement; + } + + public String getRefinement() { + return refinement; + } + + @Override + public String toString() { + StringBuilder sb = new StringBuilder(); + sb.append("Refinement: ").append(refinement).append("\n"); + return super.toString(sb.toString()); + } +} diff --git a/liquidjava-verifier/src/main/java/liquidjava/errors/errors/LJError.java b/liquidjava-verifier/src/main/java/liquidjava/errors/errors/LJError.java new file mode 100644 index 00000000..a01db30b --- /dev/null +++ b/liquidjava-verifier/src/main/java/liquidjava/errors/errors/LJError.java @@ -0,0 +1,65 @@ +package liquidjava.errors.errors; + +import liquidjava.errors.ErrorPosition; +import liquidjava.utils.Utils; +import spoon.reflect.cu.SourcePosition; +import spoon.reflect.declaration.CtElement; + +// base class for all LiquidJava errors +public abstract class LJError extends Exception { + + private String title; + private String message; + private CtElement element; + private ErrorPosition position; + private SourcePosition location; + + public LJError(String title, String message, CtElement element) { + super(message); + this.title = title; + this.message = message; + this.element = element; + try { + this.location = element.getPosition(); + this.position = ErrorPosition.fromSpoonPosition(element.getPosition()); + } catch (Exception e) { + this.location = null; + this.position = null; + } + } + + public String getTitle() { + return title; + } + + public String getMessage() { + return message; + } + + public CtElement getElement() { + return element; + } + + public ErrorPosition getPosition() { + return position; + } + + public SourcePosition getLocation() { + return location; + } + + @Override + public abstract String toString(); + + public String toString(String extra) { + StringBuilder sb = new StringBuilder(); + sb.append(title).append(" at: \n").append(element.toString().replace("@liquidjava.specification.", "@")) + .append("\n\n"); + sb.append(message).append("\n"); + if (extra != null) + sb.append(extra).append("\n"); + sb.append("Location: ").append(location != null ? Utils.stripParens(location.toString()) : "") + .append("\n"); + return sb.toString(); + } +} diff --git a/liquidjava-verifier/src/main/java/liquidjava/errors/errors/NotFoundError.java b/liquidjava-verifier/src/main/java/liquidjava/errors/errors/NotFoundError.java new file mode 100644 index 00000000..4a10e7ca --- /dev/null +++ b/liquidjava-verifier/src/main/java/liquidjava/errors/errors/NotFoundError.java @@ -0,0 +1,16 @@ +package liquidjava.errors.errors; + +import spoon.reflect.declaration.CtElement; + +// e.g. when a variable used in a refinement is not found +public class NotFoundError extends LJError { + + public NotFoundError(String message, CtElement element) { + super("Not Found Error", message, element); + } + + @Override + public String toString() { + return super.toString(null); + } +} diff --git a/liquidjava-verifier/src/main/java/liquidjava/errors/errors/RefinementError.java b/liquidjava-verifier/src/main/java/liquidjava/errors/errors/RefinementError.java new file mode 100644 index 00000000..7fe05a59 --- /dev/null +++ b/liquidjava-verifier/src/main/java/liquidjava/errors/errors/RefinementError.java @@ -0,0 +1,27 @@ +package liquidjava.errors.errors; + +import liquidjava.rj_language.Predicate; +import liquidjava.rj_language.opt.derivation_node.ValDerivationNode; +import liquidjava.utils.Utils; +import spoon.reflect.declaration.CtElement; + +// when a @Refinement is violated +public class RefinementError extends LJError { + + private Predicate expected; + private ValDerivationNode found; + + public RefinementError(CtElement element, Predicate expected, ValDerivationNode found) { + super("Refinement Error", "Predicate refinement violation", element); + this.expected = expected; + this.found = found; + } + + @Override + public String toString() { + StringBuilder sb = new StringBuilder(); + sb.append("Expected: ").append(Utils.stripParens(expected.toString())).append("\n"); + sb.append("Found: ").append(found.getValue()); + return super.toString(sb.toString()); + } +} \ No newline at end of file diff --git a/liquidjava-verifier/src/main/java/liquidjava/errors/errors/StateConflictError.java b/liquidjava-verifier/src/main/java/liquidjava/errors/errors/StateConflictError.java new file mode 100644 index 00000000..fe829362 --- /dev/null +++ b/liquidjava-verifier/src/main/java/liquidjava/errors/errors/StateConflictError.java @@ -0,0 +1,33 @@ +package liquidjava.errors.errors; + +import liquidjava.rj_language.Predicate; +import spoon.reflect.declaration.CtElement; + +// when two incompatible states are found in a state set +public class StateConflictError extends LJError { + + private Predicate predicate; + private String className; + + public StateConflictError(CtElement element, Predicate predicate, String className) { + super("State Conflict Error", "Found multiple disjoint states from a StateSet in refinement", element); + this.predicate = predicate; + this.className = className; + } + + public Predicate getPredicate() { + return predicate; + } + + public String getClassName() { + return className; + } + + @Override + public String toString() { + StringBuilder sb = new StringBuilder(); + sb.append("Class: ").append(className).append("\n"); + sb.append("Predicate: ").append(predicate.toString()); + return super.toString(sb.toString()); + } +} diff --git a/liquidjava-verifier/src/main/java/liquidjava/errors/errors/StateRefinementError.java b/liquidjava-verifier/src/main/java/liquidjava/errors/errors/StateRefinementError.java new file mode 100644 index 00000000..a787e197 --- /dev/null +++ b/liquidjava-verifier/src/main/java/liquidjava/errors/errors/StateRefinementError.java @@ -0,0 +1,43 @@ +package liquidjava.errors.errors; + +import java.util.Arrays; + +import spoon.reflect.declaration.CtElement; + +// when a @StateRefinement is violated +public class StateRefinementError extends LJError { + + private final String method; + private final String[] expected; + private final String found; + + public StateRefinementError(CtElement element, String method, String[] expected, String found) { + super("State Refinement Error", "State refinement transition violation", element); + this.method = method; + this.expected = expected; + this.found = found; + } + + public String getMethod() { + return method; + } + + public String[] getExpected() { + return expected; + } + + public String getFound() { + return found; + } + + @Override + public String toString() { + StringBuilder sb = new StringBuilder(); + sb.append("Method: ").append(method).append("\n"); + sb.append("Expected: "); + Arrays.stream(expected).forEach(s -> sb.append(s).append(", ")); + sb.append("\n"); + sb.append("Found: ").append(found); + return super.toString(sb.toString()); + } +} diff --git a/liquidjava-verifier/src/main/java/liquidjava/errors/errors/SyntaxError.java b/liquidjava-verifier/src/main/java/liquidjava/errors/errors/SyntaxError.java new file mode 100644 index 00000000..639c67bd --- /dev/null +++ b/liquidjava-verifier/src/main/java/liquidjava/errors/errors/SyntaxError.java @@ -0,0 +1,29 @@ +package liquidjava.errors.errors; + +import spoon.reflect.declaration.CtElement; + +// when the syntax of a refinement is invalid +public class SyntaxError extends LJError { + + private String refinement; + + public SyntaxError(String message, String refinement) { + this(message, null, refinement); + } + + public SyntaxError(String message, CtElement element, String refinement) { + super("Syntax Error", message, element); + this.refinement = refinement; + } + + public String getRefinement() { + return refinement; + } + + @Override + public String toString() { + StringBuilder sb = new StringBuilder(); + sb.append("Invalid syntax in refinement: ").append(refinement); + return super.toString(sb.toString()); + } +} diff --git a/liquidjava-verifier/src/main/java/liquidjava/errors/warnings/ExternalClassNotFoundWarning.java b/liquidjava-verifier/src/main/java/liquidjava/errors/warnings/ExternalClassNotFoundWarning.java new file mode 100644 index 00000000..59a999f8 --- /dev/null +++ b/liquidjava-verifier/src/main/java/liquidjava/errors/warnings/ExternalClassNotFoundWarning.java @@ -0,0 +1,25 @@ +package liquidjava.errors.warnings; + +import spoon.reflect.declaration.CtElement; + +// when a class referenced in an external refinement cannot be found +public class ExternalClassNotFoundWarning extends LJWarning { + + private String className; + + public ExternalClassNotFoundWarning(CtElement element, String className) { + super("Class in external refinement not found", element); + this.className = className; + } + + public String getClassName() { + return className; + } + + @Override + public String toString() { + StringBuilder sb = new StringBuilder(); + sb.append("Class: ").append(className); + return super.toString(sb.toString()); + } +} diff --git a/liquidjava-verifier/src/main/java/liquidjava/errors/warnings/ExternalMethodNotFoundWarning.java b/liquidjava-verifier/src/main/java/liquidjava/errors/warnings/ExternalMethodNotFoundWarning.java new file mode 100644 index 00000000..086a0210 --- /dev/null +++ b/liquidjava-verifier/src/main/java/liquidjava/errors/warnings/ExternalMethodNotFoundWarning.java @@ -0,0 +1,32 @@ +package liquidjava.errors.warnings; + +import spoon.reflect.declaration.CtElement; + +// when a method referenced in an external refinement cannot be found +public class ExternalMethodNotFoundWarning extends LJWarning { + + private String methodName; + private String className; + + public ExternalMethodNotFoundWarning(CtElement element, String methodName, String className) { + super("Method in external refinement not found", element); + this.methodName = methodName; + this.className = className; + } + + public String getMethodName() { + return methodName; + } + + public String getClassName() { + return className; + } + + @Override + public String toString() { + StringBuilder sb = new StringBuilder(); + sb.append("Class: ").append(className).append("\n"); + sb.append("Method: ").append(methodName); + return super.toString(sb.toString()); + } +} diff --git a/liquidjava-verifier/src/main/java/liquidjava/errors/warnings/LJWarning.java b/liquidjava-verifier/src/main/java/liquidjava/errors/warnings/LJWarning.java new file mode 100644 index 00000000..ac4d161e --- /dev/null +++ b/liquidjava-verifier/src/main/java/liquidjava/errors/warnings/LJWarning.java @@ -0,0 +1,60 @@ +package liquidjava.errors.warnings; + +import java.net.URI; + +import liquidjava.errors.ErrorPosition; +import liquidjava.utils.Utils; +import spoon.reflect.cu.SourcePosition; +import spoon.reflect.declaration.CtElement; + +// base class for all LiquidJava warnings +public abstract class LJWarning { + + private String message; + private CtElement element; + private ErrorPosition position; + private SourcePosition location; + + public LJWarning(String message, CtElement element) { + this.message = message; + this.element = element; + try { + this.location = element.getPosition(); + this.position = ErrorPosition.fromSpoonPosition(element.getPosition()); + } catch (Exception e) { + // This warning is from a generated part of the source code, so no precise position is provided + this.location = null; + this.position = null; + } + } + + public String getMessage() { + return message; + } + + public CtElement getElement() { + return element; + } + + public ErrorPosition getPosition() { + return position; + } + + public SourcePosition getLocation() { + return location; + } + + @Override + public abstract String toString(); + + public String toString(String extra) { + StringBuilder sb = new StringBuilder(); + sb.append(message).append(" at: \n").append(element.toString().replace("@liquidjava.specification.", "@")) + .append("\n\n"); + if (extra != null) + sb.append(extra).append("\n"); + sb.append("Location: ").append(location != null ? Utils.stripParens(location.toString()) : "") + .append("\n"); + return sb.toString(); + } +} diff --git a/liquidjava-verifier/src/main/java/liquidjava/utils/Utils.java b/liquidjava-verifier/src/main/java/liquidjava/utils/Utils.java index 008879cb..6c204258 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/utils/Utils.java +++ b/liquidjava-verifier/src/main/java/liquidjava/utils/Utils.java @@ -69,4 +69,8 @@ public static String qualifyName(String prefix, String name) { return name; // dont qualify return String.format("%s.%s", prefix, name); } + + public static String stripParens(String s) { + return s.startsWith("(") && s.endsWith(")") ? s.substring(1, s.length() - 1) : s; + } } From 967849e7fc6ae267c62e02272ba5b23d20c3c979 Mon Sep 17 00:00:00 2001 From: Ricardo Costa Date: Wed, 5 Nov 2025 10:32:32 +0000 Subject: [PATCH 2/4] Rename `errors` Folder to `diagnostics` --- .../src/main/java/liquidjava/api/CommandLineLauncher.java | 3 ++- .../liquidjava/{errors => diagnostics}/ErrorEmitter.java | 2 +- .../liquidjava/{errors => diagnostics}/ErrorHandler.java | 2 +- .../liquidjava/{errors => diagnostics}/ErrorPosition.java | 2 +- .../liquidjava/{errors => diagnostics}/LJDiagnostics.java | 6 +++--- .../{errors => diagnostics}/errors/CustomError.java | 2 +- .../errors/GhostInvocationError.java | 2 +- .../errors/IllegalConstructorTransitionError.java | 2 +- .../errors/InvalidRefinementError.java | 2 +- .../liquidjava/{errors => diagnostics}/errors/LJError.java | 4 ++-- .../{errors => diagnostics}/errors/NotFoundError.java | 2 +- .../{errors => diagnostics}/errors/RefinementError.java | 2 +- .../{errors => diagnostics}/errors/StateConflictError.java | 2 +- .../errors/StateRefinementError.java | 2 +- .../{errors => diagnostics}/errors/SyntaxError.java | 2 +- .../warnings/ExternalClassNotFoundWarning.java | 2 +- .../warnings/ExternalMethodNotFoundWarning.java | 2 +- .../{errors => diagnostics}/warnings/LJWarning.java | 4 ++-- .../main/java/liquidjava/processor/RefinementProcessor.java | 3 ++- .../processor/ann_generation/FieldGhostsGeneration.java | 2 +- .../java/liquidjava/processor/context/AliasWrapper.java | 3 ++- .../refinement_checker/ExternalRefinementTypeChecker.java | 5 +++-- .../processor/refinement_checker/MethodsFirstChecker.java | 3 ++- .../processor/refinement_checker/RefinementTypeChecker.java | 3 ++- .../processor/refinement_checker/TypeChecker.java | 5 +++-- .../liquidjava/processor/refinement_checker/VCChecker.java | 5 +++-- .../refinement_checker/object_checkers/AuxStateHandler.java | 3 ++- .../liquidjava/rj_language/BuiltinFunctionPredicate.java | 2 +- .../src/main/java/liquidjava/rj_language/Predicate.java | 5 +++-- .../src/test/java/liquidjava/api/tests/TestExamples.java | 2 +- 30 files changed, 48 insertions(+), 38 deletions(-) rename liquidjava-verifier/src/main/java/liquidjava/{errors => diagnostics}/ErrorEmitter.java (98%) rename liquidjava-verifier/src/main/java/liquidjava/{errors => diagnostics}/ErrorHandler.java (99%) rename liquidjava-verifier/src/main/java/liquidjava/{errors => diagnostics}/ErrorPosition.java (96%) rename liquidjava-verifier/src/main/java/liquidjava/{errors => diagnostics}/LJDiagnostics.java (94%) rename liquidjava-verifier/src/main/java/liquidjava/{errors => diagnostics}/errors/CustomError.java (85%) rename liquidjava-verifier/src/main/java/liquidjava/{errors => diagnostics}/errors/GhostInvocationError.java (95%) rename liquidjava-verifier/src/main/java/liquidjava/{errors => diagnostics}/errors/IllegalConstructorTransitionError.java (92%) rename liquidjava-verifier/src/main/java/liquidjava/{errors => diagnostics}/errors/InvalidRefinementError.java (94%) rename liquidjava-verifier/src/main/java/liquidjava/{errors => diagnostics}/errors/LJError.java (95%) rename liquidjava-verifier/src/main/java/liquidjava/{errors => diagnostics}/errors/NotFoundError.java (90%) rename liquidjava-verifier/src/main/java/liquidjava/{errors => diagnostics}/errors/RefinementError.java (95%) rename liquidjava-verifier/src/main/java/liquidjava/{errors => diagnostics}/errors/StateConflictError.java (96%) rename liquidjava-verifier/src/main/java/liquidjava/{errors => diagnostics}/errors/StateRefinementError.java (96%) rename liquidjava-verifier/src/main/java/liquidjava/{errors => diagnostics}/errors/SyntaxError.java (94%) rename liquidjava-verifier/src/main/java/liquidjava/{errors => diagnostics}/warnings/ExternalClassNotFoundWarning.java (94%) rename liquidjava-verifier/src/main/java/liquidjava/{errors => diagnostics}/warnings/ExternalMethodNotFoundWarning.java (95%) rename liquidjava-verifier/src/main/java/liquidjava/{errors => diagnostics}/warnings/LJWarning.java (95%) diff --git a/liquidjava-verifier/src/main/java/liquidjava/api/CommandLineLauncher.java b/liquidjava-verifier/src/main/java/liquidjava/api/CommandLineLauncher.java index b7471a36..dc6aa2b4 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/api/CommandLineLauncher.java +++ b/liquidjava-verifier/src/main/java/liquidjava/api/CommandLineLauncher.java @@ -3,7 +3,8 @@ import java.io.File; import java.util.Arrays; import java.util.List; -import liquidjava.errors.ErrorEmitter; + +import liquidjava.diagnostics.ErrorEmitter; import liquidjava.processor.RefinementProcessor; import spoon.Launcher; import spoon.processing.ProcessingManager; diff --git a/liquidjava-verifier/src/main/java/liquidjava/errors/ErrorEmitter.java b/liquidjava-verifier/src/main/java/liquidjava/diagnostics/ErrorEmitter.java similarity index 98% rename from liquidjava-verifier/src/main/java/liquidjava/errors/ErrorEmitter.java rename to liquidjava-verifier/src/main/java/liquidjava/diagnostics/ErrorEmitter.java index 0036d320..02610343 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/errors/ErrorEmitter.java +++ b/liquidjava-verifier/src/main/java/liquidjava/diagnostics/ErrorEmitter.java @@ -1,4 +1,4 @@ -package liquidjava.errors; +package liquidjava.diagnostics; import java.net.URI; import java.util.HashMap; diff --git a/liquidjava-verifier/src/main/java/liquidjava/errors/ErrorHandler.java b/liquidjava-verifier/src/main/java/liquidjava/diagnostics/ErrorHandler.java similarity index 99% rename from liquidjava-verifier/src/main/java/liquidjava/errors/ErrorHandler.java rename to liquidjava-verifier/src/main/java/liquidjava/diagnostics/ErrorHandler.java index 91ab4987..af45af24 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/errors/ErrorHandler.java +++ b/liquidjava-verifier/src/main/java/liquidjava/diagnostics/ErrorHandler.java @@ -1,4 +1,4 @@ -package liquidjava.errors; +package liquidjava.diagnostics; import java.util.Formatter; import java.util.HashMap; diff --git a/liquidjava-verifier/src/main/java/liquidjava/errors/ErrorPosition.java b/liquidjava-verifier/src/main/java/liquidjava/diagnostics/ErrorPosition.java similarity index 96% rename from liquidjava-verifier/src/main/java/liquidjava/errors/ErrorPosition.java rename to liquidjava-verifier/src/main/java/liquidjava/diagnostics/ErrorPosition.java index 5b09c42a..1ee72e7d 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/errors/ErrorPosition.java +++ b/liquidjava-verifier/src/main/java/liquidjava/diagnostics/ErrorPosition.java @@ -1,4 +1,4 @@ -package liquidjava.errors; +package liquidjava.diagnostics; import spoon.reflect.cu.SourcePosition; diff --git a/liquidjava-verifier/src/main/java/liquidjava/errors/LJDiagnostics.java b/liquidjava-verifier/src/main/java/liquidjava/diagnostics/LJDiagnostics.java similarity index 94% rename from liquidjava-verifier/src/main/java/liquidjava/errors/LJDiagnostics.java rename to liquidjava-verifier/src/main/java/liquidjava/diagnostics/LJDiagnostics.java index 2a63ed44..624ffe65 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/errors/LJDiagnostics.java +++ b/liquidjava-verifier/src/main/java/liquidjava/diagnostics/LJDiagnostics.java @@ -1,10 +1,10 @@ -package liquidjava.errors; +package liquidjava.diagnostics; import java.util.ArrayList; import java.util.HashMap; -import liquidjava.errors.errors.LJError; -import liquidjava.errors.warnings.LJWarning; +import liquidjava.diagnostics.errors.LJError; +import liquidjava.diagnostics.warnings.LJWarning; import liquidjava.processor.context.PlacementInCode; public class LJDiagnostics { diff --git a/liquidjava-verifier/src/main/java/liquidjava/errors/errors/CustomError.java b/liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/CustomError.java similarity index 85% rename from liquidjava-verifier/src/main/java/liquidjava/errors/errors/CustomError.java rename to liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/CustomError.java index 2c8fee11..7fd67b13 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/errors/errors/CustomError.java +++ b/liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/CustomError.java @@ -1,4 +1,4 @@ -package liquidjava.errors.errors; +package liquidjava.diagnostics.errors; public class CustomError extends LJError { diff --git a/liquidjava-verifier/src/main/java/liquidjava/errors/errors/GhostInvocationError.java b/liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/GhostInvocationError.java similarity index 95% rename from liquidjava-verifier/src/main/java/liquidjava/errors/errors/GhostInvocationError.java rename to liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/GhostInvocationError.java index ecb2b009..1dd6db16 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/errors/errors/GhostInvocationError.java +++ b/liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/GhostInvocationError.java @@ -1,4 +1,4 @@ -package liquidjava.errors.errors; +package liquidjava.diagnostics.errors; import liquidjava.rj_language.Predicate; import spoon.reflect.declaration.CtElement; diff --git a/liquidjava-verifier/src/main/java/liquidjava/errors/errors/IllegalConstructorTransitionError.java b/liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/IllegalConstructorTransitionError.java similarity index 92% rename from liquidjava-verifier/src/main/java/liquidjava/errors/errors/IllegalConstructorTransitionError.java rename to liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/IllegalConstructorTransitionError.java index 585d46c1..14045f31 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/errors/errors/IllegalConstructorTransitionError.java +++ b/liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/IllegalConstructorTransitionError.java @@ -1,4 +1,4 @@ -package liquidjava.errors.errors; +package liquidjava.diagnostics.errors; import spoon.reflect.declaration.CtElement; diff --git a/liquidjava-verifier/src/main/java/liquidjava/errors/errors/InvalidRefinementError.java b/liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/InvalidRefinementError.java similarity index 94% rename from liquidjava-verifier/src/main/java/liquidjava/errors/errors/InvalidRefinementError.java rename to liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/InvalidRefinementError.java index 8c974383..c3686a0e 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/errors/errors/InvalidRefinementError.java +++ b/liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/InvalidRefinementError.java @@ -1,4 +1,4 @@ -package liquidjava.errors.errors; +package liquidjava.diagnostics.errors; import spoon.reflect.declaration.CtElement; diff --git a/liquidjava-verifier/src/main/java/liquidjava/errors/errors/LJError.java b/liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/LJError.java similarity index 95% rename from liquidjava-verifier/src/main/java/liquidjava/errors/errors/LJError.java rename to liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/LJError.java index a01db30b..f6c3501b 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/errors/errors/LJError.java +++ b/liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/LJError.java @@ -1,6 +1,6 @@ -package liquidjava.errors.errors; +package liquidjava.diagnostics.errors; -import liquidjava.errors.ErrorPosition; +import liquidjava.diagnostics.ErrorPosition; import liquidjava.utils.Utils; import spoon.reflect.cu.SourcePosition; import spoon.reflect.declaration.CtElement; diff --git a/liquidjava-verifier/src/main/java/liquidjava/errors/errors/NotFoundError.java b/liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/NotFoundError.java similarity index 90% rename from liquidjava-verifier/src/main/java/liquidjava/errors/errors/NotFoundError.java rename to liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/NotFoundError.java index 4a10e7ca..35758404 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/errors/errors/NotFoundError.java +++ b/liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/NotFoundError.java @@ -1,4 +1,4 @@ -package liquidjava.errors.errors; +package liquidjava.diagnostics.errors; import spoon.reflect.declaration.CtElement; diff --git a/liquidjava-verifier/src/main/java/liquidjava/errors/errors/RefinementError.java b/liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/RefinementError.java similarity index 95% rename from liquidjava-verifier/src/main/java/liquidjava/errors/errors/RefinementError.java rename to liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/RefinementError.java index 7fe05a59..614df079 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/errors/errors/RefinementError.java +++ b/liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/RefinementError.java @@ -1,4 +1,4 @@ -package liquidjava.errors.errors; +package liquidjava.diagnostics.errors; import liquidjava.rj_language.Predicate; import liquidjava.rj_language.opt.derivation_node.ValDerivationNode; diff --git a/liquidjava-verifier/src/main/java/liquidjava/errors/errors/StateConflictError.java b/liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/StateConflictError.java similarity index 96% rename from liquidjava-verifier/src/main/java/liquidjava/errors/errors/StateConflictError.java rename to liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/StateConflictError.java index fe829362..ad30b9ca 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/errors/errors/StateConflictError.java +++ b/liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/StateConflictError.java @@ -1,4 +1,4 @@ -package liquidjava.errors.errors; +package liquidjava.diagnostics.errors; import liquidjava.rj_language.Predicate; import spoon.reflect.declaration.CtElement; diff --git a/liquidjava-verifier/src/main/java/liquidjava/errors/errors/StateRefinementError.java b/liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/StateRefinementError.java similarity index 96% rename from liquidjava-verifier/src/main/java/liquidjava/errors/errors/StateRefinementError.java rename to liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/StateRefinementError.java index a787e197..93bdd4c7 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/errors/errors/StateRefinementError.java +++ b/liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/StateRefinementError.java @@ -1,4 +1,4 @@ -package liquidjava.errors.errors; +package liquidjava.diagnostics.errors; import java.util.Arrays; diff --git a/liquidjava-verifier/src/main/java/liquidjava/errors/errors/SyntaxError.java b/liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/SyntaxError.java similarity index 94% rename from liquidjava-verifier/src/main/java/liquidjava/errors/errors/SyntaxError.java rename to liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/SyntaxError.java index 639c67bd..bc5e9499 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/errors/errors/SyntaxError.java +++ b/liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/SyntaxError.java @@ -1,4 +1,4 @@ -package liquidjava.errors.errors; +package liquidjava.diagnostics.errors; import spoon.reflect.declaration.CtElement; diff --git a/liquidjava-verifier/src/main/java/liquidjava/errors/warnings/ExternalClassNotFoundWarning.java b/liquidjava-verifier/src/main/java/liquidjava/diagnostics/warnings/ExternalClassNotFoundWarning.java similarity index 94% rename from liquidjava-verifier/src/main/java/liquidjava/errors/warnings/ExternalClassNotFoundWarning.java rename to liquidjava-verifier/src/main/java/liquidjava/diagnostics/warnings/ExternalClassNotFoundWarning.java index 59a999f8..82641b6e 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/errors/warnings/ExternalClassNotFoundWarning.java +++ b/liquidjava-verifier/src/main/java/liquidjava/diagnostics/warnings/ExternalClassNotFoundWarning.java @@ -1,4 +1,4 @@ -package liquidjava.errors.warnings; +package liquidjava.diagnostics.warnings; import spoon.reflect.declaration.CtElement; diff --git a/liquidjava-verifier/src/main/java/liquidjava/errors/warnings/ExternalMethodNotFoundWarning.java b/liquidjava-verifier/src/main/java/liquidjava/diagnostics/warnings/ExternalMethodNotFoundWarning.java similarity index 95% rename from liquidjava-verifier/src/main/java/liquidjava/errors/warnings/ExternalMethodNotFoundWarning.java rename to liquidjava-verifier/src/main/java/liquidjava/diagnostics/warnings/ExternalMethodNotFoundWarning.java index 086a0210..3ffe40ca 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/errors/warnings/ExternalMethodNotFoundWarning.java +++ b/liquidjava-verifier/src/main/java/liquidjava/diagnostics/warnings/ExternalMethodNotFoundWarning.java @@ -1,4 +1,4 @@ -package liquidjava.errors.warnings; +package liquidjava.diagnostics.warnings; import spoon.reflect.declaration.CtElement; diff --git a/liquidjava-verifier/src/main/java/liquidjava/errors/warnings/LJWarning.java b/liquidjava-verifier/src/main/java/liquidjava/diagnostics/warnings/LJWarning.java similarity index 95% rename from liquidjava-verifier/src/main/java/liquidjava/errors/warnings/LJWarning.java rename to liquidjava-verifier/src/main/java/liquidjava/diagnostics/warnings/LJWarning.java index ac4d161e..8558843f 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/errors/warnings/LJWarning.java +++ b/liquidjava-verifier/src/main/java/liquidjava/diagnostics/warnings/LJWarning.java @@ -1,8 +1,8 @@ -package liquidjava.errors.warnings; +package liquidjava.diagnostics.warnings; import java.net.URI; -import liquidjava.errors.ErrorPosition; +import liquidjava.diagnostics.ErrorPosition; import liquidjava.utils.Utils; import spoon.reflect.cu.SourcePosition; import spoon.reflect.declaration.CtElement; diff --git a/liquidjava-verifier/src/main/java/liquidjava/processor/RefinementProcessor.java b/liquidjava-verifier/src/main/java/liquidjava/processor/RefinementProcessor.java index 2e168f76..46069f40 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/processor/RefinementProcessor.java +++ b/liquidjava-verifier/src/main/java/liquidjava/processor/RefinementProcessor.java @@ -2,7 +2,8 @@ import java.util.ArrayList; import java.util.List; -import liquidjava.errors.ErrorEmitter; + +import liquidjava.diagnostics.ErrorEmitter; import liquidjava.processor.ann_generation.FieldGhostsGeneration; import liquidjava.processor.context.Context; import liquidjava.processor.refinement_checker.ExternalRefinementTypeChecker; diff --git a/liquidjava-verifier/src/main/java/liquidjava/processor/ann_generation/FieldGhostsGeneration.java b/liquidjava-verifier/src/main/java/liquidjava/processor/ann_generation/FieldGhostsGeneration.java index 4e8b3987..dbe672f5 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/processor/ann_generation/FieldGhostsGeneration.java +++ b/liquidjava-verifier/src/main/java/liquidjava/processor/ann_generation/FieldGhostsGeneration.java @@ -1,6 +1,6 @@ package liquidjava.processor.ann_generation; -import liquidjava.errors.ErrorEmitter; +import liquidjava.diagnostics.ErrorEmitter; import liquidjava.processor.context.Context; import liquidjava.specification.Ghost; import spoon.reflect.declaration.*; diff --git a/liquidjava-verifier/src/main/java/liquidjava/processor/context/AliasWrapper.java b/liquidjava-verifier/src/main/java/liquidjava/processor/context/AliasWrapper.java index 6b149ca9..cb218d7e 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/processor/context/AliasWrapper.java +++ b/liquidjava-verifier/src/main/java/liquidjava/processor/context/AliasWrapper.java @@ -4,7 +4,8 @@ import java.util.HashMap; import java.util.List; import java.util.Map; -import liquidjava.errors.ErrorEmitter; + +import liquidjava.diagnostics.ErrorEmitter; import liquidjava.processor.facade.AliasDTO; import liquidjava.rj_language.Predicate; import liquidjava.rj_language.ast.Expression; diff --git a/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/ExternalRefinementTypeChecker.java b/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/ExternalRefinementTypeChecker.java index ae41e0d6..302545d9 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/ExternalRefinementTypeChecker.java +++ b/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/ExternalRefinementTypeChecker.java @@ -3,8 +3,9 @@ import java.util.Arrays; import java.util.List; import java.util.Optional; -import liquidjava.errors.ErrorEmitter; -import liquidjava.errors.ErrorHandler; + +import liquidjava.diagnostics.ErrorEmitter; +import liquidjava.diagnostics.ErrorHandler; import liquidjava.processor.context.Context; import liquidjava.processor.context.GhostFunction; import liquidjava.processor.facade.GhostDTO; diff --git a/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/MethodsFirstChecker.java b/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/MethodsFirstChecker.java index b4224d3b..92cadcf5 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/MethodsFirstChecker.java +++ b/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/MethodsFirstChecker.java @@ -2,7 +2,8 @@ import java.util.ArrayList; import java.util.List; -import liquidjava.errors.ErrorEmitter; + +import liquidjava.diagnostics.ErrorEmitter; import liquidjava.processor.context.Context; import liquidjava.processor.refinement_checker.general_checkers.MethodsFunctionsChecker; import liquidjava.rj_language.parsing.ParsingException; 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 6d46a535..ef6f2c55 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 @@ -4,7 +4,8 @@ import java.util.Arrays; import java.util.List; import java.util.Optional; -import liquidjava.errors.ErrorEmitter; + +import liquidjava.diagnostics.ErrorEmitter; import liquidjava.processor.context.*; import liquidjava.processor.refinement_checker.general_checkers.MethodsFunctionsChecker; import liquidjava.processor.refinement_checker.general_checkers.OperationsChecker; 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 6be78523..8b714d29 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 @@ -4,8 +4,9 @@ import java.util.Arrays; import java.util.List; import java.util.Optional; -import liquidjava.errors.ErrorEmitter; -import liquidjava.errors.ErrorHandler; + +import liquidjava.diagnostics.ErrorEmitter; +import liquidjava.diagnostics.ErrorHandler; import liquidjava.processor.context.AliasWrapper; import liquidjava.processor.context.Context; import liquidjava.processor.context.GhostFunction; 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 458ae4da..fcded1ce 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 @@ -8,8 +8,9 @@ import java.util.function.Consumer; import java.util.regex.Pattern; import java.util.stream.Collectors; -import liquidjava.errors.ErrorEmitter; -import liquidjava.errors.ErrorHandler; + +import liquidjava.diagnostics.ErrorEmitter; +import liquidjava.diagnostics.ErrorHandler; import liquidjava.processor.VCImplication; import liquidjava.processor.context.*; import liquidjava.rj_language.Predicate; 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 99f13890..0bd255f1 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 @@ -3,7 +3,8 @@ import java.lang.annotation.Annotation; import java.util.*; import java.util.stream.Collectors; -import liquidjava.errors.ErrorHandler; + +import liquidjava.diagnostics.ErrorHandler; import liquidjava.processor.context.*; import liquidjava.processor.refinement_checker.TypeChecker; import liquidjava.processor.refinement_checker.TypeCheckingUtils; diff --git a/liquidjava-verifier/src/main/java/liquidjava/rj_language/BuiltinFunctionPredicate.java b/liquidjava-verifier/src/main/java/liquidjava/rj_language/BuiltinFunctionPredicate.java index 62284b25..0b57ac50 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/rj_language/BuiltinFunctionPredicate.java +++ b/liquidjava-verifier/src/main/java/liquidjava/rj_language/BuiltinFunctionPredicate.java @@ -1,6 +1,6 @@ package liquidjava.rj_language; -import liquidjava.errors.ErrorEmitter; +import liquidjava.diagnostics.ErrorEmitter; import liquidjava.rj_language.parsing.ParsingException; import spoon.reflect.declaration.CtElement; diff --git a/liquidjava-verifier/src/main/java/liquidjava/rj_language/Predicate.java b/liquidjava-verifier/src/main/java/liquidjava/rj_language/Predicate.java index 7fb7fa94..1f476f15 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/rj_language/Predicate.java +++ b/liquidjava-verifier/src/main/java/liquidjava/rj_language/Predicate.java @@ -5,8 +5,9 @@ import java.util.List; import java.util.Map; import java.util.stream.Collectors; -import liquidjava.errors.ErrorEmitter; -import liquidjava.errors.ErrorHandler; + +import liquidjava.diagnostics.ErrorEmitter; +import liquidjava.diagnostics.ErrorHandler; import liquidjava.processor.context.AliasWrapper; import liquidjava.processor.context.Context; import liquidjava.processor.context.GhostState; diff --git a/liquidjava-verifier/src/test/java/liquidjava/api/tests/TestExamples.java b/liquidjava-verifier/src/test/java/liquidjava/api/tests/TestExamples.java index a1c627f9..7f216a32 100644 --- a/liquidjava-verifier/src/test/java/liquidjava/api/tests/TestExamples.java +++ b/liquidjava-verifier/src/test/java/liquidjava/api/tests/TestExamples.java @@ -8,7 +8,7 @@ import java.nio.file.Paths; import java.util.stream.Stream; import liquidjava.api.CommandLineLauncher; -import liquidjava.errors.ErrorEmitter; +import liquidjava.diagnostics.ErrorEmitter; import org.junit.Test; import org.junit.jupiter.params.ParameterizedTest; From bc965c6eb54eeb70f746a7271192ba411c8e3024 Mon Sep 17 00:00:00 2001 From: Ricardo Costa Date: Wed, 5 Nov 2025 16:52:30 +0000 Subject: [PATCH 3/4] Add JavaDocs to Classes --- .../java/liquidjava/diagnostics/errors/CustomError.java | 4 ++++ .../liquidjava/diagnostics/errors/GhostInvocationError.java | 5 ++++- .../errors/IllegalConstructorTransitionError.java | 5 ++++- .../diagnostics/errors/InvalidRefinementError.java | 5 ++++- .../main/java/liquidjava/diagnostics/errors/LJError.java | 4 +++- .../java/liquidjava/diagnostics/errors/NotFoundError.java | 5 ++++- .../java/liquidjava/diagnostics/errors/RefinementError.java | 5 ++++- .../liquidjava/diagnostics/errors/StateConflictError.java | 5 ++++- .../liquidjava/diagnostics/errors/StateRefinementError.java | 5 ++++- .../java/liquidjava/diagnostics/errors/SyntaxError.java | 5 ++++- .../diagnostics/warnings/ExternalClassNotFoundWarning.java | 5 ++++- .../diagnostics/warnings/ExternalMethodNotFoundWarning.java | 5 ++++- .../java/liquidjava/diagnostics/warnings/LJWarning.java | 6 +++--- 13 files changed, 50 insertions(+), 14 deletions(-) diff --git a/liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/CustomError.java b/liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/CustomError.java index 7fd67b13..3a91a35a 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/CustomError.java +++ b/liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/CustomError.java @@ -1,5 +1,9 @@ package liquidjava.diagnostics.errors; +/** + * Custom error with an arbitrary message + * @see LJError + */ public class CustomError extends LJError { public CustomError(String message) { diff --git a/liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/GhostInvocationError.java b/liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/GhostInvocationError.java index 1dd6db16..759dd503 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/GhostInvocationError.java +++ b/liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/GhostInvocationError.java @@ -3,7 +3,10 @@ import liquidjava.rj_language.Predicate; import spoon.reflect.declaration.CtElement; -// when a ghost call has wrong types or number of arguments +/** + * Error indicating that a ghost method invocation is invalid (e.g., has wrong arguments) + * @see LJError + */ public class GhostInvocationError extends LJError { private Predicate expected; diff --git a/liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/IllegalConstructorTransitionError.java b/liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/IllegalConstructorTransitionError.java index 14045f31..9cc2b46f 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/IllegalConstructorTransitionError.java +++ b/liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/IllegalConstructorTransitionError.java @@ -2,7 +2,10 @@ import spoon.reflect.declaration.CtElement; -// when a constructor contains a @StateRefinement with a from state +/** + * Error indicating that a constructor contains a state refinement with a 'from' state, which is not allowed + * @see LJError + */ public class IllegalConstructorTransitionError extends LJError { public IllegalConstructorTransitionError(CtElement element) { diff --git a/liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/InvalidRefinementError.java b/liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/InvalidRefinementError.java index c3686a0e..24b38936 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/InvalidRefinementError.java +++ b/liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/InvalidRefinementError.java @@ -2,7 +2,10 @@ import spoon.reflect.declaration.CtElement; -// when a refinement is invalid, e.g. is not a boolean expression +/** + * Error indicating that a refinement is invalid (e.g., not a boolean expression) + * @see LJError + */ public class InvalidRefinementError extends LJError { private String refinement; 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 f6c3501b..6e92057f 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/LJError.java +++ b/liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/LJError.java @@ -5,7 +5,9 @@ import spoon.reflect.cu.SourcePosition; import spoon.reflect.declaration.CtElement; -// base class for all LiquidJava errors +/** + * Base class for all LiquidJava errors + */ public abstract class LJError extends Exception { private String title; diff --git a/liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/NotFoundError.java b/liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/NotFoundError.java index 35758404..3be93de8 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/NotFoundError.java +++ b/liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/NotFoundError.java @@ -2,7 +2,10 @@ import spoon.reflect.declaration.CtElement; -// e.g. when a variable used in a refinement is not found +/** + * Error indicating that an element referenced in a refinement was not found + * @see LJError + */ public class NotFoundError extends LJError { public NotFoundError(String message, CtElement element) { 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 614df079..15575269 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/RefinementError.java +++ b/liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/RefinementError.java @@ -5,7 +5,10 @@ import liquidjava.utils.Utils; import spoon.reflect.declaration.CtElement; -// when a @Refinement is violated +/** + * Error indicating that a refinement constraint either was violated or cannot be proven + * @see LJError + */ public class RefinementError extends LJError { private Predicate expected; diff --git a/liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/StateConflictError.java b/liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/StateConflictError.java index ad30b9ca..b86a55db 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/StateConflictError.java +++ b/liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/StateConflictError.java @@ -3,7 +3,10 @@ import liquidjava.rj_language.Predicate; import spoon.reflect.declaration.CtElement; -// when two incompatible states are found in a state set +/** + * Error indicating that two disjoint states were found in a state refinement + * @see LJError + */ public class StateConflictError extends LJError { private Predicate predicate; 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 93bdd4c7..87533876 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/StateRefinementError.java +++ b/liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/StateRefinementError.java @@ -4,7 +4,10 @@ import spoon.reflect.declaration.CtElement; -// when a @StateRefinement is violated +/** + * Error indicating that a state refinement transition was violated + * @see LJError + */ public class StateRefinementError extends LJError { private final String method; diff --git a/liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/SyntaxError.java b/liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/SyntaxError.java index bc5e9499..9f551f2d 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/SyntaxError.java +++ b/liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/SyntaxError.java @@ -2,7 +2,10 @@ import spoon.reflect.declaration.CtElement; -// when the syntax of a refinement is invalid +/** + * Error indicating that the syntax of a refinement is invalid + * @see LJError + */ public class SyntaxError extends LJError { private String refinement; diff --git a/liquidjava-verifier/src/main/java/liquidjava/diagnostics/warnings/ExternalClassNotFoundWarning.java b/liquidjava-verifier/src/main/java/liquidjava/diagnostics/warnings/ExternalClassNotFoundWarning.java index 82641b6e..bf74cc88 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/diagnostics/warnings/ExternalClassNotFoundWarning.java +++ b/liquidjava-verifier/src/main/java/liquidjava/diagnostics/warnings/ExternalClassNotFoundWarning.java @@ -2,7 +2,10 @@ import spoon.reflect.declaration.CtElement; -// when a class referenced in an external refinement cannot be found +/** + * Warning indicating that a class referenced in an external refinement was not found + * @see LJWarning + */ public class ExternalClassNotFoundWarning extends LJWarning { private String className; diff --git a/liquidjava-verifier/src/main/java/liquidjava/diagnostics/warnings/ExternalMethodNotFoundWarning.java b/liquidjava-verifier/src/main/java/liquidjava/diagnostics/warnings/ExternalMethodNotFoundWarning.java index 3ffe40ca..1b34c3e2 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/diagnostics/warnings/ExternalMethodNotFoundWarning.java +++ b/liquidjava-verifier/src/main/java/liquidjava/diagnostics/warnings/ExternalMethodNotFoundWarning.java @@ -2,7 +2,10 @@ import spoon.reflect.declaration.CtElement; -// when a method referenced in an external refinement cannot be found +/** + * Warning indicating that a method referenced in an external refinement was not found + * @see LJWarning + */ public class ExternalMethodNotFoundWarning extends LJWarning { private String methodName; 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 8558843f..7cf59dd9 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/diagnostics/warnings/LJWarning.java +++ b/liquidjava-verifier/src/main/java/liquidjava/diagnostics/warnings/LJWarning.java @@ -1,13 +1,13 @@ package liquidjava.diagnostics.warnings; -import java.net.URI; - import liquidjava.diagnostics.ErrorPosition; import liquidjava.utils.Utils; import spoon.reflect.cu.SourcePosition; import spoon.reflect.declaration.CtElement; -// base class for all LiquidJava warnings +/** + * Base class for all LiquidJava warnings + */ public abstract class LJWarning { private String message; From abd67d3ed3aca803545fee4efd89fa0b34b9c9b0 Mon Sep 17 00:00:00 2001 From: Ricardo Costa Date: Wed, 5 Nov 2025 16:58:00 +0000 Subject: [PATCH 4/4] Fix Import --- .../src/main/java/liquidjava/diagnostics/errors/CustomError.java | 1 + .../java/liquidjava/diagnostics/errors/GhostInvocationError.java | 1 + .../diagnostics/errors/IllegalConstructorTransitionError.java | 1 + .../liquidjava/diagnostics/errors/InvalidRefinementError.java | 1 + .../main/java/liquidjava/diagnostics/errors/NotFoundError.java | 1 + .../main/java/liquidjava/diagnostics/errors/RefinementError.java | 1 + .../java/liquidjava/diagnostics/errors/StateConflictError.java | 1 + .../java/liquidjava/diagnostics/errors/StateRefinementError.java | 1 + .../src/main/java/liquidjava/diagnostics/errors/SyntaxError.java | 1 + .../diagnostics/warnings/ExternalClassNotFoundWarning.java | 1 + .../diagnostics/warnings/ExternalMethodNotFoundWarning.java | 1 + .../refinement_checker/ExternalRefinementTypeChecker.java | 1 + 12 files changed, 12 insertions(+) diff --git a/liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/CustomError.java b/liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/CustomError.java index 3a91a35a..7f885e45 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/CustomError.java +++ b/liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/CustomError.java @@ -2,6 +2,7 @@ /** * Custom error with an arbitrary message + * * @see LJError */ public class CustomError extends LJError { diff --git a/liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/GhostInvocationError.java b/liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/GhostInvocationError.java index 759dd503..7d04e28d 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/GhostInvocationError.java +++ b/liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/GhostInvocationError.java @@ -5,6 +5,7 @@ /** * Error indicating that a ghost method invocation is invalid (e.g., has wrong arguments) + * * @see LJError */ public class GhostInvocationError extends LJError { diff --git a/liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/IllegalConstructorTransitionError.java b/liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/IllegalConstructorTransitionError.java index 9cc2b46f..af5f05c6 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/IllegalConstructorTransitionError.java +++ b/liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/IllegalConstructorTransitionError.java @@ -4,6 +4,7 @@ /** * Error indicating that a constructor contains a state refinement with a 'from' state, which is not allowed + * * @see LJError */ public class IllegalConstructorTransitionError extends LJError { diff --git a/liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/InvalidRefinementError.java b/liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/InvalidRefinementError.java index 24b38936..02b41265 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/InvalidRefinementError.java +++ b/liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/InvalidRefinementError.java @@ -4,6 +4,7 @@ /** * Error indicating that a refinement is invalid (e.g., not a boolean expression) + * * @see LJError */ public class InvalidRefinementError extends LJError { diff --git a/liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/NotFoundError.java b/liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/NotFoundError.java index 3be93de8..77d1ab1f 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/NotFoundError.java +++ b/liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/NotFoundError.java @@ -4,6 +4,7 @@ /** * Error indicating that an element referenced in a refinement was not found + * * @see LJError */ public class NotFoundError extends LJError { 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 15575269..051e5d95 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/RefinementError.java +++ b/liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/RefinementError.java @@ -7,6 +7,7 @@ /** * Error indicating that a refinement constraint either was violated or cannot be proven + * * @see LJError */ public class RefinementError extends LJError { diff --git a/liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/StateConflictError.java b/liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/StateConflictError.java index b86a55db..0a9ec435 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/StateConflictError.java +++ b/liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/StateConflictError.java @@ -5,6 +5,7 @@ /** * Error indicating that two disjoint states were found in a state refinement + * * @see LJError */ public class StateConflictError extends LJError { 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 87533876..5810946d 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/StateRefinementError.java +++ b/liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/StateRefinementError.java @@ -6,6 +6,7 @@ /** * Error indicating that a state refinement transition was violated + * * @see LJError */ public class StateRefinementError extends LJError { diff --git a/liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/SyntaxError.java b/liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/SyntaxError.java index 9f551f2d..ba679cc6 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/SyntaxError.java +++ b/liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/SyntaxError.java @@ -4,6 +4,7 @@ /** * Error indicating that the syntax of a refinement is invalid + * * @see LJError */ public class SyntaxError extends LJError { diff --git a/liquidjava-verifier/src/main/java/liquidjava/diagnostics/warnings/ExternalClassNotFoundWarning.java b/liquidjava-verifier/src/main/java/liquidjava/diagnostics/warnings/ExternalClassNotFoundWarning.java index bf74cc88..6a4eef29 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/diagnostics/warnings/ExternalClassNotFoundWarning.java +++ b/liquidjava-verifier/src/main/java/liquidjava/diagnostics/warnings/ExternalClassNotFoundWarning.java @@ -4,6 +4,7 @@ /** * Warning indicating that a class referenced in an external refinement was not found + * * @see LJWarning */ public class ExternalClassNotFoundWarning extends LJWarning { diff --git a/liquidjava-verifier/src/main/java/liquidjava/diagnostics/warnings/ExternalMethodNotFoundWarning.java b/liquidjava-verifier/src/main/java/liquidjava/diagnostics/warnings/ExternalMethodNotFoundWarning.java index 1b34c3e2..eee01505 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/diagnostics/warnings/ExternalMethodNotFoundWarning.java +++ b/liquidjava-verifier/src/main/java/liquidjava/diagnostics/warnings/ExternalMethodNotFoundWarning.java @@ -4,6 +4,7 @@ /** * Warning indicating that a method referenced in an external refinement was not found + * * @see LJWarning */ public class ExternalMethodNotFoundWarning extends LJWarning { diff --git a/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/ExternalRefinementTypeChecker.java b/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/ExternalRefinementTypeChecker.java index 56d024f5..8580135b 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/ExternalRefinementTypeChecker.java +++ b/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/ExternalRefinementTypeChecker.java @@ -3,6 +3,7 @@ import java.util.Arrays; import java.util.List; import java.util.Optional; +import java.util.stream.Collectors; import liquidjava.diagnostics.ErrorEmitter; import liquidjava.diagnostics.ErrorHandler;