Improve Syntax Errors

Author: rcosta358

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

@@ -94,7 +94,7 @@ public <R> void visitCtMethod(CtMethod<R> method) {
     }
 
     protected void getGhostFunction(String value, CtElement element) throws LJError {
-        GhostDTO f = RefinementsParser.getGhostDeclaration(value);
+        GhostDTO f = getGhostDeclaration(value, element);
         if (element.getParent() instanceof CtInterface<?>) {
             GhostFunction gh = new GhostFunction(f, factory, prefix);
             context.addGhostFunction(gh);

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

@@ -163,9 +163,20 @@ private void createStateSet(CtNewArray<String> e, int set, CtElement element) th
         }
     }
 
+    protected GhostDTO getGhostDeclaration(String value, CtElement element) throws LJError {
+        try {
+            return RefinementsParser.getGhostDeclaration(value);
+        } catch (LJError e) {
+            // add location info to error
+            SourcePosition annPosition = Utils.getAnnotationPosition(element, value);
+            e.setPosition(annPosition);
+            throw e;
+        }
+    }
+
     private void createStateGhost(String string, CtAnnotation<? extends Annotation> ann, CtElement element)
             throws LJError {
-        GhostDTO gd = RefinementsParser.getGhostDeclaration(string);
+        GhostDTO gd = getGhostDeclaration(string, ann);
         if (!gd.paramTypes().isEmpty()) {
             throw new CustomError(
                     "Ghost States have the class as parameter " + "by default, no other parameters are allowed",
@@ -221,7 +232,7 @@ protected Optional<GhostFunction> createStateGhost(int order, CtElement element)
     }
 
     protected void getGhostFunction(String value, CtElement element) throws LJError {
-        GhostDTO f = RefinementsParser.getGhostDeclaration(value);
+        GhostDTO f = getGhostDeclaration(value, element);
         if (element.getParent()instanceof CtClass<?> klass) {
             GhostFunction gh = new GhostFunction(f, factory, klass.getQualifiedName());
             context.addGhostFunction(gh);

liquidjava-verifier/src/main/java/liquidjava/rj_language/parsing/RefinementsParser.java

@@ -35,16 +35,12 @@ public static GhostDTO getGhostDeclaration(String s) throws LJError {
         ParseTree rc = compile(s);
         GhostDTO g = GhostVisitor.getGhostDecl(rc);
         if (g == null)
-            throw new SyntaxError("Ghost declarations should be in format <type> <name> (<parameters>)", s);
+            throw new SyntaxError("Invalid ghost declaration, e.g. \"int size\"", s);
         return g;
     }
 
     public static AliasDTO getAliasDeclaration(String s) throws LJError {
-        Optional<String> os = getErrors(s);
-        if (os.isPresent())
-            throw new SyntaxError(os.get(), s);
-        CodePointCharStream input;
-        input = CharStreams.fromString(s);
+        CodePointCharStream input = CharStreams.fromString(s);
         RJErrorListener err = new RJErrorListener();
         RJLexer lexer = new RJLexer(input);
         lexer.removeErrorListeners();
@@ -60,14 +56,14 @@ public static AliasDTO getAliasDeclaration(String s) throws LJError {
         AliasVisitor av = new AliasVisitor(input);
         AliasDTO alias = av.getAlias(rc);
         if (alias == null)
-            throw new SyntaxError("Alias definitions should be in format <name>(<parameters>) { <definition> }", s);
+            throw new SyntaxError("Invalid alias definition, e.g. \"Positive(int v) { v >= 0 }\"", s);
         return alias;
     }
 
     private static ParseTree compile(String toParse) throws LJError {
         Optional<String> s = getErrors(toParse);
         if (s.isPresent())
-            throw new SyntaxError(s.get(), toParse);
+            throw new SyntaxError("Invalid refinement expression, e.g. \"v > 0\"", toParse);
 
         CodePointCharStream input = CharStreams.fromString(toParse);
         RJErrorListener err = new RJErrorListener();