diff --git a/jbmc/regression/jbmc-strings/ConstantEvaluationStringBuilderAppend03/Test.class b/jbmc/regression/jbmc-strings/ConstantEvaluationStringBuilderAppend03/Test.class new file mode 100644 index 0000000000..f132779bbd Binary files /dev/null and b/jbmc/regression/jbmc-strings/ConstantEvaluationStringBuilderAppend03/Test.class differ diff --git a/jbmc/regression/jbmc-strings/ConstantEvaluationStringBuilderAppend03/Test.java b/jbmc/regression/jbmc-strings/ConstantEvaluationStringBuilderAppend03/Test.java new file mode 100644 index 0000000000..f2a95718e8 --- /dev/null +++ b/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"); + } +} diff --git a/jbmc/regression/jbmc-strings/ConstantEvaluationStringBuilderAppend03/test_bool_no_propagation.desc b/jbmc/regression/jbmc-strings/ConstantEvaluationStringBuilderAppend03/test_bool_no_propagation.desc new file mode 100644 index 0000000000..9c35cb0910 --- /dev/null +++ b/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$ +-- +-- diff --git a/jbmc/regression/jbmc-strings/ConstantEvaluationStringBuilderAppend03/test_bool_success.desc b/jbmc/regression/jbmc-strings/ConstantEvaluationStringBuilderAppend03/test_bool_success.desc new file mode 100644 index 0000000000..572ca82879 --- /dev/null +++ b/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$ +-- +-- diff --git a/jbmc/regression/jbmc-strings/ConstantEvaluationStringBuilderAppend03/test_char_no_propagation.desc b/jbmc/regression/jbmc-strings/ConstantEvaluationStringBuilderAppend03/test_char_no_propagation.desc new file mode 100644 index 0000000000..d6e618d4b3 --- /dev/null +++ b/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$ +-- +-- diff --git a/jbmc/regression/jbmc-strings/ConstantEvaluationStringBuilderAppend03/test_char_sequence_no_propagation.desc b/jbmc/regression/jbmc-strings/ConstantEvaluationStringBuilderAppend03/test_char_sequence_no_propagation.desc new file mode 100644 index 0000000000..a5125e01ca --- /dev/null +++ b/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$ +-- +-- diff --git a/jbmc/regression/jbmc-strings/ConstantEvaluationStringBuilderAppend03/test_char_sequence_success.desc b/jbmc/regression/jbmc-strings/ConstantEvaluationStringBuilderAppend03/test_char_sequence_success.desc new file mode 100644 index 0000000000..b11ca109df --- /dev/null +++ b/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$ +-- +-- diff --git a/jbmc/regression/jbmc-strings/ConstantEvaluationStringBuilderAppend03/test_char_success.desc b/jbmc/regression/jbmc-strings/ConstantEvaluationStringBuilderAppend03/test_char_success.desc new file mode 100644 index 0000000000..6de73b7407 --- /dev/null +++ b/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$ +-- +-- diff --git a/jbmc/regression/jbmc-strings/ConstantEvaluationStringBuilderAppend03/test_int_no_propagation.desc b/jbmc/regression/jbmc-strings/ConstantEvaluationStringBuilderAppend03/test_int_no_propagation.desc new file mode 100644 index 0000000000..2428805c10 --- /dev/null +++ b/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$ +-- +-- diff --git a/jbmc/regression/jbmc-strings/ConstantEvaluationStringBuilderAppend03/test_int_success.desc b/jbmc/regression/jbmc-strings/ConstantEvaluationStringBuilderAppend03/test_int_success.desc new file mode 100644 index 0000000000..4c3745a29b --- /dev/null +++ b/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$ +-- +-- diff --git a/jbmc/regression/jbmc-strings/ConstantEvaluationStringBuilderAppend03/test_long_no_propagation.desc b/jbmc/regression/jbmc-strings/ConstantEvaluationStringBuilderAppend03/test_long_no_propagation.desc new file mode 100644 index 0000000000..62dc3085ff --- /dev/null +++ b/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$ +-- +-- diff --git a/jbmc/regression/jbmc-strings/ConstantEvaluationStringBuilderAppend03/test_long_success.desc b/jbmc/regression/jbmc-strings/ConstantEvaluationStringBuilderAppend03/test_long_success.desc new file mode 100644 index 0000000000..c316ab5a6c --- /dev/null +++ b/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$ +-- +-- diff --git a/jbmc/regression/jbmc-strings/ConstantEvaluationStringBuilderAppend03/test_string_buffer_no_propagation.desc b/jbmc/regression/jbmc-strings/ConstantEvaluationStringBuilderAppend03/test_string_buffer_no_propagation.desc new file mode 100644 index 0000000000..67fb56823d --- /dev/null +++ b/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$ +-- +-- diff --git a/jbmc/regression/jbmc-strings/ConstantEvaluationStringBuilderAppend03/test_string_buffer_success.desc b/jbmc/regression/jbmc-strings/ConstantEvaluationStringBuilderAppend03/test_string_buffer_success.desc new file mode 100644 index 0000000000..26960274e8 --- /dev/null +++ b/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$ +-- +--