Tests for constant propagation of StringBuilder.append()

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

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

jbmc/regression/jbmc-strings/ConstantEvaluationStringBuilderAppend03/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/ConstantEvaluationStringBuilderAppend03/test_bool_success.desc

@@ -0,0 +1,9 @@
+CORE
+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/ConstantEvaluationStringBuilderAppend03/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/ConstantEvaluationStringBuilderAppend03/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/ConstantEvaluationStringBuilderAppend03/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/ConstantEvaluationStringBuilderAppend03/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/ConstantEvaluationStringBuilderAppend03/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/ConstantEvaluationStringBuilderAppend03/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/ConstantEvaluationStringBuilderAppend03/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/ConstantEvaluationStringBuilderAppend03/test_long_success.desc

@@ -0,0 +1,9 @@
+CORE
+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/ConstantEvaluationStringBuilderAppend03/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/ConstantEvaluationStringBuilderAppend03/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

@@ -1692,6 +1692,9 @@ void java_string_library_preprocesst::initialize_conversion_table()
   cprover_equivalent_to_java_assign_and_return_function
     ["java::java.lang.StringBuilder.append:(Ljava/lang/String;)"
      "Ljava/lang/StringBuilder;"] = ID_cprover_string_concat_func;
+  cprover_equivalent_to_java_assign_and_return_function
+    ["java::java.lang.StringBuilder.append:(Ljava/lang/StringBuffer;)"
+     "Ljava/lang/StringBuilder;"] = ID_cprover_string_concat_func;
   cprover_equivalent_to_java_assign_and_return_function
     ["java::java.lang.StringBuilder.appendCodePoint:(I)"
      "Ljava/lang/StringBuilder;"]=