Merge pull request #5125 from danpoe/fixes/string-preprocessing-string-buffer-delete-char-at

Fix string solver string preprocessing of deleteCharAt()

jbmc/regression/strings-smoke-tests/java_delete_char_at/TestDeleteCharAt.java

@@ -0,0 +1,42 @@
+public class TestDeleteCharAt
+{
+   public static void testStringBuilderSuccess(boolean b)
+   {
+      String s = b ? "abc" : "xyz";
+      StringBuilder sb = new StringBuilder(s);
+      org.cprover.CProverString.deleteCharAt(sb, 1);
+      String result = sb.toString();
+      assert !b || result.equals("ac");
+      assert b || result.equals("xz");
+   }
+
+   public static void testStringBuilderFailure(boolean b)
+   {
+      String s = b ? "abc" : "xyz";
+      StringBuilder sb = new StringBuilder(s);
+      org.cprover.CProverString.deleteCharAt(sb, 1);
+      String result = sb.toString();
+      assert !b || result.equals("ab");
+      assert b || result.equals("yz");
+   }
+
+   public static void testStringBufferSuccess(boolean b)
+   {
+      String s = b ? "abc" : "xyz";
+      StringBuffer sb = new StringBuffer(s);
+      org.cprover.CProverString.deleteCharAt(sb, 1);
+      String result = sb.toString();
+      assert !b || result.equals("ac");
+      assert b || result.equals("xz");
+   }
+
+   public static void testStringBufferFailure(boolean b)
+   {
+      String s = b ? "abc" : "xyz";
+      StringBuffer sb = new StringBuffer(s);
+      org.cprover.CProverString.deleteCharAt(sb, 1);
+      String result = sb.toString();
+      assert !b || result.equals("ab");
+      assert b || result.equals("yz");
+   }
+}

jbmc/regression/strings-smoke-tests/java_delete_char_at/test.desc

@@ -1,8 +0,0 @@
-CORE
-test_delete_char_at.class
---max-nondet-string-length 1000 --function test_delete_char_at.main --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar`
-^EXIT=0$
-^SIGNAL=0$
-^VERIFICATION SUCCESSFUL$
---
-non equal types

jbmc/regression/strings-smoke-tests/java_delete_char_at/test_delete_char_at.java

@@ -1,11 +0,0 @@
-public class test_delete_char_at
-{
-   public static void main()
-   {
-      StringBuilder s = new StringBuilder();
-      s.append("Abc");
-      org.cprover.CProverString.deleteCharAt(s, 1);
-      String str = s.toString();
-      assert(str.equals("Ac"));
-   }
-}

jbmc/regression/strings-smoke-tests/java_delete_char_at/test_string_buffer_failure.desc

@@ -0,0 +1,8 @@
+CORE
+TestDeleteCharAt.class
+--max-nondet-string-length 1000 --function TestDeleteCharAt.testStringBufferFailure --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar`
+^EXIT=10$
+^SIGNAL=0$
+^VERIFICATION FAILED$
+--
+non equal types

jbmc/regression/strings-smoke-tests/java_delete_char_at/test_string_buffer_success.desc

@@ -0,0 +1,8 @@
+CORE
+TestDeleteCharAt.class
+--max-nondet-string-length 1000 --function TestDeleteCharAt.testStringBufferSuccess --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar`
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+non equal types

jbmc/regression/strings-smoke-tests/java_delete_char_at/test_string_builder_failure.desc

@@ -0,0 +1,8 @@
+CORE
+TestDeleteCharAt.class
+--max-nondet-string-length 1000 --function TestDeleteCharAt.testStringBuilderFailure --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar`
+^EXIT=10$
+^SIGNAL=0$
+^VERIFICATION FAILED$
+--
+non equal types

jbmc/regression/strings-smoke-tests/java_delete_char_at/test_string_builder_success.desc

@@ -0,0 +1,8 @@
+CORE
+TestDeleteCharAt.class
+--max-nondet-string-length 1000 --function TestDeleteCharAt.testStringBuilderSuccess --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar`
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+non equal types

jbmc/src/java_bytecode/java_string_library_preprocess.cpp

@@ -1507,7 +1507,7 @@ void java_string_library_preprocesst::initialize_conversion_table()
       ID_cprover_string_delete_func;
   cprover_equivalent_to_java_assign_and_return_function
     ["java::org.cprover.CProverString.deleteCharAt:(Ljava/lang/"
-     "StringBufferI)Ljava/lang/StringBuffer;"] =
+     "StringBuffer;I)Ljava/lang/StringBuffer;"] =
       ID_cprover_string_delete_char_at_func;
   cprover_equivalent_to_java_assign_and_return_function
     ["java::org.cprover.CProverString.deleteCharAt:(Ljava/lang/"