Add tests showing the effect on string-max-length

These tests show how the result of the solver can depend on the
string-max-input-length and string-max-length parameters.

Author: romainbrenguier

regression/jbmc-strings/max-length/Test.class

@@ -0,0 +1,37 @@
+public class Test {
+
+    static void checkMaxInputLength(String arg1, String arg2) {
+        // Filter
+        if (arg1 == null || arg2 == null)
+            return;
+
+        // The validity of this depends on string-max-input-length
+        assert arg1.length() + arg2.length() < 1_000_000;
+    }
+
+    static void checkMaxLength(String arg1, String arg2) {
+        // Filter
+        if (arg1 == null || arg2 == null)
+            return;
+
+        if(arg1.length() + arg2.length() < 4_001)
+            return;
+
+        // Act
+        String s = arg1.concat(arg2);
+
+        // When string-max-length is smaller than 4_000 this will
+        // always be the case
+        assert org.cprover.CProverString.charAt(s, 4_000) == '?';
+    }
+
+    static void main(String argv[]) {
+        // Filter
+        if (argv.length < 2)
+            return;
+
+        // Act
+        checkMaxInputLength(argv[0], argv[1]);
+        checkMaxLength(argv[0], argv[1]);
+    }
+}

regression/jbmc-strings/max-length/Test.java

@@ -0,0 +1,6 @@
+CORE
+Test.class
+--refine-strings --verbosity 10 --string-max-input-length 499999 --function Test.checkMaxInputLength
+^EXIT=0$
+^SIGNAL=0$
+assertion.* line 9 function java::Test.checkMaxInputLength.* bytecode-index 16: SUCCESS

regression/jbmc-strings/max-length/test1.desc

@@ -0,0 +1,6 @@
+CORE
+Test.class
+--refine-strings --verbosity 10 --string-max-input-length 500000 --function Test.checkMaxInputLength
+^EXIT=10$
+^SIGNAL=0$
+assertion.* line 9 function java::Test.checkMaxInputLength.* bytecode-index 16: FAILURE

regression/jbmc-strings/max-length/test2.desc

@@ -0,0 +1,6 @@
+CORE
+Test.class
+--refine-strings --verbosity 10 --string-max-length 4001 --function Test.checkMaxLength
+^EXIT=10$
+^SIGNAL=0$
+assertion.* line 25 function java::Test.checkMaxLength.* bytecode-index 26: FAILURE

regression/jbmc-strings/max-length/test3.desc

@@ -0,0 +1,11 @@
+CORE
+Test.class
+--refine-strings --verbosity 10 --string-max-length 4000 --function Test.checkMaxLength
+^SIGNAL=0$
+--
+^EXIT=0$
+assertion.* line 25 function java::Test.checkMaxLength.* bytecode-index 26: SUCCESS
+--
+The solver may give an ERROR because the value of string-max-length is too
+small to give an answer about the assertion.
+So we just check that the answer is not success.