diff --git a/liquidjava-example/src/main/java/testSuite/ErrorMissingAliasTypeParameter.java b/liquidjava-example/src/main/java/testSuite/ErrorMissingAliasTypeParameter.java new file mode 100644 index 00000000..52c2c758 --- /dev/null +++ b/liquidjava-example/src/main/java/testSuite/ErrorMissingAliasTypeParameter.java @@ -0,0 +1,6 @@ +package testSuite; + +import liquidjava.specification.RefinementAlias; + +@RefinementAlias("Positive(v) { v > 0 }") +public class ErrorMissingAliasTypeParameter {} diff --git a/liquidjava-verifier/src/main/java/liquidjava/processor/facade/AliasDTO.java b/liquidjava-verifier/src/main/java/liquidjava/processor/facade/AliasDTO.java index 9bb59f18..8737f572 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/processor/facade/AliasDTO.java +++ b/liquidjava-verifier/src/main/java/liquidjava/processor/facade/AliasDTO.java @@ -22,7 +22,7 @@ public AliasDTO(String name, List> varTypes, List var this.expression = expression; } - public AliasDTO(String name2, List varTypes2, List varNames2, String ref) throws ParsingException { + public AliasDTO(String name2, List varTypes2, List varNames2, String ref) { super(); this.name = name2; this.varTypes = varTypes2; 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 6be78523..426e8723 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 @@ -233,25 +233,22 @@ protected void getGhostFunction(String value, CtElement element) { protected void handleAlias(String value, CtElement element) { try { AliasDTO a = RefinementsParser.getAliasDeclaration(value); - - if (a != null) { - String klass = null; - String path = null; - if (element instanceof CtClass) { - klass = ((CtClass) element).getSimpleName(); - path = ((CtClass) element).getQualifiedName(); - } else if (element instanceof CtInterface) { - klass = ((CtInterface) element).getSimpleName(); - path = ((CtInterface) element).getQualifiedName(); - } - if (klass != null && path != null) { - a.parse(path); - AliasWrapper aw = new AliasWrapper(a, factory, WILD_VAR, context, klass, path); - context.addAlias(aw); - } + String klass = null; + String path = null; + if (element instanceof CtClass) { + klass = ((CtClass) element).getSimpleName(); + path = ((CtClass) element).getQualifiedName(); + } else if (element instanceof CtInterface) { + klass = ((CtInterface) element).getSimpleName(); + path = ((CtInterface) element).getQualifiedName(); + } + if (klass != null && path != null) { + a.parse(path); + AliasWrapper aw = new AliasWrapper(a, factory, WILD_VAR, context, klass, path); + context.addAlias(aw); } } catch (ParsingException e) { - ErrorHandler.printCustomError(element, e.getMessage(), errorEmitter); + ErrorHandler.printSyntaxError(e.getMessage(), value, element, errorEmitter); return; // e.printStackTrace(); } diff --git a/liquidjava-verifier/src/main/java/liquidjava/rj_language/parsing/RefinementsParser.java b/liquidjava-verifier/src/main/java/liquidjava/rj_language/parsing/RefinementsParser.java index ed049551..572d5e71 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/rj_language/parsing/RefinementsParser.java +++ b/liquidjava-verifier/src/main/java/liquidjava/rj_language/parsing/RefinementsParser.java @@ -36,7 +36,7 @@ public static GhostDTO getGhostDeclaration(String s) throws ParsingException { ParseTree rc = compile(s); GhostDTO g = GhostVisitor.getGhostDecl(rc); if (g == null) - throw new ParsingException(" The ghost should be in format ()"); + throw new ParsingException("Ghost declarations should be in format ()"); return g; } @@ -59,7 +59,10 @@ public static AliasDTO getAliasDeclaration(String s) throws ParsingException { RuleContext rc = parser.prog(); AliasVisitor av = new AliasVisitor(input); - return av.getAlias(rc); + AliasDTO alias = av.getAlias(rc); + if (alias == null) + throw new ParsingException("Alias definitions should be in format () { }"); + return alias; } private static ParseTree compile(String toParse) throws ParsingException { diff --git a/liquidjava-verifier/src/main/java/liquidjava/rj_language/visitors/AliasVisitor.java b/liquidjava-verifier/src/main/java/liquidjava/rj_language/visitors/AliasVisitor.java index f0937af2..de155282 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/rj_language/visitors/AliasVisitor.java +++ b/liquidjava-verifier/src/main/java/liquidjava/rj_language/visitors/AliasVisitor.java @@ -31,7 +31,7 @@ public AliasVisitor(CodePointCharStream input) { * * @throws ParsingException */ - public AliasDTO getAlias(ParseTree rc) throws ParsingException { + public AliasDTO getAlias(ParseTree rc) { if (rc instanceof AliasContext) { AliasContext ac = (AliasContext) rc; String name = ac.ID_UPPER().getText();