Tests for CProverString.substring

Author: romainbrenguier

regression/jbmc-strings/StringSubstring/Test.class

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

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

regression/jbmc-strings/StringSubstring/test.desc

@@ -0,0 +1,10 @@
+CORE
+Test.class
+--refine-strings --unwind 10 --string-max-input-length 6 --function Test.testFail
+^EXIT=10$
+^SIGNAL=0$
+assertion at file Test.java line 37 .*: FAILURE
+assertion at file Test.java line 39 .*: FAILURE
+assertion at file Test.java line 41 .*: FAILURE
+assertion at file Test.java line 43 .*: FAILURE
+assertion at file Test.java line 45 .*: FAILURE