From f53a598fb370f1c3a83c793953eb276607255ea2 Mon Sep 17 00:00:00 2001 From: Daniel Poetzl Date: Wed, 18 Sep 2019 13:55:34 +0100 Subject: [PATCH 1/2] Remove ID of unimplemented string function The string function with ID_cprover_string_concat_long_func was unimplemented and will be obsolete when the functionality is handled by a model. --- jbmc/src/java_bytecode/java_string_library_preprocess.cpp | 3 --- src/util/irep_ids.def | 1 - 2 files changed, 4 deletions(-) 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) From 6155f2a1ab98910c70b418f4b6283e0e95a459b0 Mon Sep 17 00:00:00 2001 From: Daniel Poetzl Date: Wed, 18 Sep 2019 13:58:07 +0100 Subject: [PATCH 2/2] Add regression tests for constant propagation of StringBuffer.append() --- .../Main.class | Bin 0 -> 801 bytes .../Main.java | 7 ++ .../test.desc | 9 +++ .../Main.class | Bin 0 -> 1050 bytes .../Main.java | 22 +++++ .../test1.desc | 9 +++ .../test2.desc | 9 +++ .../test3.desc | 9 +++ .../Test.class | Bin 0 -> 2675 bytes .../Test.java | 75 ++++++++++++++++++ .../test_bool_no_propagation.desc | 9 +++ .../test_bool_success.desc | 9 +++ .../test_char_no_propagation.desc | 9 +++ .../test_char_sequence_no_propagation.desc | 9 +++ .../test_char_sequence_success.desc | 9 +++ .../test_char_success.desc | 9 +++ .../test_int_no_propagation.desc | 9 +++ .../test_int_success.desc | 9 +++ .../test_long_no_propagation.desc | 9 +++ .../test_long_success.desc | 9 +++ .../test_string_buffer_no_propagation.desc | 9 +++ .../test_string_buffer_success.desc | 9 +++ 22 files changed, 248 insertions(+) create mode 100644 jbmc/regression/jbmc-strings/ConstantEvaluationStringBufferAppend01/Main.class create mode 100644 jbmc/regression/jbmc-strings/ConstantEvaluationStringBufferAppend01/Main.java create mode 100644 jbmc/regression/jbmc-strings/ConstantEvaluationStringBufferAppend01/test.desc create mode 100644 jbmc/regression/jbmc-strings/ConstantEvaluationStringBufferAppend02-WithEmptyString/Main.class create mode 100644 jbmc/regression/jbmc-strings/ConstantEvaluationStringBufferAppend02-WithEmptyString/Main.java create mode 100644 jbmc/regression/jbmc-strings/ConstantEvaluationStringBufferAppend02-WithEmptyString/test1.desc create mode 100644 jbmc/regression/jbmc-strings/ConstantEvaluationStringBufferAppend02-WithEmptyString/test2.desc create mode 100644 jbmc/regression/jbmc-strings/ConstantEvaluationStringBufferAppend02-WithEmptyString/test3.desc create mode 100644 jbmc/regression/jbmc-strings/ConstantEvaluationStringBufferAppend03/Test.class create mode 100644 jbmc/regression/jbmc-strings/ConstantEvaluationStringBufferAppend03/Test.java create mode 100644 jbmc/regression/jbmc-strings/ConstantEvaluationStringBufferAppend03/test_bool_no_propagation.desc create mode 100644 jbmc/regression/jbmc-strings/ConstantEvaluationStringBufferAppend03/test_bool_success.desc create mode 100644 jbmc/regression/jbmc-strings/ConstantEvaluationStringBufferAppend03/test_char_no_propagation.desc create mode 100644 jbmc/regression/jbmc-strings/ConstantEvaluationStringBufferAppend03/test_char_sequence_no_propagation.desc create mode 100644 jbmc/regression/jbmc-strings/ConstantEvaluationStringBufferAppend03/test_char_sequence_success.desc create mode 100644 jbmc/regression/jbmc-strings/ConstantEvaluationStringBufferAppend03/test_char_success.desc create mode 100644 jbmc/regression/jbmc-strings/ConstantEvaluationStringBufferAppend03/test_int_no_propagation.desc create mode 100644 jbmc/regression/jbmc-strings/ConstantEvaluationStringBufferAppend03/test_int_success.desc create mode 100644 jbmc/regression/jbmc-strings/ConstantEvaluationStringBufferAppend03/test_long_no_propagation.desc create mode 100644 jbmc/regression/jbmc-strings/ConstantEvaluationStringBufferAppend03/test_long_success.desc create mode 100644 jbmc/regression/jbmc-strings/ConstantEvaluationStringBufferAppend03/test_string_buffer_no_propagation.desc create mode 100644 jbmc/regression/jbmc-strings/ConstantEvaluationStringBufferAppend03/test_string_buffer_success.desc diff --git a/jbmc/regression/jbmc-strings/ConstantEvaluationStringBufferAppend01/Main.class b/jbmc/regression/jbmc-strings/ConstantEvaluationStringBufferAppend01/Main.class new file mode 100644 index 0000000000000000000000000000000000000000..39f7f4e104d5ee0f373222eff1cb0cddf334e298 GIT binary patch literal 801 zcmZuvO>fgc5Pcgvw&OS?algVxfkJ_#4h5`9TFqTWoLHg?VC3<`{UQwZvdLOW1@&NI#vywHIczN1Lvh(%b|b^ z(z|G2-NYqa)^Wu|UV^J8YS_@>Ff6R|C=y}p^@Hf47xAtydJJrjLEG{IFTTs5RBO)} z)a`yxFcjNfAf60gcSZP2f+-P;C}t>hV(z}$;e#Yhf*6b~*Z;#|cKXB66^}jnBDcf6 zVDpf_I;q&02(TPJZICwDJ-xnd3=3Q4}>g2wA|G~mlY+5LxY@vZ`q>=Iz z*Kys#4cug?q)hi`eLV`pK5?nCs*a|GTe!_oN|8^yhr*>6ma6SEI2F>8t!sQR5CM&) z{y)I6H&gK~>ObyJSr`_pwPQF!{3T+B)Wn-1_oIK*OeMBzw3lM4aoeZm(fE2I@mIe v7+^o)=%|o)a$c*M)CbCTVT=T^-li=75AjN literal 0 HcmV?d00001 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 0000000000000000000000000000000000000000..abf6e6d8882245011abf9c459c3d74c8092fe293 GIT binary patch literal 1050 zcmb7?TW=CU6vzJq?1g11uw06lTB}u|-0a0$XpCC*3G@M@Y2Ox@lC8Ml?&62x3;3)i zkk~}u{Z1OsaN8(NlV+2hnKS=6zcc?czy5sx0bmc0G{ms3;JS(p4FTLxaZ`+&VMK9D z%x-JAgPelA1`X>XLh>yQ1r!yO7?PW&>vG4ldba!Aa?NI!w;9+GgS>CqmiL$;n9ILq z2p#m=oFP`TZ2oHSp~;;$Ld+m}-1W8@q7Bb%y|0`7Nt|j@P@e7X%*I^?b-&e}<<%O! zfz#qIEs-T$H!Zt-Vtz7p7)UZ?#Jtiq?M|iPIhNgdHaI@!4wYjzTS8M|fR4M^))7ZS z#}0OhsFN%A7_$E9r}O*0aGV~U4+)Zj`#K)rAw%3(zHXlImiJF+ie^aXYQAn7tO{3T zv)|`7IaWMNuykg6hbr0N_2#Klx%`rj6f*xfFuU%5=xK@7JoP8$7j)32CX!`s?ph9S zFK$d7@dmU(9X!GYJ&72-8WztA!)PXf39sp&qSYFWWGSSrG1wO&M4JBcBq+8r3uy;I z`hfB&0*6L$j8M&x>V@J6^1H84hFC3(pc=su!b3z(p&gD9`6+S+COI>N24&C?qM{_q zE29Jjs}zlZ{YFVaR>38LUS2>s9Tw1{fR3TpjNpZl8dL&A=-ng;T)>KtEG&>$&Ox4W zOX>VuCJ1Q|GD*l3A=Ar96;~I?y@}mG!ibKrGK3QPj8O0!6yLphM}%7v0{RotoHbem GaP2RxpTe2| literal 0 HcmV?d00001 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 0000000000000000000000000000000000000000..dfc34ee703ae3add1c6d34afe5e252f7a4abb3ee GIT binary patch literal 2675 zcmb7_eN!7%6vm%RUUmrqLU>7PtbL<3kOb@tEgDJ-p)bKeYlE$zZC%1Prp66!HjesH z_yYc|&V(5|qyPJv)bY8S&F(_l(1u~}%{}Ly-#zC%d-L~yfBXsH8ng&bVNt=yDn5x| z0D1XX8bks&?>39g9RxlC^(5z4<@`%Be*EcYIsJ+<iK&_apGmQS&oQI+ZT;#_EWb5mV`6U+a1w>lJ^x{z~NEcGHmp z^w~7(HK9=FZNVPw>CKv{@3}qa+itaJ;8n4Mv%IHH@%9n1q!bTlBmAf6An*Zaauggx zvxgABaw2es&#=8HO=n%#rwH)I0y3{KupJK^B3Q}<+Xy}R4dDYMGHobvwT;08481~R z`w&Ba$$$fPz&L`O2Y5jS5km;GM4aP_3h@tS6`UvPf{S|Qpt3$xOlu?RXASpf4U!eX z7>1BR)MI5jtZA3^y0pS=jQCNb{ZXR?#rQYIwBjDhN$aAEdhVo^^QAR`SR3(ofK3uM zMN9%&Bt2NRlh-8|RwXRJ3eS14`1nR9+s1^SHuhfDyHLY{E_hITHcqwJ?5THPpC|hQCNNFqUgR(FC69g0W=qk`u;v{p%SOtC zJ$-IuQ=UGV_=)La2q6LqBrmBUI8W%5OtlX8$>PkpyqiDFDv<$dIj9fo$p@+mUizZCLVO$4J)-UtRU~Tt7)r&0tA2@;pRstNjpPB8 f;4cUUen;552fG)me2YRDh~AcW>~($_z>WU_aE}@E literal 0 HcmV?d00001 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$ +-- +--