From d60aadcecc15910739f54f216c39aeccc3de1f6a Mon Sep 17 00:00:00 2001 From: Ricardo Costa Date: Fri, 6 Feb 2026 15:49:39 +0000 Subject: [PATCH 1/2] Fix Exception on State Refinement Syntax Errors --- .../{ErrorSyntax1.java => ErrorSyntaxRefinement.java} | 2 +- .../java/testSuite/ErrorSyntaxStateRefinement.java | 10 ++++++++++ .../processor/refinement_checker/TypeChecker.java | 2 +- .../main/java/liquidjava/rj_language/Predicate.java | 2 +- .../src/main/java/liquidjava/utils/Utils.java | 10 ++++------ 5 files changed, 17 insertions(+), 9 deletions(-) rename liquidjava-example/src/main/java/testSuite/{ErrorSyntax1.java => ErrorSyntaxRefinement.java} (85%) create mode 100644 liquidjava-example/src/main/java/testSuite/ErrorSyntaxStateRefinement.java 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..947f339c 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); 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..66c5e10d 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); 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..ae8ffd0b 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/utils/Utils.java +++ b/liquidjava-verifier/src/main/java/liquidjava/utils/Utils.java @@ -35,11 +35,9 @@ 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) { + return element.getAnnotations().stream() + .filter(a -> a.getAnnotationType().getQualifiedName().startsWith("liquidjava.specification")) + .findFirst().map(CtElement::getPosition).orElse(element.getPosition()); } } From b2254c832c70deda2180f075f9cf406d16dcf575 Mon Sep 17 00:00:00 2001 From: Ricardo Costa Date: Fri, 6 Feb 2026 16:01:22 +0000 Subject: [PATCH 2/2] Find Annotation by Value --- .../refinement_checker/TypeChecker.java | 2 +- .../liquidjava/rj_language/Predicate.java | 2 +- .../src/main/java/liquidjava/utils/Utils.java | 19 ++++++++++++++++--- 3 files changed, 18 insertions(+), 5 deletions(-) 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 947f339c..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.getAnnotationPosition(element); + 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 66c5e10d..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.getAnnotationPosition(element); + 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 ae8ffd0b..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,9 +38,19 @@ public static String qualifyName(String prefix, String name) { return String.format("%s.%s", prefix, name); } - public static SourcePosition getAnnotationPosition(CtElement element) { + public static SourcePosition getAnnotationPosition(CtElement element, String refinement) { return element.getAnnotations().stream() - .filter(a -> a.getAnnotationType().getQualifiedName().startsWith("liquidjava.specification")) - .findFirst().map(CtElement::getPosition).orElse(element.getPosition()); + .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)))); } }