From 9f3cd0a414f80205297e22549cbc3b3ff4aa6616 Mon Sep 17 00:00:00 2001 From: Ricardo Costa Date: Thu, 20 Nov 2025 19:23:37 +0000 Subject: [PATCH 1/3] Check Java Compilation Before Verification This approach is not ideal since a compilation error in a single file causes the whole verification to be skipped for the whole directory. --- .../src/main/java/liquidjava/api/CommandLineLauncher.java | 7 ++++++- 1 file changed, 6 insertions(+), 1 deletion(-) diff --git a/liquidjava-verifier/src/main/java/liquidjava/api/CommandLineLauncher.java b/liquidjava-verifier/src/main/java/liquidjava/api/CommandLineLauncher.java index 6a066f7b..513092c8 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/api/CommandLineLauncher.java +++ b/liquidjava-verifier/src/main/java/liquidjava/api/CommandLineLauncher.java @@ -54,7 +54,12 @@ public static void launch(String... paths) { } launcher.getEnvironment().setNoClasspath(true); launcher.getEnvironment().setComplianceLevel(8); - launcher.run(); + + boolean buildSuccess = launcher.getModelBuilder().build(); + if (!buildSuccess) { + diagnostics.add(new CustomError("Java compilation error detected. Skipping verification.")); + return; + } final Factory factory = launcher.getFactory(); final ProcessingManager processingManager = new QueueProcessingManager(factory); From c851e91b7c90a786dce4615a5be0b7d7a38580c1 Mon Sep 17 00:00:00 2001 From: Ricardo Costa Date: Fri, 21 Nov 2025 14:36:39 +0000 Subject: [PATCH 2/3] Report Warning Instead of Error --- .../liquidjava/api/CommandLineLauncher.java | 4 ++-- .../diagnostics/warnings/CustomWarning.java | 20 +++++++++++++++++++ .../ExternalClassNotFoundWarning.java | 6 +++--- .../ExternalMethodNotFoundWarning.java | 6 +++--- .../ExternalRefinementTypeChecker.java | 6 +++--- 5 files changed, 31 insertions(+), 11 deletions(-) create mode 100644 liquidjava-verifier/src/main/java/liquidjava/diagnostics/warnings/CustomWarning.java diff --git a/liquidjava-verifier/src/main/java/liquidjava/api/CommandLineLauncher.java b/liquidjava-verifier/src/main/java/liquidjava/api/CommandLineLauncher.java index 513092c8..e27cbc1c 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/api/CommandLineLauncher.java +++ b/liquidjava-verifier/src/main/java/liquidjava/api/CommandLineLauncher.java @@ -6,6 +6,7 @@ import liquidjava.diagnostics.Diagnostics; import liquidjava.diagnostics.errors.CustomError; +import liquidjava.diagnostics.warnings.CustomWarning; import liquidjava.processor.RefinementProcessor; import spoon.Launcher; import spoon.processing.ProcessingManager; @@ -57,8 +58,7 @@ public static void launch(String... paths) { boolean buildSuccess = launcher.getModelBuilder().build(); if (!buildSuccess) { - diagnostics.add(new CustomError("Java compilation error detected. Skipping verification.")); - return; + diagnostics.add(new CustomWarning("Java compilation error detected")); } final Factory factory = launcher.getFactory(); diff --git a/liquidjava-verifier/src/main/java/liquidjava/diagnostics/warnings/CustomWarning.java b/liquidjava-verifier/src/main/java/liquidjava/diagnostics/warnings/CustomWarning.java new file mode 100644 index 00000000..22e5917d --- /dev/null +++ b/liquidjava-verifier/src/main/java/liquidjava/diagnostics/warnings/CustomWarning.java @@ -0,0 +1,20 @@ +package liquidjava.diagnostics.warnings; + +import spoon.reflect.cu.SourcePosition; + +/** + * Custom warning with a message + * + * @see LJWarning + */ +public class CustomWarning extends LJWarning { + + public CustomWarning(SourcePosition position, String message) { + super(message, position); + } + + public CustomWarning(String message) { + super(message, null); + } + +} 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 86438b6b..356542f0 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/diagnostics/warnings/ExternalClassNotFoundWarning.java +++ b/liquidjava-verifier/src/main/java/liquidjava/diagnostics/warnings/ExternalClassNotFoundWarning.java @@ -1,6 +1,6 @@ package liquidjava.diagnostics.warnings; -import spoon.reflect.declaration.CtElement; +import spoon.reflect.cu.SourcePosition; /** * Warning indicating that a class referenced in an external refinement was not found @@ -11,8 +11,8 @@ public class ExternalClassNotFoundWarning extends LJWarning { private final String className; - public ExternalClassNotFoundWarning(CtElement element, String message, String className) { - super(message, element.getPosition()); + public ExternalClassNotFoundWarning(SourcePosition position, String message, String className) { + super(message, position); this.className = 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 60f20f17..c9f573ae 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/diagnostics/warnings/ExternalMethodNotFoundWarning.java +++ b/liquidjava-verifier/src/main/java/liquidjava/diagnostics/warnings/ExternalMethodNotFoundWarning.java @@ -1,6 +1,6 @@ package liquidjava.diagnostics.warnings; -import spoon.reflect.declaration.CtElement; +import spoon.reflect.cu.SourcePosition; /** * Warning indicating that a method referenced in an external refinement was not found @@ -13,9 +13,9 @@ public class ExternalMethodNotFoundWarning extends LJWarning { private final String className; private final String[] overloads; - public ExternalMethodNotFoundWarning(CtElement element, String message, String methodName, String className, + public ExternalMethodNotFoundWarning(SourcePosition position, String message, String methodName, String className, String[] overloads) { - super(message, element.getPosition()); + super(message, position); this.methodName = methodName; this.className = className; this.overloads = overloads; 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 a52ac891..7bd910b6 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 @@ -43,7 +43,7 @@ public void visitCtInterface(CtInterface intrface) { this.prefix = externalRefinements.get(); if (!classExists(prefix)) { String message = String.format("Could not find class '%s'", prefix); - diagnostics.add(new ExternalClassNotFoundWarning(intrface, message, prefix)); + diagnostics.add(new ExternalClassNotFoundWarning(intrface.getPosition(), message, prefix)); return; } getRefinementFromAnnotation(intrface); @@ -72,7 +72,7 @@ public void visitCtMethod(CtMethod method) { prefix); String[] overloads = getOverloads(targetType, method); diagnostics.add( - new ExternalMethodNotFoundWarning(method, message, method.getSignature(), prefix, overloads)); + new ExternalMethodNotFoundWarning(method.getPosition(), message, method.getSignature(), prefix, overloads)); } } else { if (!methodExists(targetType, method)) { @@ -80,7 +80,7 @@ public void visitCtMethod(CtMethod method) { method.getType().getSimpleName(), method.getSignature(), prefix); String[] overloads = getOverloads(targetType, method); diagnostics.add( - new ExternalMethodNotFoundWarning(method, message, method.getSignature(), prefix, overloads)); + new ExternalMethodNotFoundWarning(method.getPosition(), message, method.getSignature(), prefix, overloads)); return; } } From da2bfce9e17de063cf31b026259b87b88545ce1b Mon Sep 17 00:00:00 2001 From: Ricardo Costa Date: Fri, 21 Nov 2025 14:45:08 +0000 Subject: [PATCH 3/3] Improve Message --- .../src/main/java/liquidjava/api/CommandLineLauncher.java | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/liquidjava-verifier/src/main/java/liquidjava/api/CommandLineLauncher.java b/liquidjava-verifier/src/main/java/liquidjava/api/CommandLineLauncher.java index e27cbc1c..e7efeff6 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/api/CommandLineLauncher.java +++ b/liquidjava-verifier/src/main/java/liquidjava/api/CommandLineLauncher.java @@ -58,7 +58,7 @@ public static void launch(String... paths) { boolean buildSuccess = launcher.getModelBuilder().build(); if (!buildSuccess) { - diagnostics.add(new CustomWarning("Java compilation error detected")); + diagnostics.add(new CustomWarning("Java compilation error detected. Verification might be affected.")); } final Factory factory = launcher.getFactory();