Skip to content

Commit a3bee27

Browse files
author
RajShivu
committed
Support as a restricted refinement variable
1 parent 58a5475 commit a3bee27

2 files changed

Lines changed: 15 additions & 3 deletions

File tree

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

Lines changed: 4 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -36,6 +36,7 @@ operand:
3636
literalExpression:
3737
'(' literalExpression ')' #litGroup
3838
| literal #lit
39+
| RESULT #result
3940
| ID #var
4041
| ID '.' functionCall #targetInvocation
4142
| functionCall #invocation
@@ -91,8 +92,9 @@ ARITHOP : '+'|'*'|'/'|'%';//|'-';
9192
BOOL : 'true' | 'false';
9293
ID_UPPER: ([A-Z][a-zA-Z0-9]*);
9394
OBJECT_TYPE:
94-
(([a-zA-Z][a-zA-Z0-9]+) ('.' [a-zA-Z][a-zA-Z0-9]*)+);
95-
ID : '#'*('$')? [a-zA-Z_] [a-zA-Z0-9_#]* ;
95+
(([a-zA-Z][a-zA-Z0-9]+) ('.' [a-zA-Z][a-zA-Z0-9]*)+);
96+
RESULT : '$result';
97+
ID : '#'*[a-zA-Z_][a-zA-Z0-9_#]*;
9698
STRING : '"'(~["])*'"';
9799
INT : (([0-9]+) | ([0-9]+('_'[0-9]+)*));
98100
REAL : (([0-9]+('.'[0-9]+)?) | '.'[0-9]+);

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

Lines changed: 11 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -49,6 +49,7 @@
4949
import rj.grammar.RJParser.PredLogicContext;
5050
import rj.grammar.RJParser.PredNegateContext;
5151
import rj.grammar.RJParser.ProgContext;
52+
import rj.grammar.RJParser.ResultContext;
5253
import rj.grammar.RJParser.StartContext;
5354
import rj.grammar.RJParser.StartPredContext;
5455
import rj.grammar.RJParser.TargetInvocationContext;
@@ -159,9 +160,18 @@ else if (rc instanceof VarContext) {
159160
} else if (rc instanceof TargetInvocationContext) {
160161
// TODO Finish Invocation with Target (a.len())
161162
return null;
162-
} else {
163+
}
164+
// else {
165+
// return create(((InvocationContext) rc).functionCall());
166+
// }
167+
else if (rc instanceof ResultContext) {
168+
return new Var("$result");
169+
} else if (rc instanceof InvocationContext) {
163170
return create(((InvocationContext) rc).functionCall());
171+
} else {
172+
throw new IllegalStateException("Unknown literalExpression: " + rc.getClass());
164173
}
174+
165175
}
166176

167177
private Expression functionCallCreate(FunctionCallContext rc) throws LJError {

0 commit comments

Comments
 (0)