Use Annotation Position in Invalid Refinement Errors

Author: rcosta358

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

@@ -81,7 +81,8 @@ public Optional<Predicate> getRefinementFromAnnotation(CtElement element) throws
         if (ref.isPresent()) {
             Predicate p = new Predicate(ref.get(), element);
             if (!p.getExpression().isBooleanExpression()) {
-                throw new InvalidRefinementError(element.getPosition(),
+                SourcePosition position = Utils.getAnnotationPosition(element, ref.get());
+                throw new InvalidRefinementError(position,
                         "Refinement predicate must be a boolean expression", ref.get());
             }
             constr = Optional.of(p);
@@ -250,7 +251,7 @@ protected void handleAlias(String ref, CtElement element, SourcePosition positio
             if (klass != null && path != null) {
                 a.parse(path);
                 if (a.getExpression() != null && !a.getExpression().isBooleanExpression()) {
-                    throw new InvalidRefinementError(element.getPosition(),
+                    throw new InvalidRefinementError(position,
                             "Refinement alias must return a boolean expression", ref);
                 }
                 AliasWrapper aw = new AliasWrapper(a, factory, klass, path);

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

@@ -16,6 +16,7 @@
 import liquidjava.utils.constants.Keys;
 import liquidjava.utils.constants.Types;
 import spoon.reflect.code.*;
+import spoon.reflect.cu.SourcePosition;
 import spoon.reflect.declaration.*;
 import spoon.reflect.reference.CtTypeReference;
 
@@ -69,7 +70,7 @@ private static void setConstructorStates(RefinedFunction f, List<CtAnnotation<?
             if (to != null) {
                 Predicate p = new Predicate(to, element);
                 if (!p.getExpression().isBooleanExpression()) {
-                    throw new InvalidRefinementError(element.getPosition(),
+                    throw new InvalidRefinementError(an.getPosition(),
                             "State refinement transition must be a boolean expression", to);
                 }
                 state.setTo(p);
@@ -208,7 +209,8 @@ private static Predicate createStatePredicate(String value, String targetClass,
             boolean isTo, String prefix) throws LJError {
         Predicate p = new Predicate(value, e, prefix);
         if (!p.getExpression().isBooleanExpression()) {
-            throw new InvalidRefinementError(e.getPosition(),
+            SourcePosition position = Utils.getAnnotationPosition(e, value);
+            throw new InvalidRefinementError(position,
                     "State refinement transition must be a boolean expression", value);
         }
         CtTypeReference<?> r = tc.getFactory().Type().createReference(targetClass);