Tests for String.valueOf(int)

Author: romainbrenguier

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

@@ -0,0 +1,68 @@
+public class Test
+{
+    public static String checkDet()
+    {
+        String tmp = String.valueOf(1000000);
+        tmp = String.valueOf(1000001);
+        tmp = String.valueOf(1000002);
+        tmp = String.valueOf(1000003);
+        tmp = String.valueOf(1000004);
+        tmp = String.valueOf(1000005);
+        tmp = String.valueOf(-1000001);
+        tmp = String.valueOf(-1000002);
+        tmp = String.valueOf(-1000003);
+        tmp = String.valueOf(1000004);
+        tmp = String.valueOf(1000005);
+        tmp = String.valueOf(-1000001);
+        tmp = String.valueOf(-1000002);
+        tmp = String.valueOf(1000003);
+        tmp = String.valueOf(1000004);
+        tmp = String.valueOf(1000005);
+        tmp = String.valueOf(1000001);
+        tmp = String.valueOf(-1000002);
+        tmp = String.valueOf(-1000003);
+        tmp = String.valueOf(1000004);
+        tmp = String.valueOf(1000005);
+        return tmp;
+    }
+
+    public static String checkNonDet(int i)
+    {
+        String tmp = String.valueOf(1000000);
+        tmp = String.valueOf(i + 1);
+        tmp = String.valueOf(i + 2);
+        tmp = String.valueOf(i + 3);
+        tmp = String.valueOf(i + 4);
+        tmp = String.valueOf(i + 5);
+        tmp = String.valueOf(i - 1);
+        tmp = String.valueOf(i - 2);
+        tmp = String.valueOf(i - 3);
+        tmp = String.valueOf(i - 4);
+        tmp = String.valueOf(i - 5);
+        tmp += " ";
+        tmp += String.valueOf(i);
+        tmp += " ";
+        tmp += String.valueOf(i + 2);
+        tmp += " ";
+        tmp += String.valueOf(i + 3);
+        tmp += " ";
+        tmp += String.valueOf(-i);
+        tmp += " ";
+        tmp += String.valueOf(-i + 1);
+        tmp += " ";
+        tmp += String.valueOf(-i - 2);
+        return tmp;
+    }
+
+    public static void checkWithDependency(boolean b)
+    {
+        String s = String.valueOf(12);
+        if (b) {
+            assert(s.startsWith("12"));
+        }
+        else {
+            assert(!s.startsWith("12"));
+        }
+    }
+
+}

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

@@ -0,0 +1,10 @@
+CORE
+Test.class
+--function Test.checkWithDependency --depth 10000
+^EXIT=10$
+^SIGNAL=0$
+assertion at file Test.java line 61 .*: SUCCESS
+assertion at file Test.java line 64 .*: FAILURE
+--
+--
+Check that when a dependency is present, the correct constraints are added

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

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

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

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