Error Improvements

Author: rcosta358

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

@@ -18,6 +18,10 @@ public CustomError(String message, SourcePosition pos) {
         super("Error", message, null, pos, null);
     }
 
+    public CustomError(String message, String detail, CtElement element) {
+        super("Error", message, detail, element.getPosition(), null);
+    }
+
     public CustomError(String message, CtElement element) {
         super("Error", message, null, element.getPosition(), null);
     }

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

@@ -3,7 +3,6 @@
 import java.util.Arrays;
 
 import liquidjava.diagnostics.TranslationTable;
-import liquidjava.rj_language.Predicate;
 import liquidjava.rj_language.ast.Expression;
 import spoon.reflect.declaration.CtElement;
 

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

@@ -48,7 +48,7 @@ public <T> void visitCtInterface(CtInterface<T> intrface) {
         if (externalRefinements.isPresent()) {
             this.prefix = externalRefinements.get();
             if (!classExists(prefix)) {
-                String message = String.format("Could not find external class '%s'", prefix);
+                String message = String.format("Could not find class '%s'", prefix);
                 diagnostics.add(new ExternalClassNotFoundWarning(intrface, message, prefix));
                 return;
             }
@@ -130,7 +130,7 @@ protected void getGhostFunction(String value, CtElement element) {
             }
 
         } catch (ParsingException e) {
-            diagnostics.add(new CustomError("Could not parse the ghost function" + e.getMessage(), element));
+            diagnostics.add(new CustomError("Could not parse the ghost function", e.getMessage(), element));
         }
     }
 

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

@@ -121,8 +121,7 @@ private void createStateSet(CtNewArray<String> e, int set, CtElement element) {
                 CtLiteral<String> s = (CtLiteral<String>) ce;
                 String f = s.getValue();
                 if (Character.isUpperCase(f.charAt(0))) {
-                    diagnostics
-                            .add(new CustomError(String.format("State name must start with lowercase in '%s'", f), s));
+                    diagnostics.add(new CustomError("State names must start with lowercase", s));
                 }
             }
         }
@@ -163,12 +162,12 @@ private void createStateGhost(String string, CtAnnotation<? extends Annotation>
         try {
             gd = RefinementsParser.getGhostDeclaration(string);
         } catch (ParsingException e) {
-            diagnostics.add(new CustomError("Could not parse the ghost function " + e.getMessage(), ann));
+            diagnostics.add(new CustomError("Could not parse the ghost function", e.getMessage(), ann));
             return;
         }
         if (gd.getParam_types().size() > 0) {
-            diagnostics.add(new CustomError("Ghost States have the class as parameter "
-                    + "by default, no other parameters are allowed in '" + string + "'", ann));
+            diagnostics.add(new CustomError(
+                    "Ghost States have the class as parameter " + "by default, no other parameters are allowed", ann));
             return;
         }
         // Set class as parameter of Ghost
@@ -226,7 +225,7 @@ protected void getGhostFunction(String value, CtElement element) {
                 context.addGhostFunction(gh);
             }
         } catch (ParsingException e) {
-            diagnostics.add(new CustomError("Could not parse the ghost function " + e.getMessage(), element));
+            diagnostics.add(new CustomError("Could not parse the ghost function", e.getMessage(), element));
             // e.printStackTrace();
             return;
         }

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

@@ -236,13 +236,24 @@ private void recAuxGetVars(RefinedVariable var, List<RefinedVariable> newVars) {
         getVariablesFromContext(l, newVars, varName);
     }
 
-    public boolean smtChecks(Predicate cSMT, Predicate expectedType, SourcePosition p) {
+    public boolean smtChecks(Predicate found, Predicate expectedType, SourcePosition p) {
         try {
-            new SMTEvaluator().verifySubtype(cSMT, expectedType, context, p);
+            new SMTEvaluator().verifySubtype(found, expectedType, context, p);
         } catch (TypeCheckError e) {
             return false;
         } catch (Exception e) {
-            diagnostics.add(new CustomError(e.getMessage(), p));
+            String msg = e.getLocalizedMessage().toLowerCase();
+            LJError error;
+            if (msg.contains("wrong number of arguments")) {
+                error = new GhostInvocationError("Wrong number of arguments in ghost invocation", p,
+                        expectedType.getExpression(), null);
+            } else if (msg.contains("sort mismatch")) {
+                error = new GhostInvocationError("Type mismatch in arguments of ghost invocation", p,
+                        expectedType.getExpression(), null);
+            } else {
+                error = new CustomError(e.getMessage(), p);
+            }
+            diagnostics.add(error);
         }
         return true;
     }

liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/object_checkers/AuxStateHandler.java

@@ -390,10 +390,8 @@ public static void updateGhostField(CtFieldWrite<?> fw, TypeChecker tc) {
             stateChange.setFrom(fromPredicate);
             stateChange.setTo(toPredicate);
         } catch (ParsingException e) {
-            String message = String.format(
-                    "Parsing error while constructing assignment update for `%s` in class `%s` : %s", fw,
-                    field.getDeclaringType().getQualifiedName(), e.getMessage());
-            diagnostics.add(new CustomError(message, field));
+            String message = String.format("Parsing error while constructing assignment update for `%s`", fw);
+            diagnostics.add(new CustomError(message, e.getMessage(), field));
             return;
         }
 

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

@@ -1,13 +1,10 @@
 package liquidjava.smt;
 
-import static liquidjava.diagnostics.LJDiagnostics.diagnostics;
-
 import com.martiansoftware.jsap.SyntaxException;
 import com.microsoft.z3.Expr;
 import com.microsoft.z3.Status;
 import com.microsoft.z3.Z3Exception;
 
-import liquidjava.diagnostics.errors.GhostInvocationError;
 import liquidjava.processor.context.Context;
 import liquidjava.rj_language.Predicate;
 import liquidjava.rj_language.ast.Expression;
@@ -42,10 +39,6 @@ public void verifySubtype(Predicate subRef, Predicate supRef, Context c, SourceP
             System.out.println("Could not parse: " + toVerify);
             e1.printStackTrace();
         } catch (Z3Exception e) {
-            String msg = e.getLocalizedMessage().toLowerCase();
-            if (msg.contains("wrong number of arguments") || msg.contains("sort mismatch"))
-                diagnostics.add(new GhostInvocationError(msg, pos, supRef.getExpression(), null));
-
             throw new Z3Exception(e.getLocalizedMessage());
         }
     }