Use Annotation Position Directly for Syntax Errors

Author: rcosta358

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

@@ -15,6 +15,7 @@
 import liquidjava.rj_language.parsing.RefinementsParser;
 import liquidjava.utils.Utils;
 import spoon.reflect.code.CtLiteral;
+import spoon.reflect.cu.SourcePosition;
 import spoon.reflect.declaration.CtAnnotation;
 import spoon.reflect.declaration.CtClass;
 import spoon.reflect.declaration.CtElement;
@@ -93,8 +94,8 @@ public <R> void visitCtMethod(CtMethod<R> method) {
         super.visitCtMethod(method);
     }
 
-    protected void getGhostFunction(String value, CtElement element) throws LJError {
-        GhostDTO f = getGhostDeclaration(value, element);
+    protected void getGhostFunction(String value, CtElement element, SourcePosition position) throws LJError {
+        GhostDTO f = getGhostDeclaration(value, position);
         if (element.getParent() instanceof CtInterface<?>) {
             GhostFunction gh = new GhostFunction(f, factory, prefix);
             context.addGhostFunction(gh);

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

@@ -66,22 +66,20 @@ public Optional<Predicate> getRefinementFromAnnotation(CtElement element) throws
         for (CtAnnotation<? extends Annotation> ann : element.getAnnotations()) {
             String an = ann.getActualAnnotation().annotationType().getCanonicalName();
             if (an.contentEquals("liquidjava.specification.Refinement")) {
-                String st = getStringFromAnnotation(ann.getValue("value"));
-                ref = Optional.of(st);
+                String value = getStringFromAnnotation(ann.getValue("value"));
+                ref = Optional.of(value);
 
             } else if (an.contentEquals("liquidjava.specification.RefinementPredicate")) {
-                String st = getStringFromAnnotation(ann.getValue("value"));
-                getGhostFunction(st, element);
+                String value = getStringFromAnnotation(ann.getValue("value"));
+                getGhostFunction(value, element, ann.getPosition());
 
             } else if (an.contentEquals("liquidjava.specification.RefinementAlias")) {
-                String st = getStringFromAnnotation(ann.getValue("value"));
-                handleAlias(st, element);
+                String value = getStringFromAnnotation(ann.getValue("value"));
+                handleAlias(value, element, ann.getPosition());
             }
         }
         if (ref.isPresent()) {
             Predicate p = new Predicate(ref.get(), element);
-
-            // check if refinement is valid
             if (!p.getExpression().isBooleanExpression()) {
                 throw new InvalidRefinementError(element.getPosition(),
                         "Refinement predicate must be a boolean expression", ref.get());
@@ -117,7 +115,7 @@ public void handleStateSetsFromAnnotation(CtElement element) throws LJError {
             }
             if (an.contentEquals("liquidjava.specification.Ghost")) {
                 CtLiteral<String> s = (CtLiteral<String>) ann.getAllValues().get("value");
-                createStateGhost(s.getValue(), ann, element);
+                createStateGhost(s.getValue(), element, ann.getPosition());
             }
         }
     }
@@ -163,24 +161,22 @@ private void createStateSet(CtNewArray<String> e, int set, CtElement element) th
         }
     }
 
-    protected GhostDTO getGhostDeclaration(String value, CtElement element) throws LJError {
+    protected GhostDTO getGhostDeclaration(String value, SourcePosition position) throws LJError {
         try {
             return RefinementsParser.getGhostDeclaration(value);
         } catch (LJError e) {
             // add location info to error
-            SourcePosition annPosition = Utils.getAnnotationPosition(element, value);
-            e.setPosition(annPosition);
+            e.setPosition(position);
             throw e;
         }
     }
 
-    private void createStateGhost(String string, CtAnnotation<? extends Annotation> ann, CtElement element)
-            throws LJError {
-        GhostDTO gd = getGhostDeclaration(string, ann);
+    private void createStateGhost(String string, CtElement element, SourcePosition position) throws LJError {
+        GhostDTO gd = getGhostDeclaration(string, position);
         if (!gd.paramTypes().isEmpty()) {
             throw new CustomError(
                     "Ghost States have the class as parameter " + "by default, no other parameters are allowed",
-                    ann.getPosition());
+                    position);
         }
         // Set class as parameter of Ghost
         String qn = getQualifiedClassName(element);
@@ -231,15 +227,15 @@ protected Optional<GhostFunction> createStateGhost(int order, CtElement element)
         return Optional.empty();
     }
 
-    protected void getGhostFunction(String value, CtElement element) throws LJError {
-        GhostDTO f = getGhostDeclaration(value, element);
+    protected void getGhostFunction(String value, CtElement element, SourcePosition position) throws LJError {
+        GhostDTO f = getGhostDeclaration(value, position);
         if (element.getParent()instanceof CtClass<?> klass) {
             GhostFunction gh = new GhostFunction(f, factory, klass.getQualifiedName());
             context.addGhostFunction(gh);
         }
     }
 
-    protected void handleAlias(String ref, CtElement element) throws LJError {
+    protected void handleAlias(String ref, CtElement element, SourcePosition position) throws LJError {
         try {
             AliasDTO a = RefinementsParser.getAliasDeclaration(ref);
             String klass = null;
@@ -253,7 +249,6 @@ protected void handleAlias(String ref, CtElement element) throws LJError {
             }
             if (klass != null && path != null) {
                 a.parse(path);
-                // refinement alias must return a boolean expression
                 if (a.getExpression() != null && !a.getExpression().isBooleanExpression()) {
                     throw new InvalidRefinementError(element.getPosition(),
                             "Refinement alias must return a boolean expression", ref);
@@ -263,8 +258,7 @@ protected void handleAlias(String ref, CtElement element) throws LJError {
             }
         } catch (LJError e) {
             // add location info to error
-            SourcePosition pos = Utils.getAnnotationPosition(element, ref);
-            e.setPosition(pos);
+            e.setPosition(position);
             throw e;
         }
     }