Refactor SMT Errors

Author: rcosta358

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

@@ -11,7 +11,6 @@ public class SyntaxError extends LJError {
 
     private String refinement;
 
-
     public SyntaxError(String message, String refinement) {
         this(message, null, refinement);
     }

liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/VCChecker.java

@@ -22,10 +22,8 @@
 import liquidjava.processor.context.*;
 import liquidjava.rj_language.Predicate;
 import liquidjava.rj_language.ast.Expression;
-import liquidjava.smt.GhostFunctionError;
-import liquidjava.smt.NotFoundSMTError;
 import liquidjava.smt.SMTEvaluator;
-import liquidjava.smt.TypeCheckError;
+import liquidjava.smt.errors.TypeCheckError;
 import liquidjava.utils.constants.Keys;
 import spoon.reflect.cu.SourcePosition;
 import spoon.reflect.declaration.CtElement;
@@ -267,10 +265,10 @@ public boolean smtChecks(Predicate found, Predicate expectedType, SourcePosition
      *
      * @throws Exception
      * @throws GhostFunctionError
-     * @throws TypeCheckError
+     * @throws SMTError
      */
     private void smtChecking(Predicate cSMT, Predicate expectedType, SourcePosition p)
-            throws TypeCheckError, GhostFunctionError, Exception {
+            throws TypeCheckError, Exception {
         new SMTEvaluator().verifySubtype(cSMT, expectedType, context, p);
     }
 
@@ -335,10 +333,7 @@ private LJError mapError(Exception e, Predicate premisesBeforeChange, Predicate
             TranslationTable map) {
         if (e instanceof TypeCheckError) {
             return new RefinementError(element, expectedType.getExpression(), premisesBeforeChange.simplify(), map);
-        } else if (e instanceof GhostFunctionError) {
-            return new GhostInvocationError("Invalid types or number of arguments in ghost invocation",
-                    element.getPosition(), expectedType.getExpression(), map);
-        } else if (e instanceof NotFoundSMTError) {
+        } else if (e instanceof liquidjava.smt.errors.NotFoundError) {
             return new NotFoundError(element, e.getMessage(), map);
         } else {
             return new CustomError(e.getMessage(), element);

liquidjava-verifier/src/main/java/liquidjava/rj_language/parsing/ParsingException.java

@@ -2,9 +2,6 @@
 
 public class ParsingException extends Exception {
 
-    /** */
-    private static final long serialVersionUID = 1L;
-
     public ParsingException(String errorMessage) {
         super(errorMessage);
     }

liquidjava-verifier/src/main/java/liquidjava/smt/GhostFunctionError.java

@@ -8,12 +8,13 @@
 import liquidjava.processor.context.Context;
 import liquidjava.rj_language.Predicate;
 import liquidjava.rj_language.ast.Expression;
+import liquidjava.smt.errors.TypeCheckError;
 import spoon.reflect.cu.SourcePosition;
 
 public class SMTEvaluator {
 
     public void verifySubtype(Predicate subRef, Predicate supRef, Context c, SourcePosition pos)
-            throws TypeCheckError, GhostFunctionError, Exception {
+            throws TypeCheckError, Exception {
         // Creates a parser for our SMT-ready refinement language
         // Discharges the verification to z3
 

liquidjava-verifier/src/main/java/liquidjava/smt/NotFoundSMTError.java

@@ -17,6 +17,7 @@
 import java.util.List;
 import java.util.Map;
 import liquidjava.processor.context.AliasWrapper;
+import liquidjava.smt.errors.NotFoundError;
 import liquidjava.utils.Utils;
 
 import org.apache.commons.lang3.NotImplementedException;
@@ -75,7 +76,7 @@ public Expr<?> makeBooleanLiteral(boolean value) {
 
     private Expr<?> getVariableTranslation(String name) throws Exception {
         if (!varTranslation.containsKey(name))
-            throw new NotFoundSMTError("Variable '" + name.toString() + "' not found");
+            throw new NotFoundError("Variable '" + name.toString() + "' not found");
         Expr<?> e = varTranslation.get(name);
         if (e == null)
             e = varTranslation.get(String.format("this#%s", name));
@@ -144,7 +145,7 @@ private FuncDecl<?> resolveFunctionDeclFallback(String name, Expr<?>[] params) t
         if (candidate != null) {
             return candidate;
         }
-        throw new NotFoundSMTError("Function '" + name + "' not found");
+        throw new NotFoundError("Function '" + name + "' not found");
     }
 
     @SuppressWarnings({ "unchecked", "rawtypes" })

liquidjava-verifier/src/main/java/liquidjava/smt/SMTEvaluator.java

@@ -0,0 +1,8 @@
+package liquidjava.smt.errors;
+
+public class NotFoundError extends SMTError {
+
+    public NotFoundError(String message) {
+        super(message);
+    }
+}

liquidjava-verifier/src/main/java/liquidjava/smt/TranslatorToZ3.java

@@ -1,12 +1,11 @@
-package liquidjava.smt;
+package liquidjava.smt.errors;
 
 import spoon.reflect.declaration.CtElement;
 
-public class TypeCheckError extends Exception {
-
+public class SMTError extends Exception {
     private CtElement location;
 
-    public TypeCheckError(String message) {
+    public SMTError(String message) {
         super(message);
     }
 
@@ -17,7 +16,4 @@ public CtElement getLocation() {
     public void setLocation(CtElement location) {
         this.location = location;
     }
-
-    /** */
-    private static final long serialVersionUID = 1L;
 }

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

@@ -0,0 +1,8 @@
+package liquidjava.smt.errors;
+
+public class TypeCheckError extends Exception {
+
+    public TypeCheckError(String message) {
+        super(message);
+    }
+}