Tests where model involves long strings

Author: romainbrenguier

regression/jbmc-strings/long_string/Test.class

@@ -0,0 +1,41 @@
+import org.cprover.CProverString;
+
+public class Test {
+    public static void check(String s, String t) {
+        // Filter
+        if(s == null || t == null)
+            return;
+
+        // Act
+        String u = s.concat(t);
+
+        // Filter out
+        if(u.length() < 3_000_000)
+            return;
+        if(CProverString.charAt(u, 500_000) != 'a')
+            return;
+        if(CProverString.charAt(u, 2_000_000) != 'b')
+            return;
+
+        // Assert
+        assert(false);
+    }
+
+    public static void checkAbort(String s, String t) {
+        // Filter
+        if(s == null || t == null)
+            return;
+
+        // Act
+        String u = s.concat(t);
+
+        // Filter out
+        if(u.length() < 67_108_864)
+            return;
+        if(CProverString.charAt(u, 2_000_000) != 'b')
+            return;
+
+        // Assert
+        assert(false);
+    }
+}

regression/jbmc-strings/long_string/Test.java

@@ -0,0 +1,11 @@
+CORE
+Test.class
+--refine-strings --function Test.check --string-max-input-length 2000000
+^EXIT=10$
+^SIGNAL=0$
+assertion at file Test.java line 21 .* FAILURE
+--
+--
+This checks that the solver manage to violate assertions even when this requires
+some very long strings, as long as they don't exceed the arbitrary limit that
+is set by the solver (64M characters).

regression/jbmc-strings/long_string/test.desc

@@ -0,0 +1,8 @@
+CORE
+Test.class
+--refine-strings --function Test.checkAbort
+^EXIT=6$
+^SIGNAL=0$
+--
+--
+This tests should abort, because concretizing a string of the requiered length may take to much memory.