Add Tests

Author: rcosta358

liquidjava-example/src/main/java/testSuite/CorrectChars.java

@@ -0,0 +1,22 @@
+package testSuite;
+
+import liquidjava.specification.Refinement;
+
+public class CorrectChars {
+
+    @Refinement("_ == 65")
+    int getA() {
+        return 'A';
+    }
+
+    void test() {
+        printLetter('A');
+        printLetter('Z');
+        printLetter('a');
+        printLetter('z');
+    }
+
+    void printLetter(@Refinement("_ >= 65 && _ <= 90 || _ >= 97 && _ <= 122") char c) {
+        System.out.println(c);
+    }
+}

liquidjava-example/src/main/java/testSuite/ErrorChars.java

@@ -0,0 +1,15 @@
+
+package testSuite;
+
+import liquidjava.specification.Refinement;
+
+public class ErrorChars {
+
+    void test() {
+        printLetter('$'); // error
+    }
+
+    void printLetter(@Refinement("_ >= 65 && _ <= 90 || _ >= 97 && _ <= 122") char c) {
+        System.out.println(c);
+    }
+}

liquidjava-verifier/src/main/java/liquidjava/rj_language/ast/typing/TypeInfer.java

@@ -39,10 +39,10 @@ else if (e instanceof LiteralLong)
             return Optional.of(Utils.getType("long", factory));
         else if (e instanceof LiteralReal)
             return Optional.of(Utils.getType("double", factory));
-        else if (e instanceof LiteralBoolean)
-            return boolType(factory);
         else if (e instanceof LiteralChar)
             return Optional.of(Utils.getType("char", factory));
+        else if (e instanceof LiteralBoolean)
+            return boolType(factory);
         else if (e instanceof Var)
             return varType(ctx, (Var) e);
         else if (e instanceof UnaryExpression)

liquidjava-verifier/src/main/java/liquidjava/smt/TranslatorContextToZ3.java

@@ -42,7 +42,8 @@ public static void storeVariablesSubtypes(Context z3, List<RefinedVariable> vari
     private static Expr<?> getExpr(Context z3, String name, CtTypeReference<?> type) {
         String typeName = type.getQualifiedName();
         return switch (typeName) {
-        case "int", "short", "java.lang.Integer", "java.lang.Short" -> z3.mkIntConst(name);
+        case "int", "short", "char", "java.lang.Integer", "java.lang.Short", "java.lang.Character" ->
+            z3.mkIntConst(name);
         case "boolean", "java.lang.Boolean" -> z3.mkBoolConst(name);
         case "long", "java.lang.Long" -> z3.mkRealConst(name);
         case "float", "double", "java.lang.Float", "java.lang.Double" -> (FPExpr) z3.mkConst(name, z3.mkFPSort64());
@@ -81,7 +82,8 @@ private static void addBuiltinFunctions(Context z3, Map<String, FuncDecl<?>> fun
 
     static Sort getSort(Context z3, String sort) {
         return switch (sort) {
-        case "int", "short", "java.lang.Integer", "java.lang.Short" -> z3.getIntSort();
+        case "int", "short", "char", "java.lang.Integer", "java.lang.Short", "java.lang.Character" ->
+            z3.getIntSort();
         case "boolean", "java.lang.Boolean" -> z3.getBoolSort();
         case "long", "java.lang.Long" -> z3.getRealSort();
         case "float", "java.lang.Float" -> z3.mkFPSort32();