Cleanup

liquidjava-verifier/src/main/java/liquidjava/api/CommandLineLauncher.java

@@ -30,7 +30,9 @@ public static void main(String[] args) {
         launch(paths.toArray(new String[0]));
 
         // print diagnostics
-        System.out.println(diagnostics.getWarningOutput());
+        if (diagnostics.foundWarning()) {
+            System.out.println(diagnostics.getWarningOutput());
+        }
         if (diagnostics.foundError()) {
             System.out.println(diagnostics.getErrorOutput());
         } else {
@@ -50,7 +52,6 @@ public static void launch(String... paths) {
             }
             launcher.addInputResource(path);
         }
-
         launcher.getEnvironment().setNoClasspath(true);
         launcher.getEnvironment().setComplianceLevel(8);
         launcher.run();
@@ -60,16 +61,9 @@ public static void launch(String... paths) {
         final RefinementProcessor processor = new RefinementProcessor(factory);
         processingManager.addProcessor(processor);
 
-        try {
-            // analyze all packages
-            CtPackage root = factory.Package().getRootPackage();
-            if (root != null)
-                processingManager.process(root);
-        } catch (Exception e) {
-            e.printStackTrace();
-            throw e;
-        }
-
-        return;
+        // analyze all packages
+        CtPackage root = factory.Package().getRootPackage();
+        if (root != null)
+            processingManager.process(root);
     }
 }

liquidjava-verifier/src/main/java/liquidjava/diagnostics/Colors.java

@@ -3,10 +3,7 @@
 // ANSI color codes
 public class Colors {
     public static final String RESET = "\u001B[0m";
-    public static final String BOLD = "\u001B[1m";
     public static final String GREY = "\u001B[90m";
-    public static final String RED = "\u001B[31m";
     public static final String BOLD_RED = "\u001B[1;31m";
-    public static final String YELLOW = "\u001B[33m";
     public static final String BOLD_YELLOW = "\u001B[1;33m";
 }

liquidjava-verifier/src/main/java/liquidjava/diagnostics/Diagnostics.java

@@ -13,8 +13,8 @@
 public class Diagnostics {
     private static final Diagnostics instance = new Diagnostics();
 
-    private LinkedHashSet<LJError> errors;
-    private LinkedHashSet<LJWarning> warnings;
+    private final LinkedHashSet<LJError> errors;
+    private final LinkedHashSet<LJWarning> warnings;
 
     private Diagnostics() {
         this.errors = new LinkedHashSet<>();

liquidjava-verifier/src/main/java/liquidjava/diagnostics/ErrorPosition.java

@@ -2,59 +2,11 @@
 
 import spoon.reflect.cu.SourcePosition;
 
-public class ErrorPosition {
-
-    private int lineStart;
-    private int colStart;
-    private int lineEnd;
-    private int colEnd;
-
-    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() {
-        return lineStart;
-    }
-
-    public int getColStart() {
-        return colStart;
-    }
-
-    public int getLineEnd() {
-        return lineEnd;
-    }
-
-    public int getColEnd() {
-        return colEnd;
-    }
+public record ErrorPosition(int lineStart, int colStart, int lineEnd, int 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());
     }
-
-    @Override
-    public boolean equals(Object obj) {
-        if (this == obj)
-            return true;
-        if (obj == null || getClass() != obj.getClass())
-            return false;
-        ErrorPosition other = (ErrorPosition) obj;
-        return lineStart == other.lineStart && colStart == other.colStart && lineEnd == other.lineEnd
-                && colEnd == other.colEnd;
-    }
-
-    @Override
-    public int hashCode() {
-        int result = lineStart;
-        result = 31 * result + colStart;
-        result = 31 * result + lineEnd;
-        result = 31 * result + colEnd;
-        return result;
-    }
 }

liquidjava-verifier/src/main/java/liquidjava/diagnostics/LJDiagnostic.java

@@ -8,12 +8,12 @@
 
 public class LJDiagnostic extends RuntimeException {
 
-    private String title;
-    private String message;
-    private String details;
-    private String file;
-    private ErrorPosition position;
-    private String accentColor;
+    private final String title;
+    private final String message;
+    private final String details;
+    private final String file;
+    private final ErrorPosition position;
+    private final String accentColor;
 
     public LJDiagnostic(String title, String message, String details, SourcePosition pos, String accentColor) {
         this.title = title;
@@ -65,7 +65,7 @@ public String toString() {
 
         // location
         if (file != null && position != null) {
-            sb.append("\n").append(file).append(":").append(position.getLineStart()).append(Colors.RESET).append("\n");
+            sb.append("\n").append(file).append(":").append(position.lineStart()).append(Colors.RESET).append("\n");
         }
 
         return sb.toString();
@@ -83,12 +83,11 @@ public String getSnippet() {
             // before and after lines for context
             int contextBefore = 2;
             int contextAfter = 2;
-            int startLine = Math.max(1, position.getLineStart() - contextBefore);
-            int endLine = Math.min(lines.size(), position.getLineEnd() + contextAfter);
+            int startLine = Math.max(1, position.lineStart() - contextBefore);
+            int endLine = Math.min(lines.size(), position.lineEnd() + contextAfter);
 
             // calculate padding for line numbers
-            int maxLineNum = endLine;
-            int padding = String.valueOf(maxLineNum).length();
+            int padding = String.valueOf(endLine).length();
 
             for (int i = startLine; i <= endLine; i++) {
                 String lineNumStr = String.format("%" + padding + "d", i);
@@ -98,9 +97,9 @@ public String getSnippet() {
                 sb.append(Colors.GREY).append(lineNumStr).append(" | ").append(line).append(Colors.RESET).append("\n");
 
                 // add error markers on the line(s) with the error
-                if (i >= position.getLineStart() && i <= position.getLineEnd()) {
-                    int colStart = (i == position.getLineStart()) ? position.getColStart() : 1;
-                    int colEnd = (i == position.getLineEnd()) ? position.getColEnd() : line.length();
+                if (i >= position.lineStart() && i <= position.lineEnd()) {
+                    int colStart = (i == position.lineStart()) ? position.colStart() : 1;
+                    int colEnd = (i == position.lineEnd()) ? position.colEnd() : line.length();
 
                     if (colStart > 0 && colEnd > 0) {
                         // line number padding + " | " + column offset

liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/GhostInvocationError.java

@@ -11,7 +11,7 @@
  */
 public class GhostInvocationError extends LJError {
 
-    private String expected;
+    private final String expected;
 
     public GhostInvocationError(String message, SourcePosition pos, Expression expected,
             TranslationTable translationTable) {

liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/InvalidRefinementError.java

@@ -9,7 +9,7 @@
  */
 public class InvalidRefinementError extends LJError {
 
-    private String refinement;
+    private final String refinement;
 
     public InvalidRefinementError(CtElement element, String message, String refinement) {
         super("Invalid Refinement", message, "", element.getPosition(), null);

liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/LJError.java

@@ -10,7 +10,7 @@
  */
 public abstract class LJError extends LJDiagnostic {
 
-    private TranslationTable translationTable;
+    private final TranslationTable translationTable;
 
     public LJError(String title, String message, String details, SourcePosition pos,
             TranslationTable translationTable) {

liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/RefinementError.java

@@ -12,8 +12,8 @@
  */
 public class RefinementError extends LJError {
 
-    private String expected;
-    private ValDerivationNode found;
+    private final String expected;
+    private final ValDerivationNode found;
 
     public RefinementError(CtElement element, Expression expected, ValDerivationNode found,
             TranslationTable translationTable) {

liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/StateConflictError.java

@@ -11,8 +11,8 @@
  */
 public class StateConflictError extends LJError {
 
-    private String state;
-    private String className;
+    private final String state;
+    private final String className;
 
     public StateConflictError(CtElement element, Expression state, String className,
             TranslationTable translationTable) {

liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/SyntaxError.java

@@ -9,7 +9,7 @@
  */
 public class SyntaxError extends LJError {
 
-    private String refinement;
+    private final String refinement;
 
     public SyntaxError(String message, String refinement) {
         this(message, null, refinement);

liquidjava-verifier/src/main/java/liquidjava/diagnostics/warnings/ExternalClassNotFoundWarning.java

@@ -9,7 +9,7 @@
  */
 public class ExternalClassNotFoundWarning extends LJWarning {
 
-    private String className;
+    private final String className;
 
     public ExternalClassNotFoundWarning(CtElement element, String message, String className) {
         super(message, "", element.getPosition());

liquidjava-verifier/src/main/java/liquidjava/diagnostics/warnings/ExternalMethodNotFoundWarning.java

@@ -9,8 +9,8 @@
  */
 public class ExternalMethodNotFoundWarning extends LJWarning {
 
-    private String methodName;
-    private String className;
+    private final String methodName;
+    private final String className;
 
     public ExternalMethodNotFoundWarning(CtElement element, String message, String details, String methodName,
             String className) {

liquidjava-verifier/src/main/java/liquidjava/processor/VCImplication.java

@@ -32,7 +32,7 @@ public String toString() {
             String qualType = type.getQualifiedName();
             String simpleType = qualType.contains(".") ? Utils.getSimpleName(qualType) : qualType;
             return String.format("%-20s %s %s", "∀" + name + ":" + simpleType + ",", refinement.toString(),
-                    next != null ? " => \n" + next.toString() : "");
+                    next != null ? " => \n" + next : "");
         } else
             return String.format("%-20s %s", "", refinement.toString());
     }

liquidjava-verifier/src/main/java/liquidjava/processor/ann_generation/FieldGhostsGeneration.java

@@ -28,10 +28,10 @@ public Factory getFactory() {
     public <T> void visitCtClass(CtClass<T> ctClass) {
         ctClass.getDeclaredFields().stream().filter(fld -> fld.getType().getQualifiedName().equals("int"))
                 .forEach(fld -> {
-                    CtTypeReference<?> fld_type = fld.getType();
-                    CtAnnotation<?> gen_ann = factory.createAnnotation(factory.createCtTypeReference(Ghost.class));
-                    gen_ann.addValue("value", fld_type.getSimpleName() + " " + fld.getSimpleName());
-                    ctClass.addAnnotation(gen_ann);
+                    CtTypeReference<?> fldType = fld.getType();
+                    CtAnnotation<?> genAnn = factory.createAnnotation(factory.createCtTypeReference(Ghost.class));
+                    genAnn.addValue("value", fldType.getSimpleName() + " " + fld.getSimpleName());
+                    ctClass.addAnnotation(genAnn);
                 });
 
         super.visitCtClass(ctClass);