Handle Alias Syntax Errors

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 {}

liquidjava-verifier/src/main/java/liquidjava/processor/facade/AliasDTO.java

@@ -22,7 +22,7 @@ public AliasDTO(String name, List<CtTypeReference<?>> varTypes, List<String> var
         this.expression = expression;
     }
 
-    public AliasDTO(String name2, List<String> varTypes2, List<String> varNames2, String ref) throws ParsingException {
+    public AliasDTO(String name2, List<String> varTypes2, List<String> varNames2, String ref) {
         super();
         this.name = name2;
         this.varTypes = varTypes2;

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();
         }

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 <type> <name> (<parameters>)");
+            throw new ParsingException("Ghost declarations should be in format <type> <name> (<parameters>)");
         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 <name>(<parameters>) { <definition> }");
+        return alias;
     }
 
     private static ParseTree compile(String toParse) throws ParsingException {

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();