Skip to content

Commit d60aadc

Browse files
committed
Fix Exception on State Refinement Syntax Errors
1 parent 1b290cb commit d60aadc

File tree

5 files changed

+17
-9
lines changed

5 files changed

+17
-9
lines changed

liquidjava-example/src/main/java/testSuite/ErrorSyntax1.java renamed to liquidjava-example/src/main/java/testSuite/ErrorSyntaxRefinement.java

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -4,7 +4,7 @@
44
import liquidjava.specification.Refinement;
55

66
@SuppressWarnings("unused")
7-
public class ErrorSyntax1 {
7+
public class ErrorSyntaxRefinement {
88
public static void main(String[] args) {
99
@Refinement("_ < 100 +")
1010
int value = 90 + 4;
Lines changed: 10 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,10 @@
1+
// Syntax Error
2+
package testSuite;
3+
4+
import liquidjava.specification.StateRefinement;
5+
6+
public class ErrorSyntaxStateRefinement {
7+
8+
@StateRefinement(from="$", to="#")
9+
void test() {}
10+
}

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

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -235,7 +235,7 @@ protected void handleAlias(String ref, CtElement element) throws LJError {
235235
}
236236
} catch (LJError e) {
237237
// add location info to error
238-
SourcePosition pos = Utils.getRefinementAnnotationPosition(element, ref);
238+
SourcePosition pos = Utils.getAnnotationPosition(element);
239239
e.setPosition(pos);
240240
throw e;
241241
}

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

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -87,7 +87,7 @@ protected Expression parse(String ref, CtElement element) throws LJError {
8787
return RefinementsParser.createAST(ref, prefix);
8888
} catch (LJError e) {
8989
// add location info to error
90-
SourcePosition pos = Utils.getRefinementAnnotationPosition(element, ref);
90+
SourcePosition pos = Utils.getAnnotationPosition(element);
9191
e.setPosition(pos);
9292
throw e;
9393
}

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

Lines changed: 4 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -35,11 +35,9 @@ public static String qualifyName(String prefix, String name) {
3535
return String.format("%s.%s", prefix, name);
3636
}
3737

38-
public static SourcePosition getRefinementAnnotationPosition(CtElement element, String refinement) {
39-
return element.getAnnotations().stream().filter(a -> {
40-
String value = a.getValue("value").toString();
41-
String unquoted = value.substring(1, value.length() - 1);
42-
return unquoted.equals(refinement);
43-
}).findFirst().map(CtElement::getPosition).orElse(element.getPosition());
38+
public static SourcePosition getAnnotationPosition(CtElement element) {
39+
return element.getAnnotations().stream()
40+
.filter(a -> a.getAnnotationType().getQualifiedName().startsWith("liquidjava.specification"))
41+
.findFirst().map(CtElement::getPosition).orElse(element.getPosition());
4442
}
4543
}

0 commit comments

Comments
 (0)