From 9d7e2dc138c9f335b5f9adfd7dd7179b2a392455 Mon Sep 17 00:00:00 2001 From: RajShivu Date: Tue, 10 Feb 2026 22:44:24 +0530 Subject: [PATCH 1/4] feat: implement support and restore test infrastructure --- .../src/main/java/testSuite/CorrectResult.java | 16 ++++++++++++++++ .../main/java/testSuite/ErrorResultVariable.java | 10 ++++++++++ 2 files changed, 26 insertions(+) create mode 100644 liquidjava-example/src/main/java/testSuite/CorrectResult.java create mode 100644 liquidjava-example/src/main/java/testSuite/ErrorResultVariable.java diff --git a/liquidjava-example/src/main/java/testSuite/CorrectResult.java b/liquidjava-example/src/main/java/testSuite/CorrectResult.java new file mode 100644 index 00000000..db67c70c --- /dev/null +++ b/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; + } +} \ No newline at end of file diff --git a/liquidjava-example/src/main/java/testSuite/ErrorResultVariable.java b/liquidjava-example/src/main/java/testSuite/ErrorResultVariable.java new file mode 100644 index 00000000..c37cade8 --- /dev/null +++ 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; + } +} \ No newline at end of file From e111574005e77d2ac889a11baa4e9085cdcee66b Mon Sep 17 00:00:00 2001 From: RajShivu Date: Tue, 10 Feb 2026 22:54:08 +0530 Subject: [PATCH 2/4] TestMultiple: restored original --- .../src/test/java/liquidjava/api/tests/TestMultiple.java | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/liquidjava-verifier/src/test/java/liquidjava/api/tests/TestMultiple.java b/liquidjava-verifier/src/test/java/liquidjava/api/tests/TestMultiple.java index 6e28cc67..e833d7ba 100644 --- a/liquidjava-verifier/src/test/java/liquidjava/api/tests/TestMultiple.java +++ b/liquidjava-verifier/src/test/java/liquidjava/api/tests/TestMultiple.java @@ -14,7 +14,7 @@ public void testMultipleErrorDirectory() { String path = "../liquidjava-example/src/main/java/testMultiple/errors"; CommandLineLauncher.launch(path); Diagnostics diagnostics = Diagnostics.getInstance(); - assertEquals(9, diagnostics.getErrors().size()); + assertEquals(9, diagnostics.getErrors().size());// 9 } @Test @@ -39,7 +39,7 @@ public void testMultipleDirectory() { CommandLineLauncher.launch(path); Diagnostics diagnostics = Diagnostics.getInstance(); - assertEquals(11, diagnostics.getErrors().size()); + assertEquals(11, diagnostics.getErrors().size());// 11 assertEquals(3, diagnostics.getWarnings().size()); } } \ No newline at end of file From ab4d6002495f85309cc2dcce372e33eacc651886 Mon Sep 17 00:00:00 2001 From: RajShivu Date: Wed, 11 Feb 2026 08:35:48 +0530 Subject: [PATCH 3/4] Assert: checked assert validation tests --- .../general_checkers/MethodsFunctionsChecker.java | 8 ++++++++ .../src/test/java/liquidjava/api/tests/TestMultiple.java | 4 ++-- 2 files changed, 10 insertions(+), 2 deletions(-) diff --git a/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/general_checkers/MethodsFunctionsChecker.java b/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/general_checkers/MethodsFunctionsChecker.java index 815e8e6c..6b5115a7 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/general_checkers/MethodsFunctionsChecker.java +++ b/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 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 void getReturnRefinements(CtReturn 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 lv = fi.getArguments(); for (Variable v : lv) { rtc.getContext().addVarToContext(v); diff --git a/liquidjava-verifier/src/test/java/liquidjava/api/tests/TestMultiple.java b/liquidjava-verifier/src/test/java/liquidjava/api/tests/TestMultiple.java index e833d7ba..6e28cc67 100644 --- a/liquidjava-verifier/src/test/java/liquidjava/api/tests/TestMultiple.java +++ b/liquidjava-verifier/src/test/java/liquidjava/api/tests/TestMultiple.java @@ -14,7 +14,7 @@ public void testMultipleErrorDirectory() { String path = "../liquidjava-example/src/main/java/testMultiple/errors"; CommandLineLauncher.launch(path); Diagnostics diagnostics = Diagnostics.getInstance(); - assertEquals(9, diagnostics.getErrors().size());// 9 + assertEquals(9, diagnostics.getErrors().size()); } @Test @@ -39,7 +39,7 @@ public void testMultipleDirectory() { CommandLineLauncher.launch(path); Diagnostics diagnostics = Diagnostics.getInstance(); - assertEquals(11, diagnostics.getErrors().size());// 11 + assertEquals(11, diagnostics.getErrors().size()); assertEquals(3, diagnostics.getWarnings().size()); } } \ No newline at end of file From 58a547577f3bc7eff8b11f7883ccf86537747743 Mon Sep 17 00:00:00 2001 From: RajShivu Date: Wed, 11 Feb 2026 21:32:48 +0530 Subject: [PATCH 4/4] Fix refinement handling in rj grammar --- liquidjava-verifier/src/main/antlr4/rj/grammar/RJ.g4 | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/liquidjava-verifier/src/main/antlr4/rj/grammar/RJ.g4 b/liquidjava-verifier/src/main/antlr4/rj/grammar/RJ.g4 index e34f40ad..07615f62 100644 --- a/liquidjava-verifier/src/main/antlr4/rj/grammar/RJ.g4 +++ b/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]+);