Test for CProverString.insert

This function behaves slightly differently from StringBuilder.insert
since it never raise an exception.
This tests the cases where the index exceeds the limits.

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