Improvements

Author: rcosta358

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

@@ -1,5 +1,6 @@
 package liquidjava.diagnostics.errors;
 
+import spoon.reflect.cu.SourcePosition;
 import spoon.reflect.declaration.CtElement;
 
 /**
@@ -10,11 +11,15 @@
 public class CustomError extends LJError {
 
     public CustomError(String message) {
-        super("Found Error", message, null, null);
+        super("Found Error", message, null, null, null);
+    }
+
+    public CustomError(String message, SourcePosition pos) {
+        super("Found Error", message, pos, null, null);
     }
 
     public CustomError(CtElement element, String message) {
-        super("Found Error", message, element, null);
+        super("Found Error", message, element.getPosition(), element.toString(), null);
     }
 
     @Override

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

@@ -2,7 +2,7 @@
 
 import liquidjava.diagnostics.TranslationTable;
 import liquidjava.rj_language.Predicate;
-import spoon.reflect.declaration.CtElement;
+import spoon.reflect.cu.SourcePosition;
 
 /**
  * Error indicating that a ghost method invocation is invalid (e.g., has wrong arguments)
@@ -13,9 +13,9 @@ public class GhostInvocationError extends LJError {
 
     private String expected;
 
-    public GhostInvocationError(CtElement element, Predicate expected, TranslationTable translationTable) {
-        super("Ghost Invocation Error", "Invalid types or number of arguments in ghost invocation", element,
-                translationTable);
+    public GhostInvocationError(String message, SourcePosition pos, Predicate expected,
+            TranslationTable translationTable) {
+        super("Ghost Invocation Error", message, pos, null, translationTable);
         this.expected = expected.toString();
     }
 

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

@@ -11,7 +11,8 @@ 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, null);
+                "Found constructor with 'from' state (should only have a 'to' state)", element.getPosition(),
+                element.toString(), null);
     }
 
     @Override

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

@@ -12,7 +12,7 @@ public class InvalidRefinementError extends LJError {
     private String refinement;
 
     public InvalidRefinementError(CtElement element, String message, String refinement) {
-        super("Invalid Refinement", message, element, null);
+        super("Invalid Refinement", message, element.getPosition(), element.toString(), null);
         this.refinement = refinement;
     }
 

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

@@ -4,33 +4,27 @@
 import liquidjava.diagnostics.TranslationTable;
 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 {
+public abstract class LJError {
 
     private String title;
     private String message;
-    private CtElement element;
+    private String snippet;
     private ErrorPosition position;
     private SourcePosition location;
     private TranslationTable translationTable;
 
-    public LJError(String title, String message, CtElement element, TranslationTable translationTable) {
-        super(message);
+    public LJError(String title, String message, SourcePosition pos, String snippet,
+            TranslationTable translationTable) {
         this.title = title;
         this.message = message;
-        this.element = element;
+        this.snippet = snippet;
         this.translationTable = translationTable != null ? translationTable : new TranslationTable();
-        try {
-            this.location = element.getPosition();
-            this.position = ErrorPosition.fromSpoonPosition(element.getPosition());
-        } catch (Exception e) {
-            this.location = null;
-            this.position = null;
-        }
+        this.location = pos;
+        this.position = ErrorPosition.fromSpoonPosition(pos);
     }
 
     public String getTitle() {
@@ -41,8 +35,8 @@ public String getMessage() {
         return message;
     }
 
-    public CtElement getElement() {
-        return element;
+    public String getSnippet() {
+        return snippet;
     }
 
     public ErrorPosition getPosition() {
@@ -64,8 +58,8 @@ public String toString(String extra) {
         StringBuilder sb = new StringBuilder();
         sb.append(title);
 
-        if (element != null)
-            sb.append(" at: \n").append(element.toString().replace("@liquidjava.specification.", "@"));
+        if (snippet != null)
+            sb.append(" at: \n").append(snippet.replace("@liquidjava.specification.", "@"));
 
         sb.append("\n");
         sb.append(message).append("\n");

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

@@ -11,7 +11,7 @@
 public class NotFoundError extends LJError {
 
     public NotFoundError(CtElement element, String message, TranslationTable translationTable) {
-        super("Not Found Error", message, element, translationTable);
+        super("Not Found Error", message, element.getPosition(), element.toString(), translationTable);
     }
 
     @Override

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

@@ -18,8 +18,8 @@ public class RefinementError extends LJError {
 
     public RefinementError(CtElement element, Predicate expected, ValDerivationNode found,
             TranslationTable translationTable) {
-        super("Refinement Error", String.format("%s is not a subtype of %s", found.getValue(), expected), element,
-                translationTable);
+        super("Refinement Error", String.format("%s is not a subtype of %s", found.getValue(), expected),
+                element.getPosition(), element.toString(), translationTable);
         this.expected = expected.toString();
         this.found = found;
     }

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

@@ -15,7 +15,8 @@ public class StateConflictError extends LJError {
     private String className;
 
     public StateConflictError(CtElement element, Predicate state, String className, TranslationTable translationTable) {
-        super("State Conflict Error", "Found multiple disjoint states in state transition — State transition can only go to one state of each state set", element, translationTable);
+        super("State Conflict Error", "Found multiple disjoint states in state transition — State transition can only go to one state of each state set", element.getPosition(),
+                element.toString(), translationTable);
         this.state = state.toString();
         this.className = className;
     }

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

@@ -19,7 +19,8 @@ public class StateRefinementError extends LJError {
 
     public StateRefinementError(CtElement element, String method, Predicate[] expected, Predicate found,
             TranslationTable translationTable) {
-        super("State Refinement Error", "State refinement transition violation", element, translationTable);
+        super("State Refinement Error", "State refinement transition violation", element.getPosition(),
+                element.toString(), translationTable);
         this.method = method;
         this.expected = Arrays.stream(expected).map(Predicate::toString).toArray(String[]::new);
         this.found = found.toString();

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

@@ -16,7 +16,7 @@ public SyntaxError(String message, String refinement) {
     }
 
     public SyntaxError(String message, CtElement element, String refinement) {
-        super("Syntax Error", message, element, null);
+        super("Syntax Error", message, element.getPosition(), element.toString(), null);
         this.refinement = refinement;
     }