Tests for length of String.format of hexadecimal integer

Author: Joel Allred

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

@@ -9,4 +9,14 @@ else if (u.startsWith("di"))
       assert(false);
     return u;
   }
+
+  public static void testHexLengthConstPASS() {
+    String u = String.format("di%xlue", 255);
+    assert u.length() == 7;
+  }
+
+  public static void testHexLengthConstFAIL() {
+    String u = String.format("di%xlue", 255);
+    assert u.length() != 7;
+  }
 }

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

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

jbmc/regression/jbmc-strings/StringFormatHex/test-hex-length-const-fail.desc

@@ -0,0 +1,6 @@
+CORE
+Test.class
+--function Test.testHexLengthConstPASS --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` --property "java::Test.testHexLengthConstPASS:()V.assertion.1"
+^EXIT=0$
+^SIGNAL=0$
+line 15 assertion at file Test.java .*: SUCCESS