Tests for StringBuilder.setCharAt

Author: romainbrenguier

jbmc/regression/jbmc-strings/StringBuilderSetCharAt/Test.class

@@ -0,0 +1,62 @@
+public class Test {
+    public String det()
+    {
+        StringBuilder builder = new StringBuilder("abcdefghijklmnopqrstuvwxyz");
+        builder.setCharAt(3, '!');
+        builder.setCharAt(5, '!');
+        builder.setCharAt(7, '!');
+        builder.setCharAt(9, '!');
+        builder.setCharAt(13, '!');
+        builder.setCharAt(15, '!');
+        builder.setCharAt(17, '!');
+        builder.setCharAt(19, '!');
+        builder.setCharAt(4, ':');
+        builder.setCharAt(5, ':');
+        builder.setCharAt(6, ':');
+        builder.setCharAt(9, ':');
+        builder.setCharAt(10, ':');
+        builder.setCharAt(11, ':');
+        builder.setCharAt(16, ':');
+        builder.setCharAt(18, ':');
+        return builder.toString();
+    }
+
+    public String nonDet(String s, char c, int i)
+    {
+        StringBuilder builder = new StringBuilder(s);
+        if(i + 5 >= s.length() || 19 >= s.length() || i < 0)
+            return "Out of bounds";
+        builder.setCharAt(i, c);
+        builder.setCharAt(i+5, 'x');
+        builder.setCharAt(7, '!');
+        builder.setCharAt(9, '!');
+        builder.setCharAt(13, '!');
+        builder.setCharAt(15, '!');
+        builder.setCharAt(17, '!');
+        builder.setCharAt(19, '!');
+        builder.setCharAt(4, ':');
+        builder.setCharAt(5, ':');
+        builder.setCharAt(6, c);
+        builder.setCharAt(9, ':');
+        builder.setCharAt(10, ':');
+        builder.setCharAt(11, ':');
+        builder.setCharAt(16, ':');
+        builder.setCharAt(18, ':');
+        return builder.toString();
+    }
+
+    public String withDependency(boolean b)
+    {
+        StringBuilder builder = new StringBuilder("abcdefghijklmnopqrstuvwxyz");
+        builder.setCharAt(3, '!');
+        builder.setCharAt(5, '!');
+
+        if(b) {
+            assert builder.toString().startsWith("abc!");
+        } else {
+            assert !builder.toString().startsWith("abc!");
+        }
+        return builder.toString();
+    }
+
+}

jbmc/regression/jbmc-strings/StringBuilderSetCharAt/Test.java

@@ -0,0 +1,12 @@
+CORE
+Test.class
+--function Test.withDependency --max-nondet-string-length 1000
+^EXIT=10$
+^SIGNAL=0$
+assertion at file Test.java line 55 .*: SUCCESS
+assertion at file Test.java line 57 .*: FAILURE
+--
+--
+Check that when a dependency is present, the correct constraints are added
+
+

jbmc/regression/jbmc-strings/StringBuilderSetCharAt/test_dependency.desc

@@ -0,0 +1,10 @@
+CORE
+Test.class
+--function Test.det  --verbosity 10 --cover location
+^EXIT=0$
+^SIGNAL=0$
+coverage.* file Test.java line 21 .*: SATISFIED
+--
+adding lemma .*nondet_infinite_array
+--
+Check that using the string dependence informations, no lemma involving arrays is added

jbmc/regression/jbmc-strings/StringBuilderSetCharAt/test_det.desc

@@ -0,0 +1,10 @@
+CORE
+Test.class
+--function Test.nonDet --verbosity 10 --cover location --max-nondet-string-length 1000
+^EXIT=0$
+^SIGNAL=0$
+coverage.* file Test.java line 45 .*: SATISFIED
+--
+adding lemma .*nondet_infinite_array
+--
+Check that using the string dependence informations, no lemma involving arrays is added