Conversion functions from primitive types to strings

jbmc/regression/jbmc-strings/CProverStringToString/Main.java

@@ -0,0 +1,132 @@
+import org.cprover.CProverString;
+
+class Main {
+  public void testIntSuccess(int choice) {
+    int i;
+    String r;
+
+    switch (choice) {
+    case 0:
+      i = 0;
+      r = "0";
+      break;
+    case 1:
+      i = 1;
+      r = "1";
+      break;
+    case 2:
+      i = -1;
+      r = "-1";
+      break;
+    case 3:
+      i = Integer.MIN_VALUE;
+      r = "-2147483648";
+    case 4:
+      i = Integer.MAX_VALUE;
+      r = "2147483647";
+    default:
+      return;
+    }
+
+    String s = CProverString.toString(i);
+    assert s.equals(r);
+  }
+
+  public void testIntFailure() {
+    String s = CProverString.toString(123);
+    assert s.equals("0");
+  }
+
+  public void testLongSuccess(int choice) {
+    long l;
+    String r;
+
+    switch (choice) {
+    case 0:
+      l = 0L;
+      r = "0";
+      break;
+    case 1:
+      l = 1L;
+      r = "1";
+      break;
+    case 2:
+      l = -1L;
+      r = "-1";
+      break;
+    case 3:
+      l = Long.MIN_VALUE;
+      ;
+      r = "-9223372036854775808";
+      break;
+    case 4:
+      l = Long.MAX_VALUE;
+      r = "9223372036854775807";
+      break;
+    default:
+      return;
+    }
+
+    String s = CProverString.toString(l);
+    assert s.equals(r);
+  }
+
+  public void testLongFailure() {
+    String s = CProverString.toString(9223372036854775807L);
+    assert s.equals("0");
+  }
+
+  public void testFloatSuccess(int choice) {
+    float f;
+    String r;
+
+    switch (choice) {
+    case 0:
+      f = 0F;
+      r = "0.0";
+      break;
+    case 1:
+      f = 1F;
+      r = "1.0";
+      break;
+    case 2:
+      f = -1F;
+      r = "-1.0";
+      break;
+    case 3:
+      f = 1.1F;
+      r = "1.1";
+      break;
+    case 4:
+      f = Float.MAX_VALUE;
+      r = "3.4028235E38";
+      break;
+    case 5:
+      f = Float.MIN_VALUE;
+      r = "1.4E-45";
+      break;
+    case 6:
+      f = Float.POSITIVE_INFINITY;
+      r = "Infinity";
+      break;
+    case 7:
+      f = Float.NEGATIVE_INFINITY;
+      r = "-Infinity";
+      break;
+    case 8:
+      f = Float.NaN;
+      r = "NaN";
+      break;
+    default:
+      return;
+    }
+
+    String s = CProverString.toString(f);
+    assert s.equals(r);
+  }
+
+  public void testFloatFailure() {
+    String s = CProverString.toString(1.1F);
+    assert s.equals("0");
+  }
+}

jbmc/regression/jbmc-strings/CProverStringToString/test_float_fail.desc

@@ -0,0 +1,8 @@
+CORE
+Main.class
+--function Main.testFloatFailure --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar`
+^VERIFICATION FAILED$
+^EXIT=10$
+^SIGNAL=0$
+--
+--

jbmc/regression/jbmc-strings/CProverStringToString/test_float_success.desc

@@ -0,0 +1,8 @@
+KNOWNBUG
+Main.class
+--function Main.testFloatSuccess --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar`
+^VERIFICATION SUCCESSFUL$
+^EXIT=0$
+^SIGNAL=0$
+--
+--

jbmc/regression/jbmc-strings/CProverStringToString/test_int_fail.desc

@@ -0,0 +1,8 @@
+CORE
+Main.class
+--function Main.testIntFailure --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar`
+^VERIFICATION FAILED$
+^EXIT=10$
+^SIGNAL=0$
+--
+--

jbmc/regression/jbmc-strings/CProverStringToString/test_int_success.desc

@@ -0,0 +1,8 @@
+CORE
+Main.class
+--function Main.testIntSuccess --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar`
+^VERIFICATION SUCCESSFUL$
+^EXIT=0$
+^SIGNAL=0$
+--
+--

jbmc/regression/jbmc-strings/CProverStringToString/test_long_fail.desc

@@ -0,0 +1,8 @@
+CORE
+Main.class
+--function Main.testLongFailure --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar`
+^VERIFICATION FAILED$
+^EXIT=10$
+^SIGNAL=0$
+--
+--

jbmc/regression/jbmc-strings/CProverStringToString/test_long_success.desc

@@ -0,0 +1,8 @@
+CORE
+Main.class
+--function Main.testLongSuccess --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar`
+^VERIFICATION SUCCESSFUL$
+^EXIT=0$
+^SIGNAL=0$
+--
+--

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

@@ -0,0 +1,13 @@
+public class Test {
+  public void test1() {
+    char c = '\uFFFF';
+    String s = String.valueOf(c);
+    assert s.equals("\uFFFF");
+  }
+
+  public void test2() {
+    char c = '\uFFFE';
+    String s = String.valueOf(c);
+    assert s.equals("\uFFFE");
+  }
+}

jbmc/regression/jbmc-strings/CharToString/test1.desc

@@ -0,0 +1,6 @@
+KNOWNBUG
+Test.class
+--function Test.test1 --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar`
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$

jbmc/regression/jbmc-strings/CharToString/test2.desc

@@ -0,0 +1,6 @@
+CORE
+Test.class
+--function Test.test2 --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar`
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$

jbmc/regression/jbmc-strings/cprover/CProverString.java

@@ -147,4 +147,12 @@ public static StringBuffer insert(
             StringBuffer sb, int offset, long l) {
         return sb.insert(offset, l);
     }
+
+    public static String toString(int i) { return String.valueOf(i); }
+
+    public static String toString(long l) { return String.valueOf(l); }
+
+    public static String toString(float f) { return String.valueOf(f); }
+
+    public static String toString(double d) { return String.valueOf((float)d); }
 }