Add FUTURE regression tests for char arrays and string-printable

In order to implement this constraint for arrays, we would have to do a
loop even though the element type is primitive. This was deemed to
costly in terms of time for the benefit at the time of implementation.

jbmc/regression/strings-smoke-tests/java_string_printable/Test.java

@@ -33,4 +33,14 @@ public class Test {
       return b;
     }
 
+    public static boolean printable_char_array(char[] c) {
+      if(c.length != 3 || c == null)
+        return false;
+      boolean b0 = c[0] >= ' ' && c[0] <= '~';
+      boolean b1 = c[1] >= ' ' && c[1] <= '~';
+      boolean b2 = c[2] >= ' ' && c[2] <= '~';
+      assert(b0 || b1 || b2);
+      return b0 || b1 || b2;
+    }
+
 }

jbmc/regression/strings-smoke-tests/java_string_printable/test_nonprintable_char_array.desc

@@ -0,0 +1,11 @@
+FUTURE
+Test.class
+--function Test.printable_char_array --max-nondet-string-length 100
+assertion.* file Test.java line 42 .* FAILURE
+^EXIT=10$
+^SIGNAL=0$
+--
+Shows that the assertion can be violated when string-printable is not enabled
+for character arrays
+
+The constraint has not been implemented for char arrays.

jbmc/regression/strings-smoke-tests/java_string_printable/test_printable_char_array.desc

@@ -0,0 +1,12 @@
+FUTURE
+Test.class
+--function Test.printable_char_array --max-nondet-string-length 100 --string-printable
+^EXIT=10$
+^SIGNAL=0$
+--
+assertion.* file Test.java line 42 .* FAILURE
+--
+Shows that the assertion can be violated when string-printable is not enabled
+for character arrays
+
+The constraint has not been implemented for char arrays.