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 1bedda99..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 @@ -154,9 +154,20 @@ 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) { + String name = ((VarContext) rc).ID().getText(); + if (name.equals("$result") || name.equals("return")) { + name = "_"; + } + return new Var(name); + + } + + else if (rc instanceof TargetInvocationContext) { // TODO Finish Invocation with Target (a.len()) return null; } else { 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..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(9, diagnostics.getErrors().size()); + assertEquals(10, diagnostics.getErrors().size()); } @Test @@ -39,7 +39,7 @@ public void testMultipleDirectory() { CommandLineLauncher.launch(path); Diagnostics diagnostics = Diagnostics.getInstance(); - assertEquals(11, diagnostics.getErrors().size()); + assertEquals(12, diagnostics.getErrors().size()); assertEquals(3, diagnostics.getWarnings().size()); } } \ No newline at end of file