Tests for length of String.format of boolean

Author: Joel Allred

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

@@ -0,0 +1,51 @@
+public class Test {
+  public static String testBool(boolean b) {
+    String u = String.format("bool: %b", b);
+    if (u.equals("bool: true"))
+      assert(false);
+    else if (u.equals("bool: false"))
+      assert(false);
+    else
+      assert(false); // unreachable
+    return u;
+  }
+
+  public static String testBoolLength(boolean b) {
+    String u = String.format("bool: %b", b);
+    if (u.length() == 10)
+      assert(false);
+    else if (u.length() == 11)
+      assert(false);
+    else
+      assert(false); // unreachable
+    return u;
+  }
+
+  public static String testBoolLengthTrue() {
+    String u = String.format("bool: %b", true);
+    if (u.length() == 10)
+      assert(false);
+    else
+      assert(false); // unreachable
+    return u;
+  }
+
+  public static String testBoolLengthFalse() {
+    String u = String.format("bool: %b", false);
+    if (u.length() == 11)
+      assert(false);
+    else
+      assert(false); // unreachable
+    return u;
+  }
+
+  public static String testBoolLengthNull() {
+    Boolean b = null;
+    String u = String.format("bool: %b", b);
+    if (u.length() == 11)
+      assert(false);
+    else
+      assert(false); // unreachable
+    return u;
+  }
+}

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

@@ -0,0 +1,12 @@
+public class TestHex {
+  public static String testHex(int i) {
+    String u = String.format("di%xlue", i);
+    if (u.equals("diffblue"))
+      assert(false);
+    else if (u.startsWith("di"))
+      assert(false);
+    else
+      assert(false);
+    return u;
+  }
+}

jbmc/regression/jbmc-strings/StringFormatBool/TestHex.java

@@ -0,0 +1,6 @@
+CORE
+Test.class
+--function Test.testBoolLengthTrue --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` --property "java::Test.testBoolLengthTrue:()Ljava/lang/String;.assertion.1"
+^EXIT=10$
+^SIGNAL=0$
+line 27 assertion at file Test.java .*: FAILURE

jbmc/regression/jbmc-strings/StringFormatBool/test-bool-length-true-fail.desc

@@ -0,0 +1,10 @@
+KNOWNBUG
+Test.class
+--function Test.testBoolLengthTrue --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` --property "java::Test.testBoolLengthTrue:()Ljava/lang/String;.assertion.2"
+^EXIT=0$
+^SIGNAL=0$
+line 29 assertion at file Test.java .*: SUCCESS
+--
+--
+There seems to be some constraints missing, as the length of the 'true'
+boolean can be either 4 or 5.

jbmc/regression/jbmc-strings/StringFormatBool/test-bool-length-true-pass.desc

@@ -0,0 +1,6 @@
+CORE
+Test.class
+--function Test.testBoolLength --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` --property "java::Test.testBoolLength:(Z)Ljava/lang/String;.assertion.1"
+^EXIT=10$
+^SIGNAL=0$
+line 16 assertion at file Test.java .*: FAILURE

jbmc/regression/jbmc-strings/StringFormatBool/test-bool-length1.desc

@@ -0,0 +1,6 @@
+CORE
+Test.class
+--function Test.testBoolLength --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` --property "java::Test.testBoolLength:(Z)Ljava/lang/String;.assertion.2"
+^EXIT=10$
+^SIGNAL=0$
+line 18 assertion at file Test.java .*: FAILURE

jbmc/regression/jbmc-strings/StringFormatBool/test-bool-length2.desc

@@ -0,0 +1,6 @@
+CORE symex-driven-lazy-loading-expected-failure
+Test.class
+--function Test.testBoolLength --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` --property "java::Test.testBoolLength:(Z)Ljava/lang/String;.assertion.3"
+^EXIT=0$
+^SIGNAL=0$
+line 20 assertion at file Test.java .*: SUCCESS

jbmc/regression/jbmc-strings/StringFormatBool/test-bool-length3.desc

@@ -0,0 +1,6 @@
+CORE
+Test.class
+--function Test.testBool --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` --property "java::Test.testBool:(Z)Ljava/lang/String;.assertion.1"
+^EXIT=10$
+^SIGNAL=0$
+line 5 assertion at file Test.java .*: FAILURE

jbmc/regression/jbmc-strings/StringFormatBool/test-bool1.desc

@@ -0,0 +1,6 @@
+CORE
+Test.class
+--function Test.testBool --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` --property "java::Test.testBool:(Z)Ljava/lang/String;.assertion.2"
+^EXIT=10$
+^SIGNAL=0$
+line 7 assertion at file Test.java .*: FAILURE

jbmc/regression/jbmc-strings/StringFormatBool/test-bool2.desc

@@ -0,0 +1,6 @@
+CORE symex-driven-lazy-loading-expected-failure
+Test.class
+--function Test.testBool --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` --property "java::Test.testBool:(Z)Ljava/lang/String;.assertion.3"
+^EXIT=0$
+^SIGNAL=0$
+line 9 assertion at file Test.java .*: SUCCESS