Fix NullPointerException in MethodsFunctionsChecker

liquidjava-example/src/main/java/testSuite/ErrorInvalidRefinement.java

@@ -0,0 +1,13 @@
+// Invalid Refinement Error
+package testSuite;
+
+import liquidjava.specification.Refinement;
+
+@SuppressWarnings("unused")
+public class ErrorInvalidRefinement {
+
+    void test() {
+        @Refinement("x")
+        int x = 0;
+    }
+}

liquidjava-example/src/main/java/testSuite/ErrorInvalidRefinementParameter.java

@@ -0,0 +1,13 @@
+// Invalid Refinement Error
+package testSuite;
+
+import liquidjava.specification.Refinement;
+
+public class ErrorInvalidRefinementParameter {
+
+    void testInvalidRefinement(@Refinement("y + 1") int y) {}
+
+    int otherMethod() {
+        return -1;
+    }
+}

liquidjava-example/src/main/java/testSuite/ErrorInvalidRefinementReturn.java

@@ -0,0 +1,11 @@
+// Invalid Refinement Error
+package testSuite;
+
+import liquidjava.specification.Refinement;
+
+public class ErrorInvalidRefinementReturn {
+
+    @Refinement("_ * 2")
+    void test() {
+    }
+}

liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/InvalidRefinementError.java

@@ -12,7 +12,7 @@ public class InvalidRefinementError extends LJError {
     private final String refinement;
 
     public InvalidRefinementError(SourcePosition position, String message, String refinement) {
-        super("Invalid Refinement", message, position, null);
+        super("Invalid Refinement Error", message, position, null);
         this.refinement = refinement;
     }
 

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

@@ -96,16 +96,24 @@ public <T> void visitCtInterface(CtInterface<T> intrface) {
     @Override
     public <T> void visitCtConstructor(CtConstructor<T> c) {
         context.enterContext();
-        getRefinementFromAnnotation(c);
-        mfc.getConstructorRefinements(c);
-        super.visitCtConstructor(c);
+        try {
+            getRefinementFromAnnotation(c);
+            mfc.getConstructorRefinements(c);
+            super.visitCtConstructor(c);
+        } catch (LJError e) {
+            diagnostics.add(e);
+        }
         context.exitContext();
     }
 
     public <R> void visitCtMethod(CtMethod<R> method) {
         context.enterContext();
-        mfc.getMethodRefinements(method);
-        super.visitCtMethod(method);
+        try {
+            mfc.getMethodRefinements(method);
+            super.visitCtMethod(method);
+        } catch (LJError e) {
+            diagnostics.add(e);
+        }
         context.exitContext();
     }
 }

liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/general_checkers/MethodsFunctionsChecker.java

@@ -181,6 +181,8 @@ public <R> void getReturnRefinements(CtReturn<R> ret) throws LJError {
             if (method.getParent() instanceof CtClass) {
                 RefinedFunction fi = rtc.getContext().getFunction(method.getSimpleName(),
                         ((CtClass<?>) method.getParent()).getQualifiedName(), method.getParameters().size());
+                if (fi == null)
+                    return;
 
                 List<Variable> lv = fi.getArguments();
                 for (Variable v : lv) {
@@ -411,10 +413,6 @@ public void loadFunctionInfo(CtExecutable<?> method) {
                 List<Variable> lv = fi.getArguments();
                 for (Variable v : lv)
                     rtc.getContext().addVarToContext(v);
-            } else {
-                assert false;
-                // Method should already be in context. Should not arrive this point in
-                // refinement checker.
             }
         }
     }