Skip to content

Commit 87ef6e6

Browse files
author
RajShivu
committed
Result: implement identifier for method refinements
1 parent 055bd3e commit 87ef6e6

File tree

5 files changed

+28
-43
lines changed

5 files changed

+28
-43
lines changed

liquidjava-example/src/main/java/testMultiple/errors/ResultRefinementRegression.java

Lines changed: 0 additions & 34 deletions
This file was deleted.
Lines changed: 16 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,16 @@
1+
package testSuite;
2+
3+
import liquidjava.specification.Refinement;
4+
5+
public class CorrectResult {
6+
7+
@Refinement("$result > 10")
8+
public int getLargeNumber() {
9+
return 15;
10+
}
11+
12+
@Refinement("$result == (a + b)")
13+
public int sum(int a, int b) {
14+
return a + b;
15+
}
16+
}
Lines changed: 10 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,10 @@
1+
// Not Found Error
2+
package testSuite;
3+
import liquidjava.specification.Refinement;
4+
5+
public class ErrorResultVariable {
6+
public void test() {
7+
@Refinement("$result > 0")
8+
int x = 10;
9+
}
10+
}

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

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -161,6 +161,7 @@ private Predicate handleFunctionRefinements(RefinedFunction f, CtElement method,
161161
Optional<Predicate> oret = rtc.getRefinementFromAnnotation(method);
162162
Predicate ret = oret.orElse(new Predicate());
163163
ret = ret.substituteVariable("return", Keys.WILDCARD);
164+
ret = ret.substituteVariable("$result", Keys.WILDCARD);// new change for $result
164165
f.setRefReturn(ret);
165166
return Predicate.createConjunction(joint, ret);
166167
}

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

Lines changed: 1 addition & 9 deletions
Original file line numberDiff line numberDiff line change
@@ -155,16 +155,8 @@ private Expression literalExpressionCreate(ParseTree rc) throws LJError {
155155
else if (rc instanceof LitContext)
156156
return create(((LitContext) rc).literal());
157157

158-
// else if (rc instanceof VarContext) {
159-
// return new Var(((VarContext) rc).ID().getText());
160-
// }
161158
else if (rc instanceof VarContext) {
162-
String name = ((VarContext) rc).ID().getText();
163-
if (name.equals("$result") || name.equals("return")) {
164-
name = "_";
165-
}
166-
return new Var(name);
167-
159+
return new Var(((VarContext) rc).ID().getText());
168160
}
169161

170162
else if (rc instanceof TargetInvocationContext) {

0 commit comments

Comments
 (0)