Tests for String.toUpperCase

Author: romainbrenguier

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

@@ -0,0 +1,50 @@
+public class Test {
+    public String det()
+    {
+        StringBuilder builder = new StringBuilder();
+        builder.append("abcdefghijklmnopqrstuvwxyzABCDEFGHIJKLMNOPQRSTUVWXYZ".toLowerCase());
+        builder.append("abcdeghijklmnopfrstuqwxyzABCDvFGHIJKLMENOPQRSTUVWXYZ".toUpperCase());
+        builder.append("abcdeghijlmnopqrstvwxyzABCDEFGHIJuKLMNOPQRSfkTUVWXYZ".toUpperCase());
+        builder.append("acdefghijklmnopqrsuvwxyzABCDEFbGHIJKLMNOPtQRSTUVWXYZ".toUpperCase());
+        builder.append("abcdfghijklmnopqrstuvwxyzABCDEFGHIJeKLMNOPQRSTUVWXYZ".toUpperCase());
+        return builder.toString();
+    }
+
+    public String nonDet(String s)
+    {
+        if(s.length() < 20)
+            return "Short string";
+        if(!s.startsWith("A"))
+            return "String not starting with A";
+
+        StringBuilder builder = new StringBuilder();
+        builder.append(s.toUpperCase());
+        builder.append(s.toUpperCase());
+        builder.append(":");
+        builder.append(s);
+        builder.append(":");
+        builder.append(s.toUpperCase());
+        builder.append(s.toUpperCase());
+        return builder.toString();
+    }
+
+    public String withDependency(String s, boolean b)
+    {
+        // Filter
+        if(s == null || s.length() < 20)
+            return "Short string";
+        if(!s.endsWith("A"))
+            return "String not ending with A";
+
+        // Act
+        String result = s + s.toUpperCase();
+
+        // Assert
+        if(b) {
+            assert(result.endsWith("a"));
+        } else {
+            assert(!result.endsWith("a"));
+        }
+        return result;
+    }
+}

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

@@ -0,0 +1,10 @@
+CORE
+Test.class
+--function Test.withDependency --verbosity 10 --max-nondet-string-length 10000
+^EXIT=10$
+^SIGNAL=0$
+assertion at file Test.java line 44 .*: SUCCESS
+assertion at file Test.java line 46 .*: FAILURE
+--
+--
+Check that when there are dependency, axioms are added correctly.

jbmc/regression/jbmc-strings/StringToUpperCase/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 9 .*: SATISFIED
+--
+adding lemma .*nondet_infinite_array
+--
+Check that using the string dependence informations, no lemma involving arrays is added

jbmc/regression/jbmc-strings/StringToUpperCase/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 27 .*: SATISFIED
+--
+adding lemma .*nondet_infinite_array
+--
+Check that using the string dependence informations, no lemma involving arrays is added