Fix Annotation Position Lookup

liquidjava-example/src/main/java/testSuite/ErrorSyntax1.java → liquidjava-example/src/main/java/testSuite/ErrorSyntaxRefinement.java

@@ -4,7 +4,7 @@
 import liquidjava.specification.Refinement;
 
 @SuppressWarnings("unused")
-public class ErrorSyntax1 {
+public class ErrorSyntaxRefinement {
     public static void main(String[] args) {
         @Refinement("_ < 100 +")
         int value = 90 + 4;

liquidjava-example/src/main/java/testSuite/ErrorSyntaxStateRefinement.java

@@ -0,0 +1,10 @@
+// Syntax Error
+package testSuite;
+
+import liquidjava.specification.StateRefinement;
+
+public class ErrorSyntaxStateRefinement {
+
+    @StateRefinement(from="$", to="#")
+    void test() {}
+}

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

@@ -235,7 +235,7 @@ protected void handleAlias(String ref, CtElement element) throws LJError {
             }
         } catch (LJError e) {
             // add location info to error
-            SourcePosition pos = Utils.getRefinementAnnotationPosition(element, ref);
+            SourcePosition pos = Utils.getAnnotationPosition(element, ref);
             e.setPosition(pos);
             throw e;
         }

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

@@ -87,7 +87,7 @@ protected Expression parse(String ref, CtElement element) throws LJError {
             return RefinementsParser.createAST(ref, prefix);
         } catch (LJError e) {
             // add location info to error
-            SourcePosition pos = Utils.getRefinementAnnotationPosition(element, ref);
+            SourcePosition pos = Utils.getAnnotationPosition(element, ref);
             e.setPosition(pos);
             throw e;
         }

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

@@ -1,9 +1,12 @@
 package liquidjava.utils;
 
+import java.util.Map;
 import java.util.Set;
+import java.util.stream.Stream;
 
 import liquidjava.utils.constants.Types;
 import spoon.reflect.cu.SourcePosition;
+import spoon.reflect.declaration.CtAnnotation;
 import spoon.reflect.declaration.CtElement;
 import spoon.reflect.factory.Factory;
 import spoon.reflect.reference.CtTypeReference;
@@ -35,11 +38,19 @@ public static String qualifyName(String prefix, String name) {
         return String.format("%s.%s", prefix, name);
     }
 
-    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(CtElement::getPosition).orElse(element.getPosition());
+    public static SourcePosition getAnnotationPosition(CtElement element, String refinement) {
+        return element.getAnnotations().stream()
+                .filter(a -> isLiquidJavaAnnotation(a) && hasRefinementValue(a, "\"" + refinement + "\"")).findFirst()
+                .map(CtElement::getPosition).orElse(element.getPosition());
+    }
+
+    private static boolean isLiquidJavaAnnotation(CtAnnotation<?> annotation) {
+        return annotation.getAnnotationType().getQualifiedName().startsWith("liquidjava.specification");
+    }
+
+    private static boolean hasRefinementValue(CtAnnotation<?> annotation, String refinement) {
+        Map<String, ?> values = annotation.getValues();
+        return Stream.of("value", "to", "from")
+                .anyMatch(key -> refinement.equals(String.valueOf(values.get(key))));
     }
 }