Add Tests

Author: rcosta358

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/general_checkers/MethodsFunctionsChecker.java

@@ -413,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.
             }
         }
     }