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

Add tests for StringBuilder.setCharAt()

This commit is contained in:
Daniel Poetzl 2019-10-07 20:36:41 +01:00
parent 8a6b6fefdf
commit c8fdfe7849
8 changed files with 96 additions and 0 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

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

Binary file not shown.

41
jbmc/regression/jbmc-strings/ConstantEvaluationStringBuilderSetCharAt/Test.java Normal file
View File

@ -0,0 +1,41 @@
public class Test
{
public void testSuccess1()
{
StringBuilder sb = new StringBuilder("abc");
sb.setCharAt(0, 'd');
assert sb.toString().equals("dbc");
}
public void testSuccess2()
{
StringBuilder sb = new StringBuilder("abc");
sb.setCharAt(2, 'd');
assert sb.toString().equals("abd");
}
public void testException1()
{
StringBuilder sb = new StringBuilder("abc");
sb.setCharAt(-1, 'd');
}
public void testException2()
{
StringBuilder sb = new StringBuilder("abc");
sb.setCharAt(3, 'd');
}
public void testNoPropagation1(StringBuilder sb)
{
sb.setCharAt(1, 'd');
assert sb.toString().equals("dbc");
}
public void testNoPropagation2(int index)
{
StringBuilder sb = new StringBuilder("abc");
sb.setCharAt(index, 'd');
assert sb.toString().equals("dbc");
}
}

10
jbmc/regression/jbmc-strings/ConstantEvaluationStringBuilderSetCharAt/test_exception1.desc Normal file
View File

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

10
jbmc/regression/jbmc-strings/ConstantEvaluationStringBuilderSetCharAt/test_exception2.desc Normal file
View File

@ -0,0 +1,10 @@
CORE symex-driven-lazy-loading-expected-failure
Test.class
--function Test.testException2 --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` --property 'java::Test.testException2:()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/ConstantEvaluationStringBuilderSetCharAt/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$
--
--

8
jbmc/regression/jbmc-strings/ConstantEvaluationStringBuilderSetCharAt/test_no_propagation2.desc Normal file
View File

@ -0,0 +1,8 @@
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$
--
--

9
jbmc/regression/jbmc-strings/ConstantEvaluationStringBuilderSetCharAt/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/ConstantEvaluationStringBuilderSetCharAt/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$
--
--