Use Annotation Position in Syntax Errors

Author: rcosta358

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

@@ -1,6 +1,6 @@
 package liquidjava.diagnostics.errors;
 
-import spoon.reflect.declaration.CtElement;
+import spoon.reflect.cu.SourcePosition;
 
 /**
  * Error indicating that the syntax of a refinement is invalid
@@ -11,12 +11,13 @@ public class SyntaxError extends LJError {
 
     private String refinement;
 
+
     public SyntaxError(String message, String refinement) {
         this(message, null, refinement);
     }
 
-    public SyntaxError(String message, CtElement element, String refinement) {
-        super("Syntax Error", message, "", element.getPosition(), null);
+    public SyntaxError(String message, SourcePosition pos, String refinement) {
+        super("Syntax Error", message, "", pos, null);
         this.refinement = refinement;
     }
 

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

@@ -20,6 +20,7 @@
 import liquidjava.rj_language.Predicate;
 import liquidjava.rj_language.parsing.ParsingException;
 import liquidjava.rj_language.parsing.RefinementsParser;
+import liquidjava.utils.Utils;
 import liquidjava.utils.constants.Formats;
 import liquidjava.utils.constants.Keys;
 import liquidjava.utils.constants.Types;
@@ -254,7 +255,8 @@ protected void handleAlias(String value, CtElement element) {
                 context.addAlias(aw);
             }
         } catch (ParsingException e) {
-            diagnostics.add(new SyntaxError(e.getMessage(), element, value));
+            SourcePosition pos = Utils.getRefinementAnnotationPosition(element, value);
+            diagnostics.add(new SyntaxError(e.getMessage(), pos, value));
         }
     }
 

liquidjava-verifier/src/main/java/liquidjava/rj_language/Predicate.java

@@ -31,6 +31,7 @@
 import liquidjava.utils.constants.Keys;
 import liquidjava.utils.constants.Ops;
 import liquidjava.utils.constants.Types;
+import spoon.reflect.cu.SourcePosition;
 import spoon.reflect.declaration.CtElement;
 import spoon.reflect.declaration.CtType;
 import spoon.reflect.factory.Factory;
@@ -90,7 +91,8 @@ protected Expression parse(String ref, CtElement element) throws ParsingExceptio
         try {
             return RefinementsParser.createAST(ref, prefix);
         } catch (ParsingException e) {
-            diagnostics.add(new SyntaxError(e.getMessage(), element, ref));
+            SourcePosition pos = Utils.getRefinementAnnotationPosition(element, ref);
+            diagnostics.add(new SyntaxError(e.getMessage(), pos, ref));
             throw e;
         }
     }

liquidjava-verifier/src/main/java/liquidjava/utils/Utils.java

@@ -3,6 +3,8 @@
 import java.util.Set;
 
 import liquidjava.utils.constants.Types;
+import spoon.reflect.cu.SourcePosition;
+import spoon.reflect.declaration.CtElement;
 import spoon.reflect.factory.Factory;
 import spoon.reflect.reference.CtTypeReference;
 
@@ -36,4 +38,15 @@ public static String qualifyName(String prefix, String name) {
     public static String stripParens(String s) {
         return s.startsWith("(") && s.endsWith(")") ? s.substring(1, s.length() - 1) : s;
     }
+
+    public static SourcePosition getRefinementAnnotationPosition(CtElement element, String refinement) {
+          return element.getAnnotations().stream()
+                .filter(a -> {
+                    String value = a.getValue("value").toString();
+                    String unquoted = value.substring(1, value.length() - 1);
+                    return unquoted.equals(refinement);
+                }).findFirst()
+                .map(a -> a.getPosition())
+                .orElse(element.getPosition());
+    }
 }