replica
/
diffblue-cbmc
1
0
Fork 0
Code Issues Pull Requests Projects Releases Wiki Activity

Merge pull request #5122 from danpoe/feature/append-object-constant-evaluation-tests 

Tests for constant propagation of append(Object)
This commit is contained in:
Daniel Poetzl 2019-10-11 14:06:04 +01:00 committed by GitHub
parent 9f818162cb 906c2f3945
commit afac9c7224
No known key found for this signature in database
GPG Key ID: 4AEE18F83AFDEB23
8 changed files with 80 additions and 0 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

BIN
jbmc/regression/jbmc-strings/ConstantEvaluationStringBufferAppend04-Object/Test.class Normal file
View File

Binary file not shown.

22
jbmc/regression/jbmc-strings/ConstantEvaluationStringBufferAppend04-Object/Test.java Normal file
View File

@ -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("");
}
}

9
jbmc/regression/jbmc-strings/ConstantEvaluationStringBufferAppend04-Object/test_no_propagation.desc Normal file
View File

@ -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$
--
--

9
jbmc/regression/jbmc-strings/ConstantEvaluationStringBufferAppend04-Object/test_success.desc Normal file
View File

@ -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$
--
--

BIN
jbmc/regression/jbmc-strings/ConstantEvaluationStringBuilderAppend04-Object/Test.class Normal file
View File

Binary file not shown.

22
jbmc/regression/jbmc-strings/ConstantEvaluationStringBuilderAppend04-Object/Test.java Normal file
View File

@ -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("");
}
}

9
jbmc/regression/jbmc-strings/ConstantEvaluationStringBuilderAppend04-Object/test_no_propagation.desc Normal file
View File

@ -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$
--
--

9
jbmc/regression/jbmc-strings/ConstantEvaluationStringBuilderAppend04-Object/test_success.desc Normal file
View File

@ -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$
--
--