diff --git a/liquidjava-example/src/main/java/testSuite/CorrectCharLiteralComparisons.java b/liquidjava-example/src/main/java/testSuite/CorrectCharLiteralComparisons.java new file mode 100644 index 00000000..672da0a2 --- /dev/null +++ b/liquidjava-example/src/main/java/testSuite/CorrectCharLiteralComparisons.java @@ -0,0 +1,40 @@ +package testSuite; + +import liquidjava.specification.Refinement; + +@SuppressWarnings("unused") +public class CorrectCharLiteralComparisons { + + static int skipTo(String s) { + int i = 0; + while (s.charAt(i) != '[') + i++; + return i; + } + + static boolean isSeparator(char c) { + return c == '{' || c == '}' || c == ',' || c == ' ' || c == 'Z' || c == '"' || c == '\\'; + } + + @Refinement("_ == 48") + static int zero(char c) { + if (c == '0') + return c; + return 48; + } + + @Refinement("_ == 97") + static int letterA(char c) { + int a = 5; + if (c == 'a') + return c; + return 97; + } + + @Refinement("_ == 91") + static int bracket(char c) { + char d = c; + d += '[' - c; + return d; + } +} diff --git a/liquidjava-example/src/main/java/testSuite/ErrorCharLiteralComparisons.java b/liquidjava-example/src/main/java/testSuite/ErrorCharLiteralComparisons.java new file mode 100644 index 00000000..a4e05948 --- /dev/null +++ b/liquidjava-example/src/main/java/testSuite/ErrorCharLiteralComparisons.java @@ -0,0 +1,22 @@ +package testSuite; + +import liquidjava.specification.Refinement; + +@SuppressWarnings("unused") +public class ErrorCharLiteralComparisons { + + @Refinement("_ == 0") + static int zero(char c) { + if (c == '0') + return c; // Expect: Refinement Error + return 0; + } + + @Refinement("_ == 5") + static int letterA(char c) { + int a = 5; + if (c == 'a') + return c; // Expect: Refinement Error + return 5; + } +} diff --git a/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/RefinementTypeChecker.java b/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/RefinementTypeChecker.java index 3b6e3ac8..6541b902 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/RefinementTypeChecker.java +++ b/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/RefinementTypeChecker.java @@ -882,7 +882,7 @@ private Predicate getExpressionRefinements(CtExpression element) throws LJErr return getRefinement(op); } else if (element instanceof CtLiteral) { CtLiteral l = (CtLiteral) element; - return new Predicate(l.getValue().toString(), l); + return Predicate.createLit(l.getValue(), l); } else if (element instanceof CtInvocation) { CtInvocation inv = (CtInvocation) element; visitCtInvocation(inv); diff --git a/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/general_checkers/OperationsChecker.java b/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/general_checkers/OperationsChecker.java index a6f008ac..a739148f 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/general_checkers/OperationsChecker.java +++ b/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/general_checkers/OperationsChecker.java @@ -311,7 +311,7 @@ private Predicate getOperationRefinements(CtBinaryOperator operator, CtVariab return new Predicate(); } - return new Predicate(l.getValue().toString(), element); + return Predicate.createLit(l.getValue(), element); } else if (element instanceof CtInvocation inv) { CtExecutable method = inv.getExecutable().getDeclaration(); @@ -428,7 +428,7 @@ private Predicate getOperatorAssignmentRefinement(CtExpression element) throw } else if (element instanceof CtLiteral literal) { if (literal.getValue() == null) return new Predicate(); // null literals are not supported yet, carry no information - return new Predicate(literal.getValue().toString(), element); + return Predicate.createLit(literal.getValue(), element); } else if (element instanceof CtInvocation) { VariableInstance invocationValue = (VariableInstance) element.getMetadata(Keys.TARGET); if (invocationValue != null) diff --git a/liquidjava-verifier/src/main/java/liquidjava/rj_language/Predicate.java b/liquidjava-verifier/src/main/java/liquidjava/rj_language/Predicate.java index 0dfc158f..1d660bab 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/rj_language/Predicate.java +++ b/liquidjava-verifier/src/main/java/liquidjava/rj_language/Predicate.java @@ -339,6 +339,16 @@ public static Predicate createITE(Predicate c1, Predicate c2, Predicate c3) { return new Predicate(new Ite(c1.getExpression(), c2.getExpression(), c3.getExpression())); } + /** + * Wrap the value of a Java literal as an RJ literal. The literal node is built directly instead of parsing the + * value's text, since RJ has no char-literal syntax: {@code '['} would not parse and {@code 'a'} would read as a + * variable. + */ + public static Predicate createLit(Object value, CtElement element) throws LJError { + Predicate lit = StaticConstants.asLiteralPredicate(value); + return lit != null ? lit : new Predicate(value.toString(), element); + } + public static Predicate createLit(String value, String type) { Expression exp = switch (type) { case Types.BOOLEAN -> new LiteralBoolean(value);