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

Add tests for StringBuilder.setLength()

This commit is contained in:
Daniel Poetzl 2019-10-07 20:36:58 +01:00
parent df459cf73a
commit 236d453a48
11 changed files with 144 additions and 0 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

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

Binary file not shown.

62
jbmc/regression/jbmc-strings/ConstantEvaluationStringBuilderSetLength/Test.java Normal file
View File

@ -0,0 +1,62 @@
public class Test
{
public void testSuccess1()
{
StringBuilder sb = new StringBuilder("abc");
sb.setLength(0);
assert sb.toString().equals("");
}
public void testSuccess2()
{
StringBuilder sb = new StringBuilder("abc");
sb.setLength(2);
assert sb.toString().equals("ab");
}
public void testSuccess3()
{
StringBuilder sb = new StringBuilder("abc");
sb.setLength(3);
assert sb.toString().equals("abc");
}
public void testSuccess4()
{
StringBuilder sb = new StringBuilder("abc");
sb.setLength(4);
assert sb.toString().equals("abc\u0000");
}
public void testSuccess5()
{
StringBuilder sb = new StringBuilder("abc");
sb.setLength(5);
assert sb.toString().equals("abc\u0000\u0000");
}
public void testSuccess6(StringBuilder sb)
{
sb.setLength(0);
assert sb.toString().equals("");
}
public void testException()
{
StringBuilder sb = new StringBuilder("abc");
sb.setLength(-1);
}
public void testNoPropagation1(StringBuilder sb)
{
sb.setLength(3);
assert sb.toString().equals("abc");
}
public void testNoPropagation2(int newLength)
{
StringBuilder sb = new StringBuilder("abc");
sb.setLength(newLength);
assert sb.toString().equals("abc");
}
}

10
jbmc/regression/jbmc-strings/ConstantEvaluationStringBuilderSetLength/test_exception.desc Normal file
View File

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

9
jbmc/regression/jbmc-strings/ConstantEvaluationStringBuilderSetLength/test_no_propagation1.desc Normal file
View File

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

9
jbmc/regression/jbmc-strings/ConstantEvaluationStringBuilderSetLength/test_no_propagation2.desc Normal file
View File

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

9
jbmc/regression/jbmc-strings/ConstantEvaluationStringBuilderSetLength/test_success1.desc Normal file
View File

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

9
jbmc/regression/jbmc-strings/ConstantEvaluationStringBuilderSetLength/test_success2.desc Normal file
View File

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

9
jbmc/regression/jbmc-strings/ConstantEvaluationStringBuilderSetLength/test_success3.desc Normal file
View File

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

9
jbmc/regression/jbmc-strings/ConstantEvaluationStringBuilderSetLength/test_success4.desc Normal file
View File

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

9
jbmc/regression/jbmc-strings/ConstantEvaluationStringBuilderSetLength/test_success5.desc Normal file
View File

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

9
jbmc/regression/jbmc-strings/ConstantEvaluationStringBuilderSetLength/test_success6.desc Normal file
View File

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