Add #result for Return Refinements

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

@@ -0,0 +1,16 @@
+package testSuite;
+
+import liquidjava.specification.Refinement;
+
+public class CorrectResult {
+
+    @Refinement("$result > 10")
+    public int getLargeNumber() {
+        return 15;
+    }
+
+    @Refinement("$result == (a + b)")
+    public int sum(int a, int b) {
+        return a + b;
+    }
+}

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

@@ -0,0 +1,10 @@
+// Not Found Error
+package testSuite;
+import liquidjava.specification.Refinement;
+
+public class ErrorResultVariable {
+    public void test() {
+        @Refinement("$result > 0") 
+        int x = 10; 
+    }
+}

liquidjava-verifier/src/main/antlr4/rj/grammar/RJ.g4

@@ -92,7 +92,7 @@ BOOL    : 'true' | 'false';
 ID_UPPER: ([A-Z][a-zA-Z0-9]*);
 OBJECT_TYPE:
 		  (([a-zA-Z][a-zA-Z0-9]+) ('.' [a-zA-Z][a-zA-Z0-9]*)+);
-ID     	: '#'*[a-zA-Z_][a-zA-Z0-9_#]*;
+ID     	: '#'*('$')? [a-zA-Z_] [a-zA-Z0-9_#]* ;
 STRING  : '"'(~["])*'"';
 INT     : 	(([0-9]+) |	([0-9]+('_'[0-9]+)*));
 REAL   	: (([0-9]+('.'[0-9]+)?) | '.'[0-9]+);

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

@@ -161,6 +161,7 @@ private Predicate handleFunctionRefinements(RefinedFunction f, CtElement method,
         Optional<Predicate> oret = rtc.getRefinementFromAnnotation(method);
         Predicate ret = oret.orElse(new Predicate());
         ret = ret.substituteVariable("return", Keys.WILDCARD);
+        ret = ret.substituteVariable("$result", Keys.WILDCARD);// added for refinement
         f.setRefReturn(ret);
         return Predicate.createConjunction(joint, ret);
     }
@@ -180,6 +181,13 @@ public <R> void getReturnRefinements(CtReturn<R> ret) throws LJError {
                 RefinedFunction fi = rtc.getContext().getFunction(method.getSimpleName(),
                         ((CtClass<?>) method.getParent()).getQualifiedName(), method.getParameters().size());
 
+                if (fi == null)
+                    return;// null check refinement
+
+                if (fi.getRefReturn() == null) {
+                    return;
+                }
+
                 List<Variable> lv = fi.getArguments();
                 for (Variable v : lv) {
                     rtc.getContext().addVarToContext(v);