From 5889579c2970c1e0c1ef00ef86da8fbef1e0c156 Mon Sep 17 00:00:00 2001 From: Daniel Poetzl Date: Fri, 20 Sep 2019 11:36:45 +0100 Subject: [PATCH 1/2] Add tests for constant propagation of StringBuilder.append(Object) --- .../Test.class | Bin 0 -> 1134 bytes .../Test.java | 22 ++++++++++++++++++ .../test_no_propagation.desc | 9 +++++++ .../test_success.desc | 9 +++++++ 4 files changed, 40 insertions(+) create mode 100644 jbmc/regression/jbmc-strings/ConstantEvaluationStringBuilderAppend04-Object/Test.class create mode 100644 jbmc/regression/jbmc-strings/ConstantEvaluationStringBuilderAppend04-Object/Test.java create mode 100644 jbmc/regression/jbmc-strings/ConstantEvaluationStringBuilderAppend04-Object/test_no_propagation.desc create mode 100644 jbmc/regression/jbmc-strings/ConstantEvaluationStringBuilderAppend04-Object/test_success.desc diff --git a/jbmc/regression/jbmc-strings/ConstantEvaluationStringBuilderAppend04-Object/Test.class b/jbmc/regression/jbmc-strings/ConstantEvaluationStringBuilderAppend04-Object/Test.class new file mode 100644 index 0000000000000000000000000000000000000000..281da1a9a173fb046769a559513f41805326faf5 GIT binary patch literal 1134 zcmZ`&X-^YT6g{uoOs7){ZCPB9)mkWv3T}YxU`Qxx+Gyb0bo$Z^jx%)@qy7~BfS=W* zO(ao2`k4vu8hZ?7CLdL^Foo{O+OlR+}|7t2X#XWQ8bd5bn~>cQnGzV=i7$p z6E9PZ8F59$6-m#}>ukz5l=<349PGP9w`VO$JaYK~%z~iY;t2bhk^L zsO*q_!aa~4$?pgUVp_eslX5Acr>+E0g@i0mFCx*uyIRxC_4Aiewy`3U`m2I6U@ zfy5CK$58j1NPaJ*yE*`=4gl-OcVEm4YN3Ey4snX3P>5s(5^13?i*^f0po}CA&;<`E z+#pmE;oqQ18j>(PJVa_nFiNWs{+!AQHDf|e6FtQi`E)w-zusNJl?-*vQlZ|UhYa=$ uqtt^=$69912L=K?>1+eNN01^P5ea{R+!k`?u^<{nNL>|nkJBcEn|}dPp6WjU literal 0 HcmV?d00001 diff --git a/jbmc/regression/jbmc-strings/ConstantEvaluationStringBuilderAppend04-Object/Test.java b/jbmc/regression/jbmc-strings/ConstantEvaluationStringBuilderAppend04-Object/Test.java new file mode 100644 index 0000000000..d15ea03fdf --- /dev/null +++ b/jbmc/regression/jbmc-strings/ConstantEvaluationStringBuilderAppend04-Object/Test.java @@ -0,0 +1,22 @@ +public class Test +{ + public void testSuccess() + { + StringBuilder sb = new StringBuilder("abc"); + Integer i = new Integer(3); + sb.append(i); + assert sb.toString().equals("abc3"); + + sb.append((Object)"xyz"); + assert sb.toString().equals("abc3xyz"); + + sb.append((Object)null); + assert sb.toString().equals("abc3xyznull"); + } + + public void testNoPropagation(Object obj) + { + StringBuilder sb = new StringBuilder(); + assert obj.toString().equals(""); + } +} diff --git a/jbmc/regression/jbmc-strings/ConstantEvaluationStringBuilderAppend04-Object/test_no_propagation.desc b/jbmc/regression/jbmc-strings/ConstantEvaluationStringBuilderAppend04-Object/test_no_propagation.desc new file mode 100644 index 0000000000..139f500f8c --- /dev/null +++ b/jbmc/regression/jbmc-strings/ConstantEvaluationStringBuilderAppend04-Object/test_no_propagation.desc @@ -0,0 +1,9 @@ +CORE symex-driven-lazy-loading-expected-failure +Test.class +--function Test.testNoPropagation --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` --property 'java::Test.testNoPropagation:(Ljava/lang/Object;)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/ConstantEvaluationStringBuilderAppend04-Object/test_success.desc b/jbmc/regression/jbmc-strings/ConstantEvaluationStringBuilderAppend04-Object/test_success.desc new file mode 100644 index 0000000000..8d1b5b06f4 --- /dev/null +++ b/jbmc/regression/jbmc-strings/ConstantEvaluationStringBuilderAppend04-Object/test_success.desc @@ -0,0 +1,9 @@ +CORE +Test.class +--function Test.testSuccess --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$ +-- +-- From 906c2f3945f9b78b4ed5d61dc84d12bcd336676f Mon Sep 17 00:00:00 2001 From: Daniel Poetzl Date: Fri, 20 Sep 2019 11:39:39 +0100 Subject: [PATCH 2/2] Add tests for constant propagation of StringBuffer.append(Object) --- .../Test.class | Bin 0 -> 1132 bytes .../Test.java | 22 ++++++++++++++++++ .../test_no_propagation.desc | 9 +++++++ .../test_success.desc | 9 +++++++ 4 files changed, 40 insertions(+) create mode 100644 jbmc/regression/jbmc-strings/ConstantEvaluationStringBufferAppend04-Object/Test.class create mode 100644 jbmc/regression/jbmc-strings/ConstantEvaluationStringBufferAppend04-Object/Test.java create mode 100644 jbmc/regression/jbmc-strings/ConstantEvaluationStringBufferAppend04-Object/test_no_propagation.desc create mode 100644 jbmc/regression/jbmc-strings/ConstantEvaluationStringBufferAppend04-Object/test_success.desc diff --git a/jbmc/regression/jbmc-strings/ConstantEvaluationStringBufferAppend04-Object/Test.class b/jbmc/regression/jbmc-strings/ConstantEvaluationStringBufferAppend04-Object/Test.class new file mode 100644 index 0000000000000000000000000000000000000000..a0531eb3efc7a2e46efa8a26c627c54dc3379dc7 GIT binary patch literal 1132 zcmZ`&YflqF6g|_|Zns+sZF%@Wp4LJURPY7J8w?3WO&bk-+ir(uaow%^FzQd?5BOP4 z+C&odv%g7=cNS=|Vwz0v%sq4OIcM(v`2FQ8fH^!?(1)Ca8#3|=LYR;+sUV7i*i6Nd z#Z3`S%a~Dc3%4cQQJ^9xV^+qTjJqP66GaGePr`i#5AaaJJVRz&b6xIuhHbeUhO1Rf zUS(kW46#MSGQ1^*aDL)BLuB2qa)#87Vewu6RfRic0cJ>e-1SPnu5;IANR~WJe_7P( zL6#^JRfZmc*|ncKc3rD!q8USPe&CJSA+X*u)k?ce~Vy z$PVQv)C1*_{I)P4rq%1*qF0!@$f0wlomWj-WzRl2VaVnu{=pIA9G5d>jKB6ZlOFEE z=b$l2wfV1`G%MtLmAi(+t1V~f$vvMEG${KRp=s=+sb$>*!e5FaWC}ePtygF_NdM#$ zqLWRqj{=CRw8nx%ks544zavaPz&}Q4FCA_ovU7~+UaW~&u`tzu^x_lbBlH&HwrV0IVb5{dZna3kB42h*KPeLL@VgNDF;ew3|l)WhAkWE_g`c z8ljR1{{jutkc8pkAyPAfQCfxYXH-t8853%n=qa|yr_-7L_3jF;WT<173iSp(WU!wY tr5WZ*?oHij`{{tv`>0