Merge pull request #2052 from romainbrenguier/bugfix/default-axioms2#TG-2138

[TG-2138] Stop adding default axioms in string solver

Author: Daniel Kroening

regression/jbmc-strings/long_string/Test.class

@@ -30,7 +30,9 @@ public static void checkAbort(String s, String t) {
         String u = s.concat(t);
 
         // Filter out
-        if(u.length() < 67_108_864)
+        // 67_108_864 corresponds to the maximum length for which the solver
+        // will concretize the string.
+        if(u.length() <= 67_108_864)
             return;
         if(CProverString.charAt(u, 2_000_000) != 'b')
             return;

regression/jbmc-strings/long_string/Test.java

@@ -1,9 +1,10 @@
 CORE
 Test.class
---refine-strings --function Test.checkAbort
-^EXIT=6$
+--refine-strings --function Test.checkAbort --trace
+^EXIT=10$
 ^SIGNAL=0$
+dynamic_object[0-9]*=\(assignment removed\)
 --
 --
-This tests should abort, because concretizing a string of the required
-length may take to much memory.
+This tests that the object does not appear in the trace, because concretizing
+a string of the required length may take too much memory.

regression/jbmc-strings/long_string/test_abort.desc

@@ -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.class

@@ -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/IntegerTests.java

@@ -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