Skip to content

Commit 6e7767c

Browse files
author
RajShivu
committed
Fix in refinements: update grammar, visitor, and add regression test
1 parent 3cdb20b commit 6e7767c

File tree

3 files changed

+38
-9
lines changed

3 files changed

+38
-9
lines changed
Lines changed: 34 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,34 @@
1+
package testMultiple.errors;
2+
3+
import liquidjava.specification.Refinement;
4+
5+
public class ResultRefinementRegression {
6+
7+
8+
@Refinement("_ > 0")
9+
static int positive() {
10+
return 5;
11+
}
12+
13+
@Refinement("return> 0")
14+
static int broken() {
15+
return -1;
16+
}
17+
18+
@Refinement("$result > 0")
19+
int testPositive() {
20+
return 10;
21+
}
22+
23+
@Refinement("$result < 0")
24+
int testNegative() {
25+
return -5;
26+
}
27+
28+
29+
public static void main(String[] args) {
30+
int x = positive();
31+
int y = broken();
32+
}
33+
34+
}

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

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -92,7 +92,7 @@ BOOL : 'true' | 'false';
9292
ID_UPPER: ([A-Z][a-zA-Z0-9]*);
9393
OBJECT_TYPE:
9494
(([a-zA-Z][a-zA-Z0-9]+) ('.' [a-zA-Z][a-zA-Z0-9]*)+);
95-
ID : '#'*[a-zA-Z_][a-zA-Z0-9_#]*;
95+
ID : '#'*('$')? [a-zA-Z_] [a-zA-Z0-9_#]* ;
9696
STRING : '"'(~["])*'"';
9797
INT : (([0-9]+) | ([0-9]+('_'[0-9]+)*));
9898
REAL : (([0-9]+('.'[0-9]+)?) | '.'[0-9]+);

liquidjava-verifier/src/main/java/liquidjava/rj_language/visitors/CreateASTVisitor.java

Lines changed: 3 additions & 8 deletions
Original file line numberDiff line numberDiff line change
@@ -159,17 +159,12 @@ else if (rc instanceof LitContext)
159159
// return new Var(((VarContext) rc).ID().getText());
160160
// }
161161
else if (rc instanceof VarContext) {
162-
// Normalize return-value identifiers:
163-
// - "return" (legacy syntax)
164-
// - "_" (current shorthand)
165-
// Both are mapped to "$result", the canonical return value identifier.
166162
String name = ((VarContext) rc).ID().getText();
167-
168-
if (name.equals("return") || name.equals("_")) {
169-
name = "$result";
163+
if (name.equals("$result") || name.equals("return")) {
164+
name = "_";
170165
}
171-
172166
return new Var(name);
167+
173168
}
174169

175170
else if (rc instanceof TargetInvocationContext) {

0 commit comments

Comments
 (0)