From 3cdb20bf72dc45b6374da5be0e94c65f73036be9 Mon Sep 17 00:00:00 2001 From: RajShivu Date: Mon, 9 Feb 2026 21:27:09 +0530 Subject: [PATCH 1/4] =?UTF-8?q?Fix=20refinement=20variable=20mapping:=20'?= =?UTF-8?q?=5F'=20and=20'return'=20=E2=86=92?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit --- .../visitors/CreateASTVisitor.java | 20 +++++++++++++++++-- 1 file changed, 18 insertions(+), 2 deletions(-) diff --git a/liquidjava-verifier/src/main/java/liquidjava/rj_language/visitors/CreateASTVisitor.java b/liquidjava-verifier/src/main/java/liquidjava/rj_language/visitors/CreateASTVisitor.java index 1bedda99..7c5d8375 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/rj_language/visitors/CreateASTVisitor.java +++ b/liquidjava-verifier/src/main/java/liquidjava/rj_language/visitors/CreateASTVisitor.java @@ -154,9 +154,25 @@ private Expression literalExpressionCreate(ParseTree rc) throws LJError { return new GroupExpression(create(((LitGroupContext) rc).literalExpression())); else if (rc instanceof LitContext) return create(((LitContext) rc).literal()); + + // else if (rc instanceof VarContext) { + // return new Var(((VarContext) rc).ID().getText()); + // } else if (rc instanceof VarContext) { - return new Var(((VarContext) rc).ID().getText()); - } else if (rc instanceof TargetInvocationContext) { + // Normalize return-value identifiers: + // - "return" (legacy syntax) + // - "_" (current shorthand) + // Both are mapped to "$result", the canonical return value identifier. + String name = ((VarContext) rc).ID().getText(); + + if (name.equals("return") || name.equals("_")) { + name = "$result"; + } + + return new Var(name); + } + + else if (rc instanceof TargetInvocationContext) { // TODO Finish Invocation with Target (a.len()) return null; } else { From 6e7767cb4324230b86a1d24fd7db47ff7326e4cf Mon Sep 17 00:00:00 2001 From: RajShivu Date: Tue, 10 Feb 2026 18:33:13 +0530 Subject: [PATCH 2/4] Fix in refinements: update grammar, visitor, and add regression test --- .../errors/ResultRefinementRegression.java | 34 +++++++++++++++++++ .../src/main/antlr4/rj/grammar/RJ.g4 | 2 +- .../visitors/CreateASTVisitor.java | 11 ++---- 3 files changed, 38 insertions(+), 9 deletions(-) create mode 100644 liquidjava-example/src/main/java/testMultiple/errors/ResultRefinementRegression.java diff --git a/liquidjava-example/src/main/java/testMultiple/errors/ResultRefinementRegression.java b/liquidjava-example/src/main/java/testMultiple/errors/ResultRefinementRegression.java new file mode 100644 index 00000000..193f5ded --- /dev/null +++ b/liquidjava-example/src/main/java/testMultiple/errors/ResultRefinementRegression.java @@ -0,0 +1,34 @@ +package testMultiple.errors; + +import liquidjava.specification.Refinement; + +public class ResultRefinementRegression { + + + @Refinement("_ > 0") + static int positive() { + return 5; + } + + @Refinement("return> 0") + static int broken() { + return -1; + } + + @Refinement("$result > 0") + int testPositive() { + return 10; + } + + @Refinement("$result < 0") + int testNegative() { + return -5; + } + + + public static void main(String[] args) { + int x = positive(); + int y = broken(); + } + +} 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]+); diff --git a/liquidjava-verifier/src/main/java/liquidjava/rj_language/visitors/CreateASTVisitor.java b/liquidjava-verifier/src/main/java/liquidjava/rj_language/visitors/CreateASTVisitor.java index 7c5d8375..0d27e956 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/rj_language/visitors/CreateASTVisitor.java +++ b/liquidjava-verifier/src/main/java/liquidjava/rj_language/visitors/CreateASTVisitor.java @@ -159,17 +159,12 @@ else if (rc instanceof LitContext) // return new Var(((VarContext) rc).ID().getText()); // } else if (rc instanceof VarContext) { - // Normalize return-value identifiers: - // - "return" (legacy syntax) - // - "_" (current shorthand) - // Both are mapped to "$result", the canonical return value identifier. String name = ((VarContext) rc).ID().getText(); - - if (name.equals("return") || name.equals("_")) { - name = "$result"; + if (name.equals("$result") || name.equals("return")) { + name = "_"; } - return new Var(name); + } else if (rc instanceof TargetInvocationContext) { From 7b8f3f7e965494b61dd1e12deeb7c1a87b50d041 Mon Sep 17 00:00:00 2001 From: RajShivu Date: Tue, 10 Feb 2026 18:45:20 +0530 Subject: [PATCH 3/4] Fix handling in refinements and add regression test --- .../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..292af90c 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(11, diagnostics.getErrors().size()); } @Test @@ -39,7 +39,7 @@ public void testMultipleDirectory() { CommandLineLauncher.launch(path); Diagnostics diagnostics = Diagnostics.getInstance(); - assertEquals(11, diagnostics.getErrors().size()); + assertEquals(13, diagnostics.getErrors().size()); assertEquals(3, diagnostics.getWarnings().size()); } } \ No newline at end of file From 055bd3eae193425b9532ccb6cd56d28c66bed5ce Mon Sep 17 00:00:00 2001 From: RajShivu Date: Tue, 10 Feb 2026 18:59:34 +0530 Subject: [PATCH 4/4] TestMultiple modified with test cases, and now revert back --- .../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 292af90c..4480a9f9 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(11, diagnostics.getErrors().size()); + assertEquals(10, diagnostics.getErrors().size()); } @Test @@ -39,7 +39,7 @@ public void testMultipleDirectory() { CommandLineLauncher.launch(path); Diagnostics diagnostics = Diagnostics.getInstance(); - assertEquals(13, diagnostics.getErrors().size()); + assertEquals(12, diagnostics.getErrors().size()); assertEquals(3, diagnostics.getWarnings().size()); } } \ No newline at end of file