Build char literals directly instead of parsing their text

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;
+    }
+}

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;
+    }
+}

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);

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)

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);