diff --git a/jbmc/regression/jbmc-strings/ConstantEvaluationStringBufferAppend01/Main.class b/jbmc/regression/jbmc-strings/ConstantEvaluationStringBufferAppend01/Main.class new file mode 100644 index 00000000000..39f7f4e104d Binary files /dev/null and b/jbmc/regression/jbmc-strings/ConstantEvaluationStringBufferAppend01/Main.class differ diff --git a/jbmc/regression/jbmc-strings/ConstantEvaluationStringBufferAppend01/Main.java b/jbmc/regression/jbmc-strings/ConstantEvaluationStringBufferAppend01/Main.java new file mode 100644 index 00000000000..2e2a6bbcfc4 --- /dev/null +++ b/jbmc/regression/jbmc-strings/ConstantEvaluationStringBufferAppend01/Main.java @@ -0,0 +1,7 @@ +public class Main { + public void test() { + StringBuffer sb = new StringBuffer("abc"); + sb.append("xyz"); + assert sb.toString().equals("abcxyz"); + } +} diff --git a/jbmc/regression/jbmc-strings/ConstantEvaluationStringBufferAppend01/test.desc b/jbmc/regression/jbmc-strings/ConstantEvaluationStringBufferAppend01/test.desc new file mode 100644 index 00000000000..fb11e5707f3 --- /dev/null +++ b/jbmc/regression/jbmc-strings/ConstantEvaluationStringBufferAppend01/test.desc @@ -0,0 +1,9 @@ +CORE +Main.class +--function Main.test --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/ConstantEvaluationStringBufferAppend02-WithEmptyString/Main.class b/jbmc/regression/jbmc-strings/ConstantEvaluationStringBufferAppend02-WithEmptyString/Main.class new file mode 100644 index 00000000000..abf6e6d8882 Binary files /dev/null and b/jbmc/regression/jbmc-strings/ConstantEvaluationStringBufferAppend02-WithEmptyString/Main.class differ diff --git a/jbmc/regression/jbmc-strings/ConstantEvaluationStringBufferAppend02-WithEmptyString/Main.java b/jbmc/regression/jbmc-strings/ConstantEvaluationStringBufferAppend02-WithEmptyString/Main.java new file mode 100644 index 00000000000..85749a98d70 --- /dev/null +++ b/jbmc/regression/jbmc-strings/ConstantEvaluationStringBufferAppend02-WithEmptyString/Main.java @@ -0,0 +1,22 @@ +public class Main { + public void test1() { + StringBuffer sb1 = new StringBuffer("abc"); + String s2 = ""; + sb1.append(s2); + assert sb1.toString().equals("abc"); + } + + public void test2() { + StringBuffer sb1 = new StringBuffer(); + String s2 = "abc"; + sb1.append(s2); + assert sb1.toString().equals("abc"); + } + + public void test3() { + StringBuffer sb1 = new StringBuffer(); + String s2 = ""; + sb1.append(s2); + assert sb1.toString().equals(""); + } +} diff --git a/jbmc/regression/jbmc-strings/ConstantEvaluationStringBufferAppend02-WithEmptyString/test1.desc b/jbmc/regression/jbmc-strings/ConstantEvaluationStringBufferAppend02-WithEmptyString/test1.desc new file mode 100644 index 00000000000..8914f55af0a --- /dev/null +++ b/jbmc/regression/jbmc-strings/ConstantEvaluationStringBufferAppend02-WithEmptyString/test1.desc @@ -0,0 +1,9 @@ +CORE +Main.class +--function Main.test1 --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/ConstantEvaluationStringBufferAppend02-WithEmptyString/test2.desc b/jbmc/regression/jbmc-strings/ConstantEvaluationStringBufferAppend02-WithEmptyString/test2.desc new file mode 100644 index 00000000000..dc7a010c361 --- /dev/null +++ b/jbmc/regression/jbmc-strings/ConstantEvaluationStringBufferAppend02-WithEmptyString/test2.desc @@ -0,0 +1,9 @@ +CORE +Main.class +--function Main.test2 --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/ConstantEvaluationStringBufferAppend02-WithEmptyString/test3.desc b/jbmc/regression/jbmc-strings/ConstantEvaluationStringBufferAppend02-WithEmptyString/test3.desc new file mode 100644 index 00000000000..958b46c5537 --- /dev/null +++ b/jbmc/regression/jbmc-strings/ConstantEvaluationStringBufferAppend02-WithEmptyString/test3.desc @@ -0,0 +1,9 @@ +CORE +Main.class +--function Main.test3 --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/ConstantEvaluationStringBufferAppend03/Test.class b/jbmc/regression/jbmc-strings/ConstantEvaluationStringBufferAppend03/Test.class new file mode 100644 index 00000000000..dfc34ee703a Binary files /dev/null and b/jbmc/regression/jbmc-strings/ConstantEvaluationStringBufferAppend03/Test.class differ diff --git a/jbmc/regression/jbmc-strings/ConstantEvaluationStringBufferAppend03/Test.java b/jbmc/regression/jbmc-strings/ConstantEvaluationStringBufferAppend03/Test.java new file mode 100644 index 00000000000..088063bcb6f --- /dev/null +++ b/jbmc/regression/jbmc-strings/ConstantEvaluationStringBufferAppend03/Test.java @@ -0,0 +1,75 @@ +class Test { + public void testBooleanSuccess() { + StringBuffer sb = new StringBuffer("abc"); + sb.append(true); + assert sb.toString().equals("abctrue"); + } + + public void testCharSuccess() { + StringBuffer sb = new StringBuffer("abc"); + sb.append('a'); + assert sb.toString().equals("abca"); + } + + public void testIntSuccess() { + StringBuffer sb = new StringBuffer("abc"); + sb.append(3); + assert sb.toString().equals("abc3"); + } + + public void testLongSuccess() { + StringBuffer sb = new StringBuffer("abc"); + sb.append(3L); + assert sb.toString().equals("abc3"); + } + + public void testCharSequenceSuccess() { + StringBuffer sb = new StringBuffer("abc"); + CharSequence cs = "xyz"; + sb.append(cs); + assert sb.toString().equals("abcxyz"); + } + + public void testStringBufferSuccess() { + StringBuffer sb = new StringBuffer("abc"); + StringBuffer buf = new StringBuffer("xyz"); + sb.append(buf); + assert sb.toString().equals("abcxyz"); + } + + public void testBooleanNoPropagation(boolean b) { + StringBuffer sb = new StringBuffer("abc"); + sb.append(b); + assert sb.toString().equals("abctrue"); + } + + public void testCharNoPropagation(char c) { + StringBuffer sb = new StringBuffer("abc"); + sb.append(c); + assert sb.toString().equals("abca"); + } + + public void testIntNoPropagation(int i) { + StringBuffer sb = new StringBuffer("abc"); + sb.append(i); + assert sb.toString().equals("abc3"); + } + + public void testLongNoPropagation(long l) { + StringBuffer sb = new StringBuffer("abc"); + sb.append(l); + assert sb.toString().equals("abc3"); + } + + public void testCharSequenceNoPropagation(CharSequence cs) { + StringBuffer sb = new StringBuffer("abc"); + sb.append(cs); + assert sb.toString().equals("abcxyz"); + } + + public void testStringBufferNoPropagation(StringBuffer buf) { + StringBuffer sb = new StringBuffer("abc"); + sb.append(buf); + assert sb.toString().equals("abcxyz"); + } +} diff --git a/jbmc/regression/jbmc-strings/ConstantEvaluationStringBufferAppend03/test_bool_no_propagation.desc b/jbmc/regression/jbmc-strings/ConstantEvaluationStringBufferAppend03/test_bool_no_propagation.desc new file mode 100644 index 00000000000..9c35cb09102 --- /dev/null +++ b/jbmc/regression/jbmc-strings/ConstantEvaluationStringBufferAppend03/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/ConstantEvaluationStringBufferAppend03/test_bool_success.desc b/jbmc/regression/jbmc-strings/ConstantEvaluationStringBufferAppend03/test_bool_success.desc new file mode 100644 index 00000000000..a608f0f7e9b --- /dev/null +++ b/jbmc/regression/jbmc-strings/ConstantEvaluationStringBufferAppend03/test_bool_success.desc @@ -0,0 +1,9 @@ +FUTURE +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/ConstantEvaluationStringBufferAppend03/test_char_no_propagation.desc b/jbmc/regression/jbmc-strings/ConstantEvaluationStringBufferAppend03/test_char_no_propagation.desc new file mode 100644 index 00000000000..d6e618d4b3f --- /dev/null +++ b/jbmc/regression/jbmc-strings/ConstantEvaluationStringBufferAppend03/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/ConstantEvaluationStringBufferAppend03/test_char_sequence_no_propagation.desc b/jbmc/regression/jbmc-strings/ConstantEvaluationStringBufferAppend03/test_char_sequence_no_propagation.desc new file mode 100644 index 00000000000..a5125e01caf --- /dev/null +++ b/jbmc/regression/jbmc-strings/ConstantEvaluationStringBufferAppend03/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/ConstantEvaluationStringBufferAppend03/test_char_sequence_success.desc b/jbmc/regression/jbmc-strings/ConstantEvaluationStringBufferAppend03/test_char_sequence_success.desc new file mode 100644 index 00000000000..b11ca109df3 --- /dev/null +++ b/jbmc/regression/jbmc-strings/ConstantEvaluationStringBufferAppend03/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/ConstantEvaluationStringBufferAppend03/test_char_success.desc b/jbmc/regression/jbmc-strings/ConstantEvaluationStringBufferAppend03/test_char_success.desc new file mode 100644 index 00000000000..6de73b74075 --- /dev/null +++ b/jbmc/regression/jbmc-strings/ConstantEvaluationStringBufferAppend03/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/ConstantEvaluationStringBufferAppend03/test_int_no_propagation.desc b/jbmc/regression/jbmc-strings/ConstantEvaluationStringBufferAppend03/test_int_no_propagation.desc new file mode 100644 index 00000000000..2428805c10d --- /dev/null +++ b/jbmc/regression/jbmc-strings/ConstantEvaluationStringBufferAppend03/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/ConstantEvaluationStringBufferAppend03/test_int_success.desc b/jbmc/regression/jbmc-strings/ConstantEvaluationStringBufferAppend03/test_int_success.desc new file mode 100644 index 00000000000..4c3745a29b9 --- /dev/null +++ b/jbmc/regression/jbmc-strings/ConstantEvaluationStringBufferAppend03/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/ConstantEvaluationStringBufferAppend03/test_long_no_propagation.desc b/jbmc/regression/jbmc-strings/ConstantEvaluationStringBufferAppend03/test_long_no_propagation.desc new file mode 100644 index 00000000000..62dc3085ffa --- /dev/null +++ b/jbmc/regression/jbmc-strings/ConstantEvaluationStringBufferAppend03/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/ConstantEvaluationStringBufferAppend03/test_long_success.desc b/jbmc/regression/jbmc-strings/ConstantEvaluationStringBufferAppend03/test_long_success.desc new file mode 100644 index 00000000000..f87766b30b8 --- /dev/null +++ b/jbmc/regression/jbmc-strings/ConstantEvaluationStringBufferAppend03/test_long_success.desc @@ -0,0 +1,9 @@ +FUTURE +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/ConstantEvaluationStringBufferAppend03/test_string_buffer_no_propagation.desc b/jbmc/regression/jbmc-strings/ConstantEvaluationStringBufferAppend03/test_string_buffer_no_propagation.desc new file mode 100644 index 00000000000..67fb56823d5 --- /dev/null +++ b/jbmc/regression/jbmc-strings/ConstantEvaluationStringBufferAppend03/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/ConstantEvaluationStringBufferAppend03/test_string_buffer_success.desc b/jbmc/regression/jbmc-strings/ConstantEvaluationStringBufferAppend03/test_string_buffer_success.desc new file mode 100644 index 00000000000..26960274e80 --- /dev/null +++ b/jbmc/regression/jbmc-strings/ConstantEvaluationStringBufferAppend03/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$ +-- +-- diff --git a/jbmc/src/java_bytecode/java_string_library_preprocess.cpp b/jbmc/src/java_bytecode/java_string_library_preprocess.cpp index 5b981a8d47e..e34d4d4ba22 100644 --- a/jbmc/src/java_bytecode/java_string_library_preprocess.cpp +++ b/jbmc/src/java_bytecode/java_string_library_preprocess.cpp @@ -1752,9 +1752,6 @@ void java_string_library_preprocesst::initialize_conversion_table() cprover_equivalent_to_java_assign_and_return_function ["java::java.lang.StringBuffer.append:(C)Ljava/lang/StringBuffer;"]= ID_cprover_string_concat_char_func; - cprover_equivalent_to_java_assign_and_return_function - ["java::java.lang.StringBuffer.append:(J)Ljava/lang/StringBuffer;"]= - ID_cprover_string_concat_long_func; cprover_equivalent_to_java_assign_and_return_function ["java::java.lang.StringBuffer.append:(Ljava/lang/String;)" "Ljava/lang/StringBuffer;"]= diff --git a/src/util/irep_ids.def b/src/util/irep_ids.def index 8988b345747..66a21f73ed9 100644 --- a/src/util/irep_ids.def +++ b/src/util/irep_ids.def @@ -596,7 +596,6 @@ IREP_ID_ONE(cprover_string_code_point_count_func) IREP_ID_ONE(cprover_string_offset_by_code_point_func) IREP_ID_ONE(cprover_string_compare_to_func) IREP_ID_ONE(cprover_string_concat_func) -IREP_ID_ONE(cprover_string_concat_long_func) IREP_ID_ONE(cprover_string_concat_char_func) IREP_ID_ONE(cprover_string_concat_code_point_func) IREP_ID_ONE(cprover_string_constrain_characters_func)