Tests for constant propagation of StringBuffer.append()

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

@@ -0,0 +1,7 @@
+public class Main {
+  public void test() {
+    StringBuffer sb = new StringBuffer("abc");
+    sb.append("xyz");
+    assert sb.toString().equals("abcxyz");
+  }
+}

jbmc/regression/jbmc-strings/ConstantEvaluationStringBufferAppend01/test.desc

@@ -0,0 +1,9 @@
+CORE
+Main.class
+--function Main.test --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar`
+^Generated [0-9]+ VCC\(s\), 0 remaining after simplification$
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+--

jbmc/regression/jbmc-strings/ConstantEvaluationStringBufferAppend02-WithEmptyString/Main.java

@@ -0,0 +1,22 @@
+public class Main {
+  public void test1() {
+    StringBuffer sb1 = new StringBuffer("abc");
+    String s2 = "";
+    sb1.append(s2);
+    assert sb1.toString().equals("abc");
+  }
+
+  public void test2() {
+    StringBuffer sb1 = new StringBuffer();
+    String s2 = "abc";
+    sb1.append(s2);
+    assert sb1.toString().equals("abc");
+  }
+
+  public void test3() {
+    StringBuffer sb1 = new StringBuffer();
+    String s2 = "";
+    sb1.append(s2);
+    assert sb1.toString().equals("");
+  }
+}

jbmc/regression/jbmc-strings/ConstantEvaluationStringBufferAppend02-WithEmptyString/test1.desc

@@ -0,0 +1,9 @@
+CORE
+Main.class
+--function Main.test1 --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar`
+^Generated [0-9]+ VCC\(s\), 0 remaining after simplification$
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+--

jbmc/regression/jbmc-strings/ConstantEvaluationStringBufferAppend02-WithEmptyString/test2.desc

@@ -0,0 +1,9 @@
+CORE
+Main.class
+--function Main.test2 --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar`
+^Generated [0-9]+ VCC\(s\), 0 remaining after simplification$
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+--

jbmc/regression/jbmc-strings/ConstantEvaluationStringBufferAppend02-WithEmptyString/test3.desc

@@ -0,0 +1,9 @@
+CORE
+Main.class
+--function Main.test3 --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar`
+^Generated [0-9]+ VCC\(s\), 0 remaining after simplification$
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+--

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

@@ -0,0 +1,75 @@
+class Test {
+  public void testBooleanSuccess() {
+    StringBuffer sb = new StringBuffer("abc");
+    sb.append(true);
+    assert sb.toString().equals("abctrue");
+  }
+
+  public void testCharSuccess() {
+    StringBuffer sb = new StringBuffer("abc");
+    sb.append('a');
+    assert sb.toString().equals("abca");
+  }
+
+  public void testIntSuccess() {
+    StringBuffer sb = new StringBuffer("abc");
+    sb.append(3);
+    assert sb.toString().equals("abc3");
+  }
+
+  public void testLongSuccess() {
+    StringBuffer sb = new StringBuffer("abc");
+    sb.append(3L);
+    assert sb.toString().equals("abc3");
+  }
+
+  public void testCharSequenceSuccess() {
+    StringBuffer sb = new StringBuffer("abc");
+    CharSequence cs = "xyz";
+    sb.append(cs);
+    assert sb.toString().equals("abcxyz");
+  }
+
+  public void testStringBufferSuccess() {
+    StringBuffer sb = new StringBuffer("abc");
+    StringBuffer buf = new StringBuffer("xyz");
+    sb.append(buf);
+    assert sb.toString().equals("abcxyz");
+  }
+
+  public void testBooleanNoPropagation(boolean b) {
+    StringBuffer sb = new StringBuffer("abc");
+    sb.append(b);
+    assert sb.toString().equals("abctrue");
+  }
+
+  public void testCharNoPropagation(char c) {
+    StringBuffer sb = new StringBuffer("abc");
+    sb.append(c);
+    assert sb.toString().equals("abca");
+  }
+
+  public void testIntNoPropagation(int i) {
+    StringBuffer sb = new StringBuffer("abc");
+    sb.append(i);
+    assert sb.toString().equals("abc3");
+  }
+
+  public void testLongNoPropagation(long l) {
+    StringBuffer sb = new StringBuffer("abc");
+    sb.append(l);
+    assert sb.toString().equals("abc3");
+  }
+
+  public void testCharSequenceNoPropagation(CharSequence cs) {
+    StringBuffer sb = new StringBuffer("abc");
+    sb.append(cs);
+    assert sb.toString().equals("abcxyz");
+  }
+
+  public void testStringBufferNoPropagation(StringBuffer buf) {
+    StringBuffer sb = new StringBuffer("abc");
+    sb.append(buf);
+    assert sb.toString().equals("abcxyz");
+  }
+}

jbmc/regression/jbmc-strings/ConstantEvaluationStringBufferAppend03/test_bool_no_propagation.desc

@@ -0,0 +1,9 @@
+CORE symex-driven-lazy-loading-expected-failure
+Test.class
+--function Test.testBooleanNoPropagation --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` --property 'java::Test.testBooleanNoPropagation:(Z)V.assertion.1'
+^Generated [0-9]+ VCC\(s\), 1 remaining after simplification$
+^EXIT=10$
+^SIGNAL=0$
+^VERIFICATION FAILED$
+--
+--

jbmc/regression/jbmc-strings/ConstantEvaluationStringBufferAppend03/test_bool_success.desc

@@ -0,0 +1,9 @@
+FUTURE
+Test.class
+--function Test.testBooleanSuccess --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar`
+^Generated [0-9]+ VCC\(s\), 0 remaining after simplification$
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+--

jbmc/regression/jbmc-strings/ConstantEvaluationStringBufferAppend03/test_char_no_propagation.desc

@@ -0,0 +1,9 @@
+CORE symex-driven-lazy-loading-expected-failure
+Test.class
+--function Test.testCharNoPropagation --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` --property 'java::Test.testCharNoPropagation:(C)V.assertion.1'
+^Generated [0-9]+ VCC\(s\), 1 remaining after simplification$
+^EXIT=10$
+^SIGNAL=0$
+^VERIFICATION FAILED$
+--
+--

jbmc/regression/jbmc-strings/ConstantEvaluationStringBufferAppend03/test_char_sequence_no_propagation.desc

@@ -0,0 +1,9 @@
+CORE symex-driven-lazy-loading-expected-failure
+Test.class
+--function Test.testCharSequenceNoPropagation --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` --property 'java::Test.testCharSequenceNoPropagation:(Ljava/lang/CharSequence;)V.assertion.1'
+^Generated [0-9]+ VCC\(s\), 1 remaining after simplification$
+^EXIT=10$
+^SIGNAL=0$
+^VERIFICATION FAILED$
+--
+--

jbmc/regression/jbmc-strings/ConstantEvaluationStringBufferAppend03/test_char_sequence_success.desc

@@ -0,0 +1,9 @@
+CORE
+Test.class
+--function Test.testCharSequenceSuccess --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar`
+^Generated [0-9]+ VCC\(s\), 0 remaining after simplification$
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+--

jbmc/regression/jbmc-strings/ConstantEvaluationStringBufferAppend03/test_char_success.desc

@@ -0,0 +1,9 @@
+FUTURE
+Test.class
+--function Test.testCharSuccess --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar`
+^Generated [0-9]+ VCC\(s\), 0 remaining after simplification$
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+--

jbmc/regression/jbmc-strings/ConstantEvaluationStringBufferAppend03/test_int_no_propagation.desc

@@ -0,0 +1,9 @@
+CORE symex-driven-lazy-loading-expected-failure
+Test.class
+--function Test.testIntNoPropagation --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` --property 'java::Test.testIntNoPropagation:(I)V.assertion.1'
+^Generated [0-9]+ VCC\(s\), 1 remaining after simplification$
+^EXIT=10$
+^SIGNAL=0$
+^VERIFICATION FAILED$
+--
+--

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

@@ -0,0 +1,9 @@
+CORE
+Test.class
+--function Test.testIntSuccess --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar`
+^Generated [0-9]+ VCC\(s\), 0 remaining after simplification$
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+--

jbmc/regression/jbmc-strings/ConstantEvaluationStringBufferAppend03/test_long_no_propagation.desc

@@ -0,0 +1,9 @@
+CORE symex-driven-lazy-loading-expected-failure
+Test.class
+--function Test.testLongNoPropagation --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` --property 'java::Test.testLongNoPropagation:(J)V.assertion.1'
+^Generated [0-9]+ VCC\(s\), 1 remaining after simplification$
+^EXIT=10$
+^SIGNAL=0$
+^VERIFICATION FAILED$
+--
+--

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

@@ -0,0 +1,9 @@
+FUTURE
+Test.class
+--function Test.testLongSuccess --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar`
+^Generated [0-9]+ VCC\(s\), 0 remaining after simplification$
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+--

jbmc/regression/jbmc-strings/ConstantEvaluationStringBufferAppend03/test_string_buffer_no_propagation.desc

@@ -0,0 +1,9 @@
+CORE symex-driven-lazy-loading-expected-failure
+Test.class
+--function Test.testStringBufferNoPropagation --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` --property 'java::Test.testStringBufferNoPropagation:(Ljava/lang/StringBuffer;)V.assertion.1'
+^Generated [0-9]+ VCC\(s\), 1 remaining after simplification$
+^EXIT=10$
+^SIGNAL=0$
+^VERIFICATION FAILED$
+--
+--

jbmc/regression/jbmc-strings/ConstantEvaluationStringBufferAppend03/test_string_buffer_success.desc

@@ -0,0 +1,9 @@
+CORE
+Test.class
+--function Test.testStringBufferSuccess --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar`
+^Generated [0-9]+ VCC\(s\), 0 remaining after simplification$
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+--

jbmc/src/java_bytecode/java_string_library_preprocess.cpp

@@ -1752,9 +1752,6 @@ void java_string_library_preprocesst::initialize_conversion_table()
   cprover_equivalent_to_java_assign_and_return_function
     ["java::java.lang.StringBuffer.append:(C)Ljava/lang/StringBuffer;"]=
       ID_cprover_string_concat_char_func;
-  cprover_equivalent_to_java_assign_and_return_function
-    ["java::java.lang.StringBuffer.append:(J)Ljava/lang/StringBuffer;"]=
-      ID_cprover_string_concat_long_func;
   cprover_equivalent_to_java_assign_and_return_function
     ["java::java.lang.StringBuffer.append:(Ljava/lang/String;)"
       "Ljava/lang/StringBuffer;"]=

src/util/irep_ids.def

@@ -596,7 +596,6 @@ IREP_ID_ONE(cprover_string_code_point_count_func)
 IREP_ID_ONE(cprover_string_offset_by_code_point_func)
 IREP_ID_ONE(cprover_string_compare_to_func)
 IREP_ID_ONE(cprover_string_concat_func)
-IREP_ID_ONE(cprover_string_concat_long_func)
 IREP_ID_ONE(cprover_string_concat_char_func)
 IREP_ID_ONE(cprover_string_concat_code_point_func)
 IREP_ID_ONE(cprover_string_constrain_characters_func)