Tests for constant propagation of append(Object)

jbmc/regression/jbmc-strings/ConstantEvaluationStringBufferAppend04-Object/Test.java

@@ -0,0 +1,22 @@
+public class Test
+{
+  public void testSuccess()
+  {
+    StringBuffer sb = new StringBuffer("abc");
+    Integer i = new Integer(3);
+    sb.append(i);
+    assert sb.toString().equals("abc3");
+
+    sb.append((Object)"xyz");
+    assert sb.toString().equals("abc3xyz");
+
+    sb.append((Object)null);
+    assert sb.toString().equals("abc3xyznull");
+  }
+
+  public void testNoPropagation(Object obj)
+  {
+    StringBuffer sb = new StringBuffer();
+    assert obj.toString().equals("");
+  }
+}

jbmc/regression/jbmc-strings/ConstantEvaluationStringBufferAppend04-Object/test_no_propagation.desc

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

jbmc/regression/jbmc-strings/ConstantEvaluationStringBufferAppend04-Object/test_success.desc

@@ -0,0 +1,9 @@
+CORE
+Test.class
+--function Test.testSuccess --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/ConstantEvaluationStringBuilderAppend04-Object/Test.java

@@ -0,0 +1,22 @@
+public class Test
+{
+  public void testSuccess()
+  {
+    StringBuilder sb = new StringBuilder("abc");
+    Integer i = new Integer(3);
+    sb.append(i);
+    assert sb.toString().equals("abc3");
+
+    sb.append((Object)"xyz");
+    assert sb.toString().equals("abc3xyz");
+
+    sb.append((Object)null);
+    assert sb.toString().equals("abc3xyznull");
+  }
+
+  public void testNoPropagation(Object obj)
+  {
+    StringBuilder sb = new StringBuilder();
+    assert obj.toString().equals("");
+  }
+}

jbmc/regression/jbmc-strings/ConstantEvaluationStringBuilderAppend04-Object/test_no_propagation.desc

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

jbmc/regression/jbmc-strings/ConstantEvaluationStringBuilderAppend04-Object/test_success.desc

@@ -0,0 +1,9 @@
+CORE
+Test.class
+--function Test.testSuccess --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$
+--
+--