Merge pull request #1939 from romainbrenguier/bugfix/builtin-string-insert-eval

Fix StringBuilder.insert and String.substring [TG-2459]

Author: romainbrenguier

regression/jbmc-strings/StringBuilderInsert/Test.class

@@ -0,0 +1,48 @@
+
+public class Test {
+    public void check (int i) {
+        if(i == 0)
+        {
+            // Arrange
+            StringBuilder s = new StringBuilder("bar");
+
+            // Act
+            s = org.cprover.CProverString.insert(s, 0, "foo");
+
+            // Should succeed
+            assert s.toString().equals("foobar");
+
+            // Should fail
+            assert !s.toString().equals("foobar");
+        }
+        if(i == 1)
+        {
+            // Arrange
+            StringBuilder s = new StringBuilder("bar");
+
+            // Act
+            s = org.cprover.CProverString.insert(s, -10, "foo");
+
+            // Should succeed
+            assert s.toString().equals("foobar");
+
+            // Should fail
+            assert !s.toString().equals("foobar");
+        }
+        if(i == 2)
+        {
+            // Arrange
+            StringBuilder s = new StringBuilder("bar");
+
+            // Act
+            s = org.cprover.CProverString.insert(s, 10, "foo");
+
+            // Should succeed
+            assert s.toString().equals("barfoo");
+
+            // Should fail
+            assert !s.toString().equals("barfoo");
+        }
+
+    }
+}

regression/jbmc-strings/StringBuilderInsert/Test.java

@@ -0,0 +1,12 @@
+CORE
+Test.class
+--refine-strings --function Test.check
+^EXIT=10$
+^SIGNAL=0$
+assertion at file Test.java line 13 .*: SUCCESS
+assertion at file Test.java line 16 .*: FAILURE
+assertion at file Test.java line 27 .*: SUCCESS
+assertion at file Test.java line 30 .*: FAILURE
+assertion at file Test.java line 41 .*: SUCCESS
+assertion at file Test.java line 44 .*: FAILURE
+--

regression/jbmc-strings/StringBuilderInsert/test.desc

@@ -0,0 +1,40 @@
+// This test uses CProverString so should be compiled with
+// javac Test.java ../cprover/CProverString.java
+import org.cprover.CProverString;
+
+class Test {
+    public void testSuccess(String s, String t, int start, int end) {
+        // Filter
+        if (s == null || t == null)
+            return;
+
+        // Act
+        StringBuilder sb = new StringBuilder(s);
+        String result = CProverString.append(sb, t, start, end).toString();
+
+        // Arrange
+        StringBuilder reference = new StringBuilder(s);
+        if(start < 0)
+            start = 0;
+        for (int i = start; i < end && i < t.length(); i++)
+            reference.append(org.cprover.CProverString.charAt(t, i));
+
+        // Assert
+        assert result.equals(reference.toString());
+    }
+
+    public void testFail(int i) {
+        // Arrange
+        StringBuilder sb = new StringBuilder("foo");
+
+        // Act
+        CProverString.append(sb, "bar", 0, 1);
+        CProverString.append(sb, "bar", 0, 4);
+        CProverString.append(sb, "foo", -1, 0);
+        CProverString.append(sb, "foo", -10, -1);
+        CProverString.append(sb, "bar", -10, 25);
+
+        // Assert
+        assert !sb.toString().equals("foobbarbar");
+    }
+}

regression/jbmc-strings/StringConcat_StringII/Test.class

@@ -0,0 +1,8 @@
+CORE
+Test.class
+--refine-strings --string-max-length 100 --string-max-input-length 4 --verbosity 10 --unwind 5 Test.class --function Test.testSuccess
+^EXIT=0$
+^SIGNAL=0$
+assertion at file Test.java line 23 .*: SUCCESS
+--
+^warning: ignoring

regression/jbmc-strings/StringConcat_StringII/Test.java

@@ -0,0 +1,8 @@
+CORE
+Test.class
+--refine-strings --string-max-length 10000 --verbosity 10 Test.class --function Test.testFail
+^EXIT=10$
+^SIGNAL=0$
+assertion at file Test.java line 38 .*: FAILURE
+--
+^warning: ignoring

regression/jbmc-strings/StringConcat_StringII/test.desc

@@ -0,0 +1,47 @@
+// This test uses CProverString so should be compiled with
+// javac Test.java ../cprover/CProverString.java
+
+class Test {
+    public void testSuccess(String s, int start, int end) {
+        // Filter
+        if (s == null)
+            return;
+
+        // Act
+        String sub = org.cprover.CProverString.substring(s, start, end);
+
+        // Arrange
+        StringBuilder reference = new StringBuilder();
+        if(start < 0)
+            start = 0;
+        for (int i = start; i < end && i < s.length(); i++)
+            reference.append(org.cprover.CProverString.charAt(s, i));
+
+        // Assert
+        assert sub.equals(reference.toString());
+    }
+
+    public void testFail(int i) {
+        // Arrange
+        String[] s = new String[5];
+
+        // Act
+        s[0] = org.cprover.CProverString.substring("foo", 0, 1);
+        s[1] = org.cprover.CProverString.substring("foo", 0, 4);
+        s[2] = org.cprover.CProverString.substring("foo", -1, 0);
+        s[3] = org.cprover.CProverString.substring("foo", -10, -1);
+        s[4] = org.cprover.CProverString.substring("foo", -10, 25);
+
+        // Assert
+        if(i == 0)
+            assert !s[0].equals("f");
+        if(i == 1)
+            assert !s[1].equals("foo");
+        if(i == 2)
+            assert !s[2].equals("");
+        if(i == 3)
+            assert !s[3].equals("");
+        if(i == 4)
+            assert !s[4].equals("foo");
+    }
+}

regression/jbmc-strings/StringConcat_StringII/test_fail.desc

@@ -0,0 +1,6 @@
+CORE
+Test.class
+--refine-strings --unwind 10 --string-max-input-length 6  --function Test.testSuccess
+^EXIT=0$
+^SIGNAL=0$
+assertion at file Test.java line 21.*: SUCCESS