Add test for generics array and strings

This adds an int greater than string-max-length in a generic array.
This is to check that TG-2138 is fixed.
Before the issue was solved setting the array to 101 was in
contradiction with default axioms added by the string solver.

Author: romainbrenguier

regression/jbmc-strings/max-length-generic-array/IntegerTests.class

@@ -0,0 +1,44 @@
+public class IntegerTests {
+
+    public static Boolean testMyGenSet(Integer key) {
+        if (key == null) return null;
+        MyGenSet<Integer> ms = new MyGenSet<>();
+        ms.array[0] = 101;
+        if (ms.contains(key)) return true;
+        return false;
+    }
+
+    public static Boolean testMySet(Integer key) {
+        if (key == null) return null;
+        MySet ms = new MySet();
+        ms.array[0] = 101;
+        if (ms.contains(key)) return true;
+        return false;
+    }
+
+}
+
+class MyGenSet<E> {
+    E[] array;
+    @SuppressWarnings("unchecked")
+    MyGenSet() {
+        array = (E[]) new Object[1];
+    }
+    boolean contains(E o) {
+        if (o.equals(array[0]))
+            return true;
+        return false;
+    }
+}
+
+class MySet {
+    Integer[] array;
+    MySet() {
+        array = new Integer[1];
+    }
+    boolean contains(Integer o) {
+        if (o.equals(array[0]))
+            return true;
+        return false;
+    }
+}

regression/jbmc-strings/max-length-generic-array/IntegerTests.java

@@ -0,0 +1,19 @@
+CORE
+IntegerTests.class
+-refine-strings --string-max-length 100 IntegerTests.class --function IntegerTests.testMySet --cover location
+^EXIT=0$
+^SIGNAL=0$
+coverage.* line 12 function java::IntegerTests.testMySet.* bytecode-index 1 .* SATISFIED
+coverage.* line 12 function java::IntegerTests.testMySet.* bytecode-index 3 .* SATISFIED
+coverage.* line 13 function java::IntegerTests.testMySet.* bytecode-index 4 .* SATISFIED
+coverage.* line 13 function java::IntegerTests.testMySet.* bytecode-index 6 .* SATISFIED
+coverage.* line 13 function java::IntegerTests.testMySet.* bytecode-index 7 .* SATISFIED
+coverage.* line 14 function java::IntegerTests.testMySet.* bytecode-index 12 .* SATISFIED
+coverage.* line 14 function java::IntegerTests.testMySet.* bytecode-index 13 .* SATISFIED
+coverage.* line 15 function java::IntegerTests.testMySet.* bytecode-index 16 .* SATISFIED
+coverage.* line 15 function java::IntegerTests.testMySet.* bytecode-index 17 .* SATISFIED
+coverage.* line 16 function java::IntegerTests.testMySet.* bytecode-index 21 .* SATISFIED
+coverage.* line 15 function java::IntegerTests.testMySet.* bytecode-index 19 .* SATISFIED
+coverage.* line 15 function java::IntegerTests.testMySet.* bytecode-index 20 .* SATISFIED
+coverage.* line 16 function java::IntegerTests.testMySet.* bytecode-index 22 .* SATISFIED
+coverage.* line 16 function java::IntegerTests.testMySet.* bytecode-index 23 .* SATISFIED

regression/jbmc-strings/max-length-generic-array/MyGenSet.class

@@ -0,0 +1,20 @@
+CORE
+IntegerTests.class
+-refine-strings --string-max-length 100 IntegerTests.class --function IntegerTests.testMyGenSet --cover location
+^EXIT=0$
+^SIGNAL=0$
+coverage.* line 4 function java::IntegerTests.testMyGenSet.* bytecode-index 1 .* SATISFIED
+coverage.* line 4 function java::IntegerTests.testMyGenSet.* bytecode-index 3 .* SATISFIED
+coverage.* line 5 function java::IntegerTests.testMyGenSet.* bytecode-index 4 .* SATISFIED
+coverage.* line 5 function java::IntegerTests.testMyGenSet.* bytecode-index 6 .* SATISFIED
+coverage.* line 5 function java::IntegerTests.testMyGenSet.* bytecode-index 7 .* SATISFIED
+coverage.* line 6 function java::IntegerTests.testMyGenSet.* bytecode-index 10 .* SATISFIED
+coverage.* line 6 function java::IntegerTests.testMyGenSet.* bytecode-index 13 .* SATISFIED
+coverage.* line 6 function java::IntegerTests.testMyGenSet.* bytecode-index 14 .* SATISFIED
+coverage.* line 7 function java::IntegerTests.testMyGenSet.* bytecode-index 17 .* SATISFIED
+coverage.* line 7 function java::IntegerTests.testMyGenSet.* bytecode-index 18 .* SATISFIED
+coverage.* line 8 function java::IntegerTests.testMyGenSet.* bytecode-index 22 .* SATISFIED
+coverage.* line 7 function java::IntegerTests.testMyGenSet.* bytecode-index 20 .* SATISFIED
+coverage.* line 7 function java::IntegerTests.testMyGenSet.* bytecode-index 21 .* SATISFIED
+coverage.* line 8 function java::IntegerTests.testMyGenSet.* bytecode-index 23 .* SATISFIED
+coverage.* line 8 function java::IntegerTests.testMyGenSet.* bytecode-index 24 .* SATISFIED