diff --git a/liquidjava-example/src/main/java/testSuite/ErrorSyntax1.java b/liquidjava-example/src/main/java/testSuite/ErrorSyntaxRefinement.java similarity index 85% rename from liquidjava-example/src/main/java/testSuite/ErrorSyntax1.java rename to liquidjava-example/src/main/java/testSuite/ErrorSyntaxRefinement.java index 6d28e95c..b02c63d0 100644 --- a/liquidjava-example/src/main/java/testSuite/ErrorSyntax1.java +++ b/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; diff --git a/liquidjava-example/src/main/java/testSuite/ErrorSyntaxStateRefinement.java b/liquidjava-example/src/main/java/testSuite/ErrorSyntaxStateRefinement.java new file mode 100644 index 00000000..14fd6a2b --- /dev/null +++ b/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() {} +} diff --git a/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/TypeChecker.java b/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/TypeChecker.java index e154a3dc..c38c3f9a 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/TypeChecker.java +++ b/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; } diff --git a/liquidjava-verifier/src/main/java/liquidjava/rj_language/Predicate.java b/liquidjava-verifier/src/main/java/liquidjava/rj_language/Predicate.java index 565de7e3..eecfaa10 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/rj_language/Predicate.java +++ b/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; } diff --git a/liquidjava-verifier/src/main/java/liquidjava/utils/Utils.java b/liquidjava-verifier/src/main/java/liquidjava/utils/Utils.java index 7d690d1c..1cf45bc7 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/utils/Utils.java +++ b/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 values = annotation.getValues(); + return Stream.of("value", "to", "from") + .anyMatch(key -> refinement.equals(String.valueOf(values.get(key)))); } }