From 89e46c8aa7b5d0a39939c66aea06d4157e035c6b Mon Sep 17 00:00:00 2001 From: Peter Schrammel Date: Tue, 31 Dec 2024 14:32:18 +0100 Subject: [PATCH 01/47] Compile jbmc/aastore_aaload1 test sources --- jbmc/regression/jbmc/aastore_aaload1/A.class | Bin 229 -> 0 bytes .../aastore_aaload1/aastore_aaload1.class | Bin 626 -> 0 bytes jbmc/regression/jbmc/aastore_aaload1/pom.xml | 30 ++++++++++++++++++ .../{ => src/main/java}/aastore_aaload1.java | 0 .../regression/jbmc/aastore_aaload1/test.desc | 2 +- jbmc/regression/jbmc/pom.xml | 1 + 6 files changed, 32 insertions(+), 1 deletion(-) delete mode 100644 jbmc/regression/jbmc/aastore_aaload1/A.class delete mode 100644 jbmc/regression/jbmc/aastore_aaload1/aastore_aaload1.class create mode 100644 jbmc/regression/jbmc/aastore_aaload1/pom.xml rename jbmc/regression/jbmc/aastore_aaload1/{ => src/main/java}/aastore_aaload1.java (100%) diff --git a/jbmc/regression/jbmc/aastore_aaload1/A.class b/jbmc/regression/jbmc/aastore_aaload1/A.class deleted file mode 100644 index 058d5ef9984c195fbb70daeb679d1517647c35fb..0000000000000000000000000000000000000000 GIT binary patch literal 0 HcmV?d00001 literal 229 zcmXX=-wMHS6#mXO#?LV20bB_eq+Ci#DJ3q*t69oGlmUbiRM5 z@AG}V0gTX4uuv_-M9oIshD#{iI7l^t7KGy15B+39Fgx8H!J0)!QR+)S)T{L3>3GXt zAdK2XX?)OgKLbtXYZAqJ&m2U29QMzAV+S@$4hksB=PAL>$U(s2X|VRr`jDU{B`hgL lGGhB*k`ksYs0}06RPPDunGYEE+@oYG(XynKdn$4paDM2}CJz7r diff --git a/jbmc/regression/jbmc/aastore_aaload1/aastore_aaload1.class b/jbmc/regression/jbmc/aastore_aaload1/aastore_aaload1.class deleted file mode 100644 index 748e45b414bf2f76c572247e24323ccc878ca0b9..0000000000000000000000000000000000000000 GIT binary patch literal 0 HcmV?d00001 literal 626 zcmZ9K&rZ}(6vn^XcIM8M0yBUxI2I8|M1vBQ9TVaNbv5W>jES%?ccwSwVrfm=F+PA# z!O{(DHIYQ3E=_y{AH@aw-BFmtH0?b(f4=iOr}xL%=dS=ZuG5y4N{Suhn|2lKu5=k(p$F(-w|*3)O$Qqh1a3C9VooTK)K+xZh0& zSzkXgR%%A6yhtShR<~v+p3s2!ZKY`o*0PhI( zweaqDjGdxHU-{cxR~-NTX_cL!@&bWCU6(i&f=m)+p8B_F-($BaMknB&!50$KV(Ay} pKm{`wz#Bs{pgtu(p>hQ29m8`!!W*?XhqqECIKh28;-w+M>>pjeb&3E0 diff --git a/jbmc/regression/jbmc/aastore_aaload1/pom.xml b/jbmc/regression/jbmc/aastore_aaload1/pom.xml new file mode 100644 index 00000000000..ec4f700c59d --- /dev/null +++ b/jbmc/regression/jbmc/aastore_aaload1/pom.xml @@ -0,0 +1,30 @@ + + + 4.0.0 + org.cprover.regression + regression.jbmc.aastore_aaload1 + 1.0-SNAPSHOT + + + org.cprover.regression + regression.jbmc + 1.0-SNAPSHOT + + + + + + maven-jar-plugin + + + default-jar + none + + + + + + + diff --git a/jbmc/regression/jbmc/aastore_aaload1/aastore_aaload1.java b/jbmc/regression/jbmc/aastore_aaload1/src/main/java/aastore_aaload1.java similarity index 100% rename from jbmc/regression/jbmc/aastore_aaload1/aastore_aaload1.java rename to jbmc/regression/jbmc/aastore_aaload1/src/main/java/aastore_aaload1.java diff --git a/jbmc/regression/jbmc/aastore_aaload1/test.desc b/jbmc/regression/jbmc/aastore_aaload1/test.desc index a5c1145917e..f5ce48e69f5 100644 --- a/jbmc/regression/jbmc/aastore_aaload1/test.desc +++ b/jbmc/regression/jbmc/aastore_aaload1/test.desc @@ -1,6 +1,6 @@ CORE aastore_aaload1 - +-cp target/classes ^EXIT=0$ ^SIGNAL=0$ ^VERIFICATION SUCCESSFUL$ diff --git a/jbmc/regression/jbmc/pom.xml b/jbmc/regression/jbmc/pom.xml index 9452e36ad45..a254dce70f8 100644 --- a/jbmc/regression/jbmc/pom.xml +++ b/jbmc/regression/jbmc/pom.xml @@ -15,6 +15,7 @@ + aastore_aaload1 ArithmeticException1 classpath-jar-load-whole-jar From 8156b37e4b26b70fdbd3782b7dae78fdefb7a9cb Mon Sep 17 00:00:00 2001 From: Peter Schrammel Date: Thu, 2 Jan 2025 11:37:03 +0100 Subject: [PATCH 02/47] Compile jbmc/address_space_size_limit1 test sources --- .../jbmc/address_space_size_limit1/Test.class | Bin 640 -> 0 bytes .../jbmc/address_space_size_limit1/pom.xml | 30 ++++++++++++++++++ .../{ => src/main/java}/Test.java | 0 .../jbmc/address_space_size_limit1/test.desc | 2 +- jbmc/regression/jbmc/pom.xml | 1 + 5 files changed, 32 insertions(+), 1 deletion(-) delete mode 100644 jbmc/regression/jbmc/address_space_size_limit1/Test.class create mode 100644 jbmc/regression/jbmc/address_space_size_limit1/pom.xml rename jbmc/regression/jbmc/address_space_size_limit1/{ => src/main/java}/Test.java (100%) diff --git a/jbmc/regression/jbmc/address_space_size_limit1/Test.class b/jbmc/regression/jbmc/address_space_size_limit1/Test.class deleted file mode 100644 index 5f81fc826ffa983a71fe170b00828a9d1b6ffa96..0000000000000000000000000000000000000000 GIT binary patch literal 0 HcmV?d00001 literal 640 zcmYL{T~8B16o%ikv)yU83zV<6bhQW~Rzf5(B%06|3~EAB0_ylDXEFn+4zpw(3!t{f1Yx(;>nm|)ko@4e)()$1t2 zL_>$_MgO#=qCKPL!fBvGLa}z(I1XM1Yuz9`T5Bee4v#j>#j$1*v`=<|SE*j&HX&PY zcZYOQGa9$q>ql+%TpM6+PsPc7!}2hWk_Q)gZey}0G2y|(7@<7s_T=9T&!VUoNi2D| zgJnWtB-w2pt9C+=hYbVT;7LZstuDU;kI+%Ej#TGAj-4lcF0jc1EbvR__?azU>=R}vkuiqncfmwf5JopIf4f0oT_6LyP4c$uV73PE44*MHtZ*v^ydH0aL z&2S|T@e^5+m@Sr&MG>W;h4s`HFgYbYBYOd9U&0n2kQuT6I;WJAf#q%TUxISldhQRu C&~X6( diff --git a/jbmc/regression/jbmc/address_space_size_limit1/pom.xml b/jbmc/regression/jbmc/address_space_size_limit1/pom.xml new file mode 100644 index 00000000000..0ad08f62a67 --- /dev/null +++ b/jbmc/regression/jbmc/address_space_size_limit1/pom.xml @@ -0,0 +1,30 @@ + + + 4.0.0 + org.cprover.regression + regression.jbmc.address_space_size_limit1 + 1.0-SNAPSHOT + + + org.cprover.regression + regression.jbmc + 1.0-SNAPSHOT + + + + + + maven-jar-plugin + + + default-jar + none + + + + + + + diff --git a/jbmc/regression/jbmc/address_space_size_limit1/Test.java b/jbmc/regression/jbmc/address_space_size_limit1/src/main/java/Test.java similarity index 100% rename from jbmc/regression/jbmc/address_space_size_limit1/Test.java rename to jbmc/regression/jbmc/address_space_size_limit1/src/main/java/Test.java diff --git a/jbmc/regression/jbmc/address_space_size_limit1/test.desc b/jbmc/regression/jbmc/address_space_size_limit1/test.desc index a9bb6c1ed0a..88299880103 100644 --- a/jbmc/regression/jbmc/address_space_size_limit1/test.desc +++ b/jbmc/regression/jbmc/address_space_size_limit1/test.desc @@ -1,6 +1,6 @@ CORE Test ---object-bits 4 +--object-bits 4 --cp target/classes too many addressed objects ^EXIT=6$ ^SIGNAL=0$ diff --git a/jbmc/regression/jbmc/pom.xml b/jbmc/regression/jbmc/pom.xml index a254dce70f8..d91567a11fc 100644 --- a/jbmc/regression/jbmc/pom.xml +++ b/jbmc/regression/jbmc/pom.xml @@ -16,6 +16,7 @@ aastore_aaload1 + address_space_size_limit1 ArithmeticException1 classpath-jar-load-whole-jar From 4f2abc52598b41d6b4a3e0f2de1a29a0ab2da44a Mon Sep 17 00:00:00 2001 From: Peter Schrammel Date: Thu, 2 Jan 2025 11:38:02 +0100 Subject: [PATCH 03/47] Compile jbmc/address_space_size_limit2 test sources --- .../jbmc/address_space_size_limit2/Test.class | Bin 640 -> 0 bytes .../jbmc/address_space_size_limit2/pom.xml | 30 ++++++++++++++++++ .../{ => src/main/java}/Test.java | 0 .../jbmc/address_space_size_limit2/test.desc | 2 +- jbmc/regression/jbmc/pom.xml | 1 + 5 files changed, 32 insertions(+), 1 deletion(-) delete mode 100644 jbmc/regression/jbmc/address_space_size_limit2/Test.class create mode 100644 jbmc/regression/jbmc/address_space_size_limit2/pom.xml rename jbmc/regression/jbmc/address_space_size_limit2/{ => src/main/java}/Test.java (100%) diff --git a/jbmc/regression/jbmc/address_space_size_limit2/Test.class b/jbmc/regression/jbmc/address_space_size_limit2/Test.class deleted file mode 100644 index 5f81fc826ffa983a71fe170b00828a9d1b6ffa96..0000000000000000000000000000000000000000 GIT binary patch literal 0 HcmV?d00001 literal 640 zcmYL{T~8B16o%ikv)yU83zV<6bhQW~Rzf5(B%06|3~EAB0_ylDXEFn+4zpw(3!t{f1Yx(;>nm|)ko@4e)()$1t2 zL_>$_MgO#=qCKPL!fBvGLa}z(I1XM1Yuz9`T5Bee4v#j>#j$1*v`=<|SE*j&HX&PY zcZYOQGa9$q>ql+%TpM6+PsPc7!}2hWk_Q)gZey}0G2y|(7@<7s_T=9T&!VUoNi2D| zgJnWtB-w2pt9C+=hYbVT;7LZstuDU;kI+%Ej#TGAj-4lcF0jc1EbvR__?azU>=R}vkuiqncfmwf5JopIf4f0oT_6LyP4c$uV73PE44*MHtZ*v^ydH0aL z&2S|T@e^5+m@Sr&MG>W;h4s`HFgYbYBYOd9U&0n2kQuT6I;WJAf#q%TUxISldhQRu C&~X6( diff --git a/jbmc/regression/jbmc/address_space_size_limit2/pom.xml b/jbmc/regression/jbmc/address_space_size_limit2/pom.xml new file mode 100644 index 00000000000..41309e373ea --- /dev/null +++ b/jbmc/regression/jbmc/address_space_size_limit2/pom.xml @@ -0,0 +1,30 @@ + + + 4.0.0 + org.cprover.regression + regression.jbmc.address_space_size_limit2 + 1.0-SNAPSHOT + + + org.cprover.regression + regression.jbmc + 1.0-SNAPSHOT + + + + + + maven-jar-plugin + + + default-jar + none + + + + + + + diff --git a/jbmc/regression/jbmc/address_space_size_limit2/Test.java b/jbmc/regression/jbmc/address_space_size_limit2/src/main/java/Test.java similarity index 100% rename from jbmc/regression/jbmc/address_space_size_limit2/Test.java rename to jbmc/regression/jbmc/address_space_size_limit2/src/main/java/Test.java diff --git a/jbmc/regression/jbmc/address_space_size_limit2/test.desc b/jbmc/regression/jbmc/address_space_size_limit2/test.desc index 87f368c70f9..600e3c82179 100644 --- a/jbmc/regression/jbmc/address_space_size_limit2/test.desc +++ b/jbmc/regression/jbmc/address_space_size_limit2/test.desc @@ -1,6 +1,6 @@ CORE Test ---object-bits 8 +--object-bits 8 -cp target/classes ^EXIT=10$ ^SIGNAL=0$ ^VERIFICATION FAILED$ diff --git a/jbmc/regression/jbmc/pom.xml b/jbmc/regression/jbmc/pom.xml index d91567a11fc..f4de3227ef1 100644 --- a/jbmc/regression/jbmc/pom.xml +++ b/jbmc/regression/jbmc/pom.xml @@ -17,6 +17,7 @@ aastore_aaload1 address_space_size_limit1 + address_space_size_limit2 ArithmeticException1 classpath-jar-load-whole-jar From 9026b89bfd58ea6b89e08057413cf2f7d09ecf5e Mon Sep 17 00:00:00 2001 From: Peter Schrammel Date: Thu, 2 Jan 2025 18:55:42 +0100 Subject: [PATCH 04/47] Compile jbmc/annotations1 test sources Add pom.xml for compilation, move sources remove obsolete pre-compiled class files. --- .../jbmc/annotations1/ClassAnnotation.class | Bin 146 -> 0 bytes .../jbmc/annotations1/FieldAnnotation.class | Bin 146 -> 0 bytes .../jbmc/annotations1/MethodAnnotation.class | Bin 147 -> 0 bytes .../jbmc/annotations1/annotations.class | Bin 409 -> 0 bytes jbmc/regression/jbmc/annotations1/pom.xml | 30 ++++++++++++++++++ .../annotations1/show_annotation_symbol.desc | 2 +- .../{ => src/main/java}/annotations.java | 0 jbmc/regression/jbmc/pom.xml | 1 + 8 files changed, 32 insertions(+), 1 deletion(-) delete mode 100644 jbmc/regression/jbmc/annotations1/ClassAnnotation.class delete mode 100644 jbmc/regression/jbmc/annotations1/FieldAnnotation.class delete mode 100644 jbmc/regression/jbmc/annotations1/MethodAnnotation.class delete mode 100644 jbmc/regression/jbmc/annotations1/annotations.class create mode 100644 jbmc/regression/jbmc/annotations1/pom.xml rename jbmc/regression/jbmc/annotations1/{ => src/main/java}/annotations.java (100%) diff --git a/jbmc/regression/jbmc/annotations1/ClassAnnotation.class b/jbmc/regression/jbmc/annotations1/ClassAnnotation.class deleted file mode 100644 index c5dbfca92fdbb06b62210139b16987567db4aa7b..0000000000000000000000000000000000000000 GIT binary patch literal 0 HcmV?d00001 literal 146 zcmX^0Z`VEs1_l!bPId-1b_RBK1`b9BuHgLAqU2P!%$!t427$!9y!?{HlFac; diff --git a/jbmc/regression/jbmc/annotations1/MethodAnnotation.class b/jbmc/regression/jbmc/annotations1/MethodAnnotation.class deleted file mode 100644 index 471b9576871250d2d06014e2b2b4dda2ab5acfb2..0000000000000000000000000000000000000000 GIT binary patch literal 0 HcmV?d00001 literal 147 zcmX^0Z`VEs1_l!bPId-1b_RBK1`b9BuHgLAqU2P!%$!t427$!9y!?{HlFaS6ot=CZDP}EfBXRv7w*)B-MCW(DHIA(LB;)~9dt@Efo4+lv0Mo*d;lLx zJjtT1x|nlj?tJ&2nXm7UPXK4w2~k5Yz*c~5fxK{y1p9Y|btcs#J2$zB6MbcE=9Dv; z%>~_PXmm1J*3Q}WD)29iHSSVSJ34+8tPQe>7PKQ{^-Yn+diJ0=iWjLeR?v&CwR_Hf z&k66dVm8)8Q-U3}j6I#Ixhk^=qgb1ffg^?$XJ!~tFC^^rN%i_A?T9@>?5 I7S%5B1BAUv>i_@% diff --git a/jbmc/regression/jbmc/annotations1/pom.xml b/jbmc/regression/jbmc/annotations1/pom.xml new file mode 100644 index 00000000000..edffa69b55e --- /dev/null +++ b/jbmc/regression/jbmc/annotations1/pom.xml @@ -0,0 +1,30 @@ + + + 4.0.0 + org.cprover.regression + regression.jbmc.annotations1 + 1.0-SNAPSHOT + + + org.cprover.regression + regression.jbmc + 1.0-SNAPSHOT + + + + + + maven-jar-plugin + + + default-jar + none + + + + + + + diff --git a/jbmc/regression/jbmc/annotations1/show_annotation_symbol.desc b/jbmc/regression/jbmc/annotations1/show_annotation_symbol.desc index a1f601974e1..879ce4fb9ff 100644 --- a/jbmc/regression/jbmc/annotations1/show_annotation_symbol.desc +++ b/jbmc/regression/jbmc/annotations1/show_annotation_symbol.desc @@ -1,6 +1,6 @@ CORE annotations ---no-lazy-methods --show-symbol-table --function annotations.main +--no-lazy-methods --show-symbol-table --function annotations.main -cp target/classes ^EXIT=0$ ^SIGNAL=0$ ^Type\.\.\.\.\.\.\.\.: @java::ClassAnnotation struct annotations diff --git a/jbmc/regression/jbmc/annotations1/annotations.java b/jbmc/regression/jbmc/annotations1/src/main/java/annotations.java similarity index 100% rename from jbmc/regression/jbmc/annotations1/annotations.java rename to jbmc/regression/jbmc/annotations1/src/main/java/annotations.java diff --git a/jbmc/regression/jbmc/pom.xml b/jbmc/regression/jbmc/pom.xml index f4de3227ef1..7588ccc9a06 100644 --- a/jbmc/regression/jbmc/pom.xml +++ b/jbmc/regression/jbmc/pom.xml @@ -18,6 +18,7 @@ aastore_aaload1 address_space_size_limit1 address_space_size_limit2 + annotations1 ArithmeticException1 classpath-jar-load-whole-jar From 32e9d9a32495c7d23611c0ccad170f0755db8d47 Mon Sep 17 00:00:00 2001 From: Peter Schrammel Date: Thu, 2 Jan 2025 18:58:53 +0100 Subject: [PATCH 05/47] Compile jbmc/annotations2 test sources Add pom.xml for compilation, move sources, remove obsolete pre-compiled class files. --- .../jbmc/annotations2/FieldAnnotation.class | Bin 139 -> 0 bytes jbmc/regression/jbmc/annotations2/Test.class | Bin 624 -> 0 bytes jbmc/regression/jbmc/annotations2/pom.xml | 30 ++++++++++++++++++ .../{ => src/main/java}/Test.java | 0 jbmc/regression/jbmc/annotations2/test.desc | 2 +- jbmc/regression/jbmc/pom.xml | 1 + 6 files changed, 32 insertions(+), 1 deletion(-) delete mode 100644 jbmc/regression/jbmc/annotations2/FieldAnnotation.class delete mode 100644 jbmc/regression/jbmc/annotations2/Test.class create mode 100644 jbmc/regression/jbmc/annotations2/pom.xml rename jbmc/regression/jbmc/annotations2/{ => src/main/java}/Test.java (100%) diff --git a/jbmc/regression/jbmc/annotations2/FieldAnnotation.class b/jbmc/regression/jbmc/annotations2/FieldAnnotation.class deleted file mode 100644 index 7be3db544bdcb4893b9f65102afcb02d368a3594..0000000000000000000000000000000000000000 GIT binary patch literal 0 HcmV?d00001 literal 139 zcmX^0Z`VEs1_l!bPId-1b_RBK1`b9BuHgLAqU2P!%$!t42F{Sw;u5{A#Ii(227b59 z)SMK@yuAF9#FEVXJVpiqkc56tVqUtwe^ORzatR}YJVGcDu2LVNNsWPlk%0+_nSmCA L*epPjiGdXWk#Qrp diff --git a/jbmc/regression/jbmc/annotations2/Test.class b/jbmc/regression/jbmc/annotations2/Test.class deleted file mode 100644 index c0260839fe336bac977a526bd979e30f34023b61..0000000000000000000000000000000000000000 GIT binary patch literal 0 HcmV?d00001 literal 624 zcmYk3Ur*FP6vfYNyDeLa>@I@qA__>tp9j%|H;IveL=)6R2#LIP+X)Vomb6{I3Sqy1 z&tf8pCi?DYGK4c5*!s}9b5HL*^Sd*DuYdjqu!g5TM$oRq#Y3}nJWTs=(Dv}i#|$2O zcp{LP-cXNm>2=!=Su1!KEq7#+V4PjB^+^(eV@ z@OQIb9;t0@>g#)|D4!jLXJLSGGy>G&2N=UWLEEUSNthn4ZroA5$@47d@utheY=Ak; z3mR4B$L^7eN|II5X2PKaQ?V*^uHvB=3CkXTaH0eHxV%}wA^;H}7-i-%20){2h?v{V zNy)XzY=%)7Yb#ffZ`=r4Tul@BD7?;LX_vW8^~EKux0kT{m{{cY`~suD;C#M9?azN| zzfz5@HLz{b0%UVY*CE|=lHI4`!TN`eJxTn@;dyHV2B6t;f57X*bH2i{zr(Kl?l6r< O4OZ~l3^O%2?!gWH+;q$U diff --git a/jbmc/regression/jbmc/annotations2/pom.xml b/jbmc/regression/jbmc/annotations2/pom.xml new file mode 100644 index 00000000000..ff39b676792 --- /dev/null +++ b/jbmc/regression/jbmc/annotations2/pom.xml @@ -0,0 +1,30 @@ + + + 4.0.0 + org.cprover.regression + regression.jbmc.annotations2 + 1.0-SNAPSHOT + + + org.cprover.regression + regression.jbmc + 1.0-SNAPSHOT + + + + + + maven-jar-plugin + + + default-jar + none + + + + + + + diff --git a/jbmc/regression/jbmc/annotations2/Test.java b/jbmc/regression/jbmc/annotations2/src/main/java/Test.java similarity index 100% rename from jbmc/regression/jbmc/annotations2/Test.java rename to jbmc/regression/jbmc/annotations2/src/main/java/Test.java diff --git a/jbmc/regression/jbmc/annotations2/test.desc b/jbmc/regression/jbmc/annotations2/test.desc index 28b08e36284..1f87fc5bbf8 100644 --- a/jbmc/regression/jbmc/annotations2/test.desc +++ b/jbmc/regression/jbmc/annotations2/test.desc @@ -1,6 +1,6 @@ CORE Test ---function Test.check +--function Test.check -cp target/classes ^EXIT=10$ ^SIGNAL=0$ assertion at file Test.java line 10 .* SUCCESS diff --git a/jbmc/regression/jbmc/pom.xml b/jbmc/regression/jbmc/pom.xml index 7588ccc9a06..0f4abe86b80 100644 --- a/jbmc/regression/jbmc/pom.xml +++ b/jbmc/regression/jbmc/pom.xml @@ -19,6 +19,7 @@ address_space_size_limit1 address_space_size_limit2 annotations1 + annotations2 ArithmeticException1 classpath-jar-load-whole-jar From 0f323e9e886e50a4f05f3695f0087afd42161988 Mon Sep 17 00:00:00 2001 From: Peter Schrammel Date: Thu, 2 Jan 2025 19:05:16 +0100 Subject: [PATCH 06/47] Compile jbmc/ArithmeticException2 test sources Add pom.xml for compilation, move sources, remove obsolete pre-compiled class files. --- .../ArithmeticExceptionTest.class | Bin 646 -> 0 bytes .../jbmc/ArithmeticException2/pom.xml | 30 ++++++++++++++++++ .../main/java}/ArithmeticExceptionTest.java | 0 .../jbmc/ArithmeticException2/test.desc | 2 +- jbmc/regression/jbmc/pom.xml | 1 + 5 files changed, 32 insertions(+), 1 deletion(-) delete mode 100644 jbmc/regression/jbmc/ArithmeticException2/ArithmeticExceptionTest.class create mode 100644 jbmc/regression/jbmc/ArithmeticException2/pom.xml rename jbmc/regression/jbmc/ArithmeticException2/{ => src/main/java}/ArithmeticExceptionTest.java (100%) diff --git a/jbmc/regression/jbmc/ArithmeticException2/ArithmeticExceptionTest.class b/jbmc/regression/jbmc/ArithmeticException2/ArithmeticExceptionTest.class deleted file mode 100644 index 3ac62d1ede54f090f97492e6620371a6529a2426..0000000000000000000000000000000000000000 GIT binary patch literal 0 HcmV?d00001 literal 646 zcmZvZ&rcIU6vw}>-QC&UF3=W)DzsSjfF9&R!okLXfTs$F5)<*X-A?M%c1vcb#=nJs zfHRQLL=(OHM;YI&)OuhKGjHCH&-=c&zkYxF0bmDDLxiZgY}+psco@LPBZ2i09%=#` zA?j!dY!a5A#aSk`QR6f_R9V~|${vBv2wqF2%Dg5Nx1PTzI0xgNBrLU6Dvu|luGFVC znFFI(rG(Y3kL^MHCEgy!X@9$8v`YK0Y~e!3#L4G(@p+!lVhDaK8Q#Ie&Um5|`Bquf z#=chO(?}YX9DPmXxm9&4GxO4dBP?K%P@gxsCp$t35ux^9(rmmVt;d?Mc2AY~jovTainI1qd{g1r?K-ZVEyyY3~b?Q6IfD1C?bVG8l{ zDz7YY0|$ki)yS*t%Vn;|GD42}%nZ1F3CqkBC>#r{Soec}+IDgjP^tR22reL;OE|?F WxK`(1_DrW`xF|$>cAC{Zy!HoF7ky*^ diff --git a/jbmc/regression/jbmc/ArithmeticException2/pom.xml b/jbmc/regression/jbmc/ArithmeticException2/pom.xml new file mode 100644 index 00000000000..65a12534b47 --- /dev/null +++ b/jbmc/regression/jbmc/ArithmeticException2/pom.xml @@ -0,0 +1,30 @@ + + + 4.0.0 + org.cprover.regression + regression.jbmc.ArithmeticException2 + 1.0-SNAPSHOT + + + org.cprover.regression + regression.jbmc + 1.0-SNAPSHOT + + + + + + maven-jar-plugin + + + default-jar + none + + + + + + + diff --git a/jbmc/regression/jbmc/ArithmeticException2/ArithmeticExceptionTest.java b/jbmc/regression/jbmc/ArithmeticException2/src/main/java/ArithmeticExceptionTest.java similarity index 100% rename from jbmc/regression/jbmc/ArithmeticException2/ArithmeticExceptionTest.java rename to jbmc/regression/jbmc/ArithmeticException2/src/main/java/ArithmeticExceptionTest.java diff --git a/jbmc/regression/jbmc/ArithmeticException2/test.desc b/jbmc/regression/jbmc/ArithmeticException2/test.desc index 1341d843ccb..2142ad4c6f4 100644 --- a/jbmc/regression/jbmc/ArithmeticException2/test.desc +++ b/jbmc/regression/jbmc/ArithmeticException2/test.desc @@ -1,6 +1,6 @@ CORE ArithmeticExceptionTest ---throw-runtime-exceptions +--throw-runtime-exceptions -cp target/classes ^EXIT=10$ ^SIGNAL=0$ ^.*assertion at file ArithmeticExceptionTest.java line 9 function.*: FAILURE$ diff --git a/jbmc/regression/jbmc/pom.xml b/jbmc/regression/jbmc/pom.xml index 0f4abe86b80..91bf2303980 100644 --- a/jbmc/regression/jbmc/pom.xml +++ b/jbmc/regression/jbmc/pom.xml @@ -21,6 +21,7 @@ annotations1 annotations2 ArithmeticException1 + ArithmeticException2 classpath-jar-load-whole-jar From a319745dcb73540b8e94b26e366103cfbcd44d19 Mon Sep 17 00:00:00 2001 From: Peter Schrammel Date: Thu, 2 Jan 2025 19:05:59 +0100 Subject: [PATCH 07/47] Compile jbmc/ArithmeticException3 test sources Add pom.xml for compilation, move sources, remove obsolete pre-compiled class files. --- .../ArithmeticExceptionTest.class | Bin 629 -> 0 bytes .../jbmc/ArithmeticException3/pom.xml | 30 ++++++++++++++++++ .../main/java}/ArithmeticExceptionTest.java | 0 .../jbmc/ArithmeticException3/test.desc | 2 +- jbmc/regression/jbmc/pom.xml | 1 + 5 files changed, 32 insertions(+), 1 deletion(-) delete mode 100644 jbmc/regression/jbmc/ArithmeticException3/ArithmeticExceptionTest.class create mode 100644 jbmc/regression/jbmc/ArithmeticException3/pom.xml rename jbmc/regression/jbmc/ArithmeticException3/{ => src/main/java}/ArithmeticExceptionTest.java (100%) diff --git a/jbmc/regression/jbmc/ArithmeticException3/ArithmeticExceptionTest.class b/jbmc/regression/jbmc/ArithmeticException3/ArithmeticExceptionTest.class deleted file mode 100644 index 21c451e02f32de87391382dd30ce9f5daacffdf4..0000000000000000000000000000000000000000 GIT binary patch literal 0 HcmV?d00001 literal 629 zcmZuuJx?1!5PfrZ_S(k*#w5lV9D+mv6wuINA`l@3a+1O*QlL7YS7gCHTYGE7Z{ZJ6 zJ4jdp33`4M%Itw-3bfLG%)IyJ&Fs_j-2;FvEc?izBrump7G;5XAD(?zd@Nv5ph}os z36n%>qq=eORV87wEn5USCS+?WR^|)AU0wS{@bbS@|=m2^6gz_8EsJ#QNyP7cf4$IaM_!M9Xp9zIA`DgP? zMuxi{hxXe%FmAUc6QyNqZzRuMnm#9ZTE|%CdFS{Gs8F_s_~wGFf8HngRppcT%&ZSV z0}I3y@7Xj+OqoW3?-qIjhsi+2trh%*-p)0O^}lehFmVs>_Yj%KLCO+b#^GgkDy#(l zY6lsJ)PUgPIm|O=hBE@rp+IqpL$m)qZKX26Ofh>4aRuRB!*g%oT7NIPBY##S11H$E KU3^H>AO8WIDtt!( diff --git a/jbmc/regression/jbmc/ArithmeticException3/pom.xml b/jbmc/regression/jbmc/ArithmeticException3/pom.xml new file mode 100644 index 00000000000..69c6eea5eaf --- /dev/null +++ b/jbmc/regression/jbmc/ArithmeticException3/pom.xml @@ -0,0 +1,30 @@ + + + 4.0.0 + org.cprover.regression + regression.jbmc.ArithmeticException3 + 1.0-SNAPSHOT + + + org.cprover.regression + regression.jbmc + 1.0-SNAPSHOT + + + + + + maven-jar-plugin + + + default-jar + none + + + + + + + diff --git a/jbmc/regression/jbmc/ArithmeticException3/ArithmeticExceptionTest.java b/jbmc/regression/jbmc/ArithmeticException3/src/main/java/ArithmeticExceptionTest.java similarity index 100% rename from jbmc/regression/jbmc/ArithmeticException3/ArithmeticExceptionTest.java rename to jbmc/regression/jbmc/ArithmeticException3/src/main/java/ArithmeticExceptionTest.java diff --git a/jbmc/regression/jbmc/ArithmeticException3/test.desc b/jbmc/regression/jbmc/ArithmeticException3/test.desc index 0577e08a51b..a07a8ddb801 100644 --- a/jbmc/regression/jbmc/ArithmeticException3/test.desc +++ b/jbmc/regression/jbmc/ArithmeticException3/test.desc @@ -1,6 +1,6 @@ CORE ArithmeticExceptionTest ---throw-runtime-exceptions +--throw-runtime-exceptions -cp target/classes ^EXIT=10$ ^SIGNAL=0$ ^.*assertion at file ArithmeticExceptionTest.java line 8 function.*: FAILURE$ diff --git a/jbmc/regression/jbmc/pom.xml b/jbmc/regression/jbmc/pom.xml index 91bf2303980..1116afe9590 100644 --- a/jbmc/regression/jbmc/pom.xml +++ b/jbmc/regression/jbmc/pom.xml @@ -22,6 +22,7 @@ annotations2 ArithmeticException1 ArithmeticException2 + ArithmeticException3 classpath-jar-load-whole-jar From e11c5b93dca5fa32e9f7aeac320defb0c1f5a9ef Mon Sep 17 00:00:00 2001 From: Peter Schrammel Date: Thu, 2 Jan 2025 19:06:19 +0100 Subject: [PATCH 08/47] Compile jbmc/ArithmeticException4 test sources Add pom.xml for compilation, move sources, remove obsolete pre-compiled class files. --- .../ArithmeticExceptionTest.class | Bin 646 -> 0 bytes .../jbmc/ArithmeticException4/pom.xml | 30 ++++++++++++++++++ .../main/java}/ArithmeticExceptionTest.java | 0 .../jbmc/ArithmeticException4/test.desc | 2 +- jbmc/regression/jbmc/pom.xml | 1 + 5 files changed, 32 insertions(+), 1 deletion(-) delete mode 100644 jbmc/regression/jbmc/ArithmeticException4/ArithmeticExceptionTest.class create mode 100644 jbmc/regression/jbmc/ArithmeticException4/pom.xml rename jbmc/regression/jbmc/ArithmeticException4/{ => src/main/java}/ArithmeticExceptionTest.java (100%) diff --git a/jbmc/regression/jbmc/ArithmeticException4/ArithmeticExceptionTest.class b/jbmc/regression/jbmc/ArithmeticException4/ArithmeticExceptionTest.class deleted file mode 100644 index a4723d1d652bd59d4cc9043e4a0654a2abb3aa7d..0000000000000000000000000000000000000000 GIT binary patch literal 0 HcmV?d00001 literal 646 zcmZvZO;6iE5Qg7LY_IJY2;nQGBq=Qi=%HMYI20j1N>70vf+`hGjOY9)H_k3!6vrs)A6c4z0~nRmv29)8{fSi_qTA*wFh_6r4G1n@C0@G^vls=z{s z8tMWK!qifnWl|f}PqPmyi`!k%4dSJ+wVxiL{p{mV9;wzeQ1+8 z(2G?{m|Z?@p2pwe)oz@gthS6+>B)OrIMy<8a<(6z=lLv#;BO?|zwoftALvAWR2H?c zt(E!OlSUZnf V*Xn#?4|Q6Gi$b(zr + + 4.0.0 + org.cprover.regression + regression.jbmc.ArithmeticException4 + 1.0-SNAPSHOT + + + org.cprover.regression + regression.jbmc + 1.0-SNAPSHOT + + + + + + maven-jar-plugin + + + default-jar + none + + + + + + + diff --git a/jbmc/regression/jbmc/ArithmeticException4/ArithmeticExceptionTest.java b/jbmc/regression/jbmc/ArithmeticException4/src/main/java/ArithmeticExceptionTest.java similarity index 100% rename from jbmc/regression/jbmc/ArithmeticException4/ArithmeticExceptionTest.java rename to jbmc/regression/jbmc/ArithmeticException4/src/main/java/ArithmeticExceptionTest.java diff --git a/jbmc/regression/jbmc/ArithmeticException4/test.desc b/jbmc/regression/jbmc/ArithmeticException4/test.desc index 1341d843ccb..2142ad4c6f4 100644 --- a/jbmc/regression/jbmc/ArithmeticException4/test.desc +++ b/jbmc/regression/jbmc/ArithmeticException4/test.desc @@ -1,6 +1,6 @@ CORE ArithmeticExceptionTest ---throw-runtime-exceptions +--throw-runtime-exceptions -cp target/classes ^EXIT=10$ ^SIGNAL=0$ ^.*assertion at file ArithmeticExceptionTest.java line 9 function.*: FAILURE$ diff --git a/jbmc/regression/jbmc/pom.xml b/jbmc/regression/jbmc/pom.xml index 1116afe9590..cffaa878ed0 100644 --- a/jbmc/regression/jbmc/pom.xml +++ b/jbmc/regression/jbmc/pom.xml @@ -23,6 +23,7 @@ ArithmeticException1 ArithmeticException2 ArithmeticException3 + ArithmeticException4 classpath-jar-load-whole-jar From 06a22eae49d24e01c891c4ff8fa916feb428a6ba Mon Sep 17 00:00:00 2001 From: Peter Schrammel Date: Thu, 2 Jan 2025 19:06:44 +0100 Subject: [PATCH 09/47] Compile jbmc/ArithmeticException5 test sources Add pom.xml for compilation, move sources, remove obsolete pre-compiled class files. --- .../ArithmeticExceptionTest.class | Bin 639 -> 0 bytes .../jbmc/ArithmeticException5/pom.xml | 30 ++++++++++++++++++ .../main/java}/ArithmeticExceptionTest.java | 0 .../jbmc/ArithmeticException5/test.desc | 2 +- jbmc/regression/jbmc/pom.xml | 1 + 5 files changed, 32 insertions(+), 1 deletion(-) delete mode 100644 jbmc/regression/jbmc/ArithmeticException5/ArithmeticExceptionTest.class create mode 100644 jbmc/regression/jbmc/ArithmeticException5/pom.xml rename jbmc/regression/jbmc/ArithmeticException5/{ => src/main/java}/ArithmeticExceptionTest.java (100%) diff --git a/jbmc/regression/jbmc/ArithmeticException5/ArithmeticExceptionTest.class b/jbmc/regression/jbmc/ArithmeticException5/ArithmeticExceptionTest.class deleted file mode 100644 index 813391d04afa843b51da2278350fa0eeaecd54a3..0000000000000000000000000000000000000000 GIT binary patch literal 0 HcmV?d00001 literal 639 zcmZuvO;6iE5Pg%_UdNaa!dD8UpGbTh;KB`5fq<$ip*;juDsXX}6L>hEXQe2Th(qhZsUgsQm}(kGG?BstHriRM{Q^uS2}S zTS8?}{H1jwW5ZJqLR%eP7?0bQnbNYo*{A0zO^*}2tpn!q`4<3GsaZjMD}pzHGM^*t z)!7nTcj*>%Wr3*h>E%H}38Sd;-9nGxz-2pA{y2`peER7U)y6g43k>~+_w5$q{wgo? zxs!uJPBhI_$UT>plsF?;1-}7SHO3i%!mhx0nL`u*M6KpDz-ZO~iP8mxa|x$-1J?@t T!`l~VIb0ON4LinUo}PLF!N`3} diff --git a/jbmc/regression/jbmc/ArithmeticException5/pom.xml b/jbmc/regression/jbmc/ArithmeticException5/pom.xml new file mode 100644 index 00000000000..48d152a576e --- /dev/null +++ b/jbmc/regression/jbmc/ArithmeticException5/pom.xml @@ -0,0 +1,30 @@ + + + 4.0.0 + org.cprover.regression + regression.jbmc.ArithmeticException5 + 1.0-SNAPSHOT + + + org.cprover.regression + regression.jbmc + 1.0-SNAPSHOT + + + + + + maven-jar-plugin + + + default-jar + none + + + + + + + diff --git a/jbmc/regression/jbmc/ArithmeticException5/ArithmeticExceptionTest.java b/jbmc/regression/jbmc/ArithmeticException5/src/main/java/ArithmeticExceptionTest.java similarity index 100% rename from jbmc/regression/jbmc/ArithmeticException5/ArithmeticExceptionTest.java rename to jbmc/regression/jbmc/ArithmeticException5/src/main/java/ArithmeticExceptionTest.java diff --git a/jbmc/regression/jbmc/ArithmeticException5/test.desc b/jbmc/regression/jbmc/ArithmeticException5/test.desc index 3df41a2390a..a5d9fe7cac6 100644 --- a/jbmc/regression/jbmc/ArithmeticException5/test.desc +++ b/jbmc/regression/jbmc/ArithmeticException5/test.desc @@ -1,6 +1,6 @@ CORE ArithmeticExceptionTest ---throw-runtime-exceptions +--throw-runtime-exceptions -cp target/classes ^EXIT=0$ ^SIGNAL=0$ ^VERIFICATION SUCCESSFUL diff --git a/jbmc/regression/jbmc/pom.xml b/jbmc/regression/jbmc/pom.xml index cffaa878ed0..49447e83847 100644 --- a/jbmc/regression/jbmc/pom.xml +++ b/jbmc/regression/jbmc/pom.xml @@ -24,6 +24,7 @@ ArithmeticException2 ArithmeticException3 ArithmeticException4 + ArithmeticException5 classpath-jar-load-whole-jar From 7c186396e939f9db07943dfca69c553d884fa154 Mon Sep 17 00:00:00 2001 From: Peter Schrammel Date: Thu, 2 Jan 2025 19:07:04 +0100 Subject: [PATCH 10/47] Compile jbmc/ArithmeticException6 test sources Add pom.xml for compilation, move sources, remove obsolete pre-compiled class files. --- .../ArithmeticExceptionTest.class | Bin 605 -> 0 bytes .../jbmc/ArithmeticException6/pom.xml | 30 ++++++++++++++++++ .../main/java}/ArithmeticExceptionTest.java | 0 .../jbmc/ArithmeticException6/test.desc | 2 +- jbmc/regression/jbmc/pom.xml | 1 + 5 files changed, 32 insertions(+), 1 deletion(-) delete mode 100644 jbmc/regression/jbmc/ArithmeticException6/ArithmeticExceptionTest.class create mode 100644 jbmc/regression/jbmc/ArithmeticException6/pom.xml rename jbmc/regression/jbmc/ArithmeticException6/{ => src/main/java}/ArithmeticExceptionTest.java (100%) diff --git a/jbmc/regression/jbmc/ArithmeticException6/ArithmeticExceptionTest.class b/jbmc/regression/jbmc/ArithmeticException6/ArithmeticExceptionTest.class deleted file mode 100644 index fdcb29ad2522533d0fdb0d5fb7d08fe1d7d592ca..0000000000000000000000000000000000000000 GIT binary patch literal 0 HcmV?d00001 literal 605 zcmZutO;5r=5Pd^Si?s@(0-~rS9@K+gI1(d4j3#~@P!qkCveCs-Ok0e<#XrCqO*GL& z@BS#`EQ)wAo6OA4ym|9xK0aUG0F+R)kU+*nb_@n`Cgv>Y>YukTj|CG2!t{z0h9Zb$ z#}9X8=rlahB+v!HC`(^PTLf)&?TnyTJ551I9!Ostb=wUQoG36C+K%+ut?nz>L_Koc z>qF;eQ038tMA`LzsH}RY8@OUus>X#%Afv0ch@@M)bH$C)a3aEJqvhN>HpXES3M$_8 z9RG6jAGD1zScKdk&~TYr5Oe}U_Ma{_!^EPEB`gzCqvqpAOSlp5I7(GLJ`W+&6rl`6 zvofUTEu$_M_%;_P@^uq@a7yKrAdWPU($98+e+Bl$KED18>MI~7*&2f+aZ3^@jurG2 zF@8WUW#zqc59xykX!jU@g?|2w_}{ogW>B8}0?o>G7XSbN diff --git a/jbmc/regression/jbmc/ArithmeticException6/pom.xml b/jbmc/regression/jbmc/ArithmeticException6/pom.xml new file mode 100644 index 00000000000..f22db55b6c9 --- /dev/null +++ b/jbmc/regression/jbmc/ArithmeticException6/pom.xml @@ -0,0 +1,30 @@ + + + 4.0.0 + org.cprover.regression + regression.jbmc.ArithmeticException6 + 1.0-SNAPSHOT + + + org.cprover.regression + regression.jbmc + 1.0-SNAPSHOT + + + + + + maven-jar-plugin + + + default-jar + none + + + + + + + diff --git a/jbmc/regression/jbmc/ArithmeticException6/ArithmeticExceptionTest.java b/jbmc/regression/jbmc/ArithmeticException6/src/main/java/ArithmeticExceptionTest.java similarity index 100% rename from jbmc/regression/jbmc/ArithmeticException6/ArithmeticExceptionTest.java rename to jbmc/regression/jbmc/ArithmeticException6/src/main/java/ArithmeticExceptionTest.java diff --git a/jbmc/regression/jbmc/ArithmeticException6/test.desc b/jbmc/regression/jbmc/ArithmeticException6/test.desc index 438f1f346da..6782f32d8d9 100644 --- a/jbmc/regression/jbmc/ArithmeticException6/test.desc +++ b/jbmc/regression/jbmc/ArithmeticException6/test.desc @@ -1,6 +1,6 @@ CORE ArithmeticExceptionTest ---throw-runtime-exceptions --function ArithmeticExceptionTest.main +--throw-runtime-exceptions --function ArithmeticExceptionTest.main -cp target/classes ^EXIT=10$ ^SIGNAL=0$ ^.*assertion at file ArithmeticExceptionTest.java line 7 function.*: FAILURE$ diff --git a/jbmc/regression/jbmc/pom.xml b/jbmc/regression/jbmc/pom.xml index 49447e83847..3c62da570ea 100644 --- a/jbmc/regression/jbmc/pom.xml +++ b/jbmc/regression/jbmc/pom.xml @@ -25,6 +25,7 @@ ArithmeticException3 ArithmeticException4 ArithmeticException5 + ArithmeticException6 classpath-jar-load-whole-jar From 42c3f8d1983001dd2c75ebaa1e3f2e827d3316ab Mon Sep 17 00:00:00 2001 From: Peter Schrammel Date: Thu, 2 Jan 2025 19:07:28 +0100 Subject: [PATCH 11/47] Compile jbmc/ArithmeticException7 test sources Add pom.xml for compilation, move sources, remove obsolete pre-compiled class files. --- .../ArithmeticExceptionTest.class | Bin 619 -> 0 bytes .../java/lang/ArithmeticException.class | Bin 232 -> 0 bytes .../java/lang/RuntimeException.class | Bin 219 -> 0 bytes .../jbmc/ArithmeticException7/pom.xml | 30 ++++++++++++++++++ .../main/java}/ArithmeticExceptionTest.java | 0 .../java}/java/lang/ArithmeticException.java | 0 .../java}/java/lang/RuntimeException.java | 0 .../jbmc/ArithmeticException7/test.desc | 2 +- jbmc/regression/jbmc/pom.xml | 1 + 9 files changed, 32 insertions(+), 1 deletion(-) delete mode 100644 jbmc/regression/jbmc/ArithmeticException7/ArithmeticExceptionTest.class delete mode 100644 jbmc/regression/jbmc/ArithmeticException7/java/lang/ArithmeticException.class delete mode 100644 jbmc/regression/jbmc/ArithmeticException7/java/lang/RuntimeException.class create mode 100644 jbmc/regression/jbmc/ArithmeticException7/pom.xml rename jbmc/regression/jbmc/ArithmeticException7/{ => src/main/java}/ArithmeticExceptionTest.java (100%) rename jbmc/regression/jbmc/ArithmeticException7/{ => src/main/java}/java/lang/ArithmeticException.java (100%) rename jbmc/regression/jbmc/ArithmeticException7/{ => src/main/java}/java/lang/RuntimeException.java (100%) diff --git a/jbmc/regression/jbmc/ArithmeticException7/ArithmeticExceptionTest.class b/jbmc/regression/jbmc/ArithmeticException7/ArithmeticExceptionTest.class deleted file mode 100644 index 621ed3729b0f22ade9a1335f634bf4892e353be0..0000000000000000000000000000000000000000 GIT binary patch literal 0 HcmV?d00001 literal 619 zcmZ`$%T60X5Uk!^d(5(aU=lFKyd)050WRF)L?9rC$iTq}34B_wM=-EnquDXyTlfLa zBvOzP3GRGUl%6Hnr)Z>kbXQeZ_q_i3^$cJeD?SRC5tyAo9yNhEAD(^JeaxdFut1nz z4bxO=qXtR3uhOs^%N~Kw3HhcqKh;J^)y5_yeuLVAd&)min=+OdE z;ys@Qi791N_->&cI7|lWZnNUg$DbciZGDG(kICQg&YqBadCXXX%Q(EOPMwv&AM79p zkr@zNyns2zOmRlQ`6f^;acFwvX*-hvrmFd$5cd$?13dQ!T$iWGAY!@H0 G^vAygOn5H< diff --git a/jbmc/regression/jbmc/ArithmeticException7/java/lang/ArithmeticException.class b/jbmc/regression/jbmc/ArithmeticException7/java/lang/ArithmeticException.class deleted file mode 100644 index a85ed965b94f14ef8b4039a41f7ab4ddc40b956f..0000000000000000000000000000000000000000 GIT binary patch literal 0 HcmV?d00001 literal 232 zcmX^0Z`VEs1_l!bUM>b^1}=66ZgvJ9Mg}&U%)HDJJ4Oa(4b3n{1{UZ1lvG9rexJ;| zRKL>Pq|~C2#H1Xc2v=}^X;E^jTPBDj;aHSel98KQl9}vUk(^pkl9`{Umz7wS$iu+G zz{nF^EX6aJ diff --git a/jbmc/regression/jbmc/ArithmeticException7/java/lang/RuntimeException.class b/jbmc/regression/jbmc/ArithmeticException7/java/lang/RuntimeException.class deleted file mode 100644 index 2f0ac26544c602aa8e73f1ca35724acb4aa9c8a5..0000000000000000000000000000000000000000 GIT binary patch literal 0 HcmV?d00001 literal 219 zcmX^0Z`VEs1_l!bUM>b^1}=66ZgvJ9Mg}&U%)HDJJ4Oa(4b3n{1{UZ1lvG9rexJ;| zRKL>Pq|~C2#H1Xc2v=}^X;E^jTPBDj8dREBl9`+8T9KSuP?DLSr!T}UWDrJ3!ZkA}GB5$11Okje2s8vpvH^LrU_Ju_tJZb~#*JWUb|A?H Q6lMTwU}WF`(o77T0A{Z)TL1t6 diff --git a/jbmc/regression/jbmc/ArithmeticException7/pom.xml b/jbmc/regression/jbmc/ArithmeticException7/pom.xml new file mode 100644 index 00000000000..6b3c9765c17 --- /dev/null +++ b/jbmc/regression/jbmc/ArithmeticException7/pom.xml @@ -0,0 +1,30 @@ + + + 4.0.0 + org.cprover.regression + regression.jbmc.ArithmeticException7 + 1.0-SNAPSHOT + + + org.cprover.regression + regression.jbmc + 1.0-SNAPSHOT + + + + + + maven-jar-plugin + + + default-jar + none + + + + + + + diff --git a/jbmc/regression/jbmc/ArithmeticException7/ArithmeticExceptionTest.java b/jbmc/regression/jbmc/ArithmeticException7/src/main/java/ArithmeticExceptionTest.java similarity index 100% rename from jbmc/regression/jbmc/ArithmeticException7/ArithmeticExceptionTest.java rename to jbmc/regression/jbmc/ArithmeticException7/src/main/java/ArithmeticExceptionTest.java diff --git a/jbmc/regression/jbmc/ArithmeticException7/java/lang/ArithmeticException.java b/jbmc/regression/jbmc/ArithmeticException7/src/main/java/java/lang/ArithmeticException.java similarity index 100% rename from jbmc/regression/jbmc/ArithmeticException7/java/lang/ArithmeticException.java rename to jbmc/regression/jbmc/ArithmeticException7/src/main/java/java/lang/ArithmeticException.java diff --git a/jbmc/regression/jbmc/ArithmeticException7/java/lang/RuntimeException.java b/jbmc/regression/jbmc/ArithmeticException7/src/main/java/java/lang/RuntimeException.java similarity index 100% rename from jbmc/regression/jbmc/ArithmeticException7/java/lang/RuntimeException.java rename to jbmc/regression/jbmc/ArithmeticException7/src/main/java/java/lang/RuntimeException.java diff --git a/jbmc/regression/jbmc/ArithmeticException7/test.desc b/jbmc/regression/jbmc/ArithmeticException7/test.desc index 0577e08a51b..a07a8ddb801 100644 --- a/jbmc/regression/jbmc/ArithmeticException7/test.desc +++ b/jbmc/regression/jbmc/ArithmeticException7/test.desc @@ -1,6 +1,6 @@ CORE ArithmeticExceptionTest ---throw-runtime-exceptions +--throw-runtime-exceptions -cp target/classes ^EXIT=10$ ^SIGNAL=0$ ^.*assertion at file ArithmeticExceptionTest.java line 8 function.*: FAILURE$ diff --git a/jbmc/regression/jbmc/pom.xml b/jbmc/regression/jbmc/pom.xml index 3c62da570ea..f9fc4f8b9bc 100644 --- a/jbmc/regression/jbmc/pom.xml +++ b/jbmc/regression/jbmc/pom.xml @@ -26,6 +26,7 @@ ArithmeticException4 ArithmeticException5 ArithmeticException6 + ArithmeticException7 classpath-jar-load-whole-jar From b44d1f4a30b8d1d0cdeb97316c1fa6f2f7e6a4ef Mon Sep 17 00:00:00 2001 From: Peter Schrammel Date: Thu, 2 Jan 2025 19:14:41 +0100 Subject: [PATCH 12/47] Compile jbmc/array1 test sources Add pom.xml for compilation, move sources, remove obsolete pre-compiled class files. --- jbmc/regression/jbmc/array1/array1.class | Bin 660 -> 0 bytes jbmc/regression/jbmc/array1/pom.xml | 30 ++++++++++++++++++ .../array1/{ => src/main/java}/array1.java | 0 .../array1/{ => src/main/java}/what_not.java | 0 jbmc/regression/jbmc/array1/test.desc | 2 +- jbmc/regression/jbmc/array1/what_not.class | Bin 190 -> 0 bytes jbmc/regression/jbmc/pom.xml | 1 + 7 files changed, 32 insertions(+), 1 deletion(-) delete mode 100644 jbmc/regression/jbmc/array1/array1.class create mode 100644 jbmc/regression/jbmc/array1/pom.xml rename jbmc/regression/jbmc/array1/{ => src/main/java}/array1.java (100%) rename jbmc/regression/jbmc/array1/{ => src/main/java}/what_not.java (100%) delete mode 100644 jbmc/regression/jbmc/array1/what_not.class diff --git a/jbmc/regression/jbmc/array1/array1.class b/jbmc/regression/jbmc/array1/array1.class deleted file mode 100644 index 6cc7d0164b63c224b902dc05f9cc95a13770a04f..0000000000000000000000000000000000000000 GIT binary patch literal 0 HcmV?d00001 literal 660 zcmYjPU2D@|6n;*V=55ogOS{@tV|40}DRV{W-O5m=;-K3uDuU~UylunG>=JpCD&G4m z=7r$Ru2pd0$GrFVcqKADZ?vly%{j?=zRscFPd*(3XkpPt0rN#zXb7COVPIb1oPcNJ zJbZx*gtiR_PpA%S)XRy&Nsbd6vvU3*9{*W+P8nC*m7ur=QA2kL+H$rvN@8`ZnK-JFxp+!#F=g?2TwQUvkWhAQDA{kXb(pJ^zCjuR)gSP zsMShRDf#l|ik5Ovg5#hFo6wkQ-<|}%t5mF5>ctb8K91s)Gyi1^Tyk(3R|xKuw%y+g z28_w|HrS@unXp!QsVQoG#P{HBhCvdlV0h}qOQd5S@G*9g~@H`ble&IT<$gWHB(Kl8?N2?$pY{1C^@v5#j*CJcMa{KyGR{*-s1Rk#lb8 KE1b#l)c*i0lzagI diff --git a/jbmc/regression/jbmc/array1/pom.xml b/jbmc/regression/jbmc/array1/pom.xml new file mode 100644 index 00000000000..f53f1d4c392 --- /dev/null +++ b/jbmc/regression/jbmc/array1/pom.xml @@ -0,0 +1,30 @@ + + + 4.0.0 + org.cprover.regression + regression.jbmc.array1 + 1.0-SNAPSHOT + + + org.cprover.regression + regression.jbmc + 1.0-SNAPSHOT + + + + + + maven-jar-plugin + + + default-jar + none + + + + + + + diff --git a/jbmc/regression/jbmc/array1/array1.java b/jbmc/regression/jbmc/array1/src/main/java/array1.java similarity index 100% rename from jbmc/regression/jbmc/array1/array1.java rename to jbmc/regression/jbmc/array1/src/main/java/array1.java diff --git a/jbmc/regression/jbmc/array1/what_not.java b/jbmc/regression/jbmc/array1/src/main/java/what_not.java similarity index 100% rename from jbmc/regression/jbmc/array1/what_not.java rename to jbmc/regression/jbmc/array1/src/main/java/what_not.java diff --git a/jbmc/regression/jbmc/array1/test.desc b/jbmc/regression/jbmc/array1/test.desc index da6eeb929fe..315e1390053 100644 --- a/jbmc/regression/jbmc/array1/test.desc +++ b/jbmc/regression/jbmc/array1/test.desc @@ -1,6 +1,6 @@ CORE array1 - +-cp target/classes ^EXIT=0$ ^SIGNAL=0$ ^VERIFICATION SUCCESSFUL$ diff --git a/jbmc/regression/jbmc/array1/what_not.class b/jbmc/regression/jbmc/array1/what_not.class deleted file mode 100644 index 752b97aa8b348b8d6f2146d9a4586a524d392cbb..0000000000000000000000000000000000000000 GIT binary patch literal 0 HcmV?d00001 literal 190 zcmX^0Z`VEs1_l!bUM>b^1}=66ZgvJ9Mg}&U%)HDJJ4Oa(4b3n{1{UZ1lvG9rexJ;| zRKL>Pq|~C2#H1Xc2v=}^X;E^jTPBFZTb_|v5}%h}qL-CemdL}v!obSNzyT9vWDo!e z>*plqrR)1AWu+#UFeorE0c`~VMj!^N2hwanmMoA4iLh#IXJFh2mSzW%Y+yl<6bF#U H#J~vvArithmeticException5 ArithmeticException6 ArithmeticException7 + array1 classpath-jar-load-whole-jar From f657d503c6db2fe8224c07b3b208b830504bd9d6 Mon Sep 17 00:00:00 2001 From: Peter Schrammel Date: Thu, 2 Jan 2025 19:15:09 +0100 Subject: [PATCH 13/47] Compile jbmc/array2 test sources Add pom.xml for compilation, move sources, remove obsolete pre-compiled class files. --- jbmc/regression/jbmc/array2/pom.xml | 30 ++++++++++++++++++ .../jbmc/array2/{ => src/main/java}/test.java | 0 jbmc/regression/jbmc/array2/test.class | Bin 591 -> 0 bytes jbmc/regression/jbmc/array2/test.desc | 2 +- jbmc/regression/jbmc/pom.xml | 1 + 5 files changed, 32 insertions(+), 1 deletion(-) create mode 100644 jbmc/regression/jbmc/array2/pom.xml rename jbmc/regression/jbmc/array2/{ => src/main/java}/test.java (100%) delete mode 100644 jbmc/regression/jbmc/array2/test.class diff --git a/jbmc/regression/jbmc/array2/pom.xml b/jbmc/regression/jbmc/array2/pom.xml new file mode 100644 index 00000000000..611d48a56f7 --- /dev/null +++ b/jbmc/regression/jbmc/array2/pom.xml @@ -0,0 +1,30 @@ + + + 4.0.0 + org.cprover.regression + regression.jbmc.array2 + 1.0-SNAPSHOT + + + org.cprover.regression + regression.jbmc + 1.0-SNAPSHOT + + + + + + maven-jar-plugin + + + default-jar + none + + + + + + + diff --git a/jbmc/regression/jbmc/array2/test.java b/jbmc/regression/jbmc/array2/src/main/java/test.java similarity index 100% rename from jbmc/regression/jbmc/array2/test.java rename to jbmc/regression/jbmc/array2/src/main/java/test.java diff --git a/jbmc/regression/jbmc/array2/test.class b/jbmc/regression/jbmc/array2/test.class deleted file mode 100644 index 10fc89c0a6861638963c32b5bb866eee630529d8..0000000000000000000000000000000000000000 GIT binary patch literal 0 HcmV?d00001 literal 591 zcmYLFO)mpc6g_X=OrK7t`b7;@9|?jqSac~uT9PI{7DR&8w0&f#R%WJthP^IWS|iZ} zVedDIxNoAmx%b_B&%NiI_x1Do0icK}69U6g7|05YnBW)|uuY6&Od!XQnQ?qydV$+& z`eoO5sts9ZV8;xRRk!H|YYcpT;gCTuwd#@~vF$eHZu_z-y#oa%>?sZBD+&|e51iV? zj&l``1jZQ#R%?yFJLZ0??bYO#tG1$n^n;~y=i0GgB4%L#Q3hKzmK#pu z9#NhtOX3(Nrm+F`=th1W60K}?|QQSe~?55Z5oiTV@%V}2>L0O zw3P&UaWJKbqD57nGNWuPcEKJM5OIo;u&G9aNKjPJ8(QU*%egz4`n$RF0Kq9yDGFTQ zqijDx>tMFPm-Kr~yn!Eep?`+WWZ~l$v0h6tX(7{GC@KP-WX9;7pqL@P5n|3!wSp8% zNFzxb7L3?8xIjwSX|j|4w^0oB0;#m|f=CBKe}K-Pq4kM+mee5wnzgRnWkMZ8zdyNV ACjbBd diff --git a/jbmc/regression/jbmc/array2/test.desc b/jbmc/regression/jbmc/array2/test.desc index 452845047bb..2b2bb8c0ee6 100644 --- a/jbmc/regression/jbmc/array2/test.desc +++ b/jbmc/regression/jbmc/array2/test.desc @@ -1,6 +1,6 @@ CORE test ---function test.f +--function test.f -cp target/classes ^EXIT=0$ ^SIGNAL=0$ -- diff --git a/jbmc/regression/jbmc/pom.xml b/jbmc/regression/jbmc/pom.xml index 953b78df7a1..1d61b9d1292 100644 --- a/jbmc/regression/jbmc/pom.xml +++ b/jbmc/regression/jbmc/pom.xml @@ -28,6 +28,7 @@ ArithmeticException6 ArithmeticException7 array1 + array2 classpath-jar-load-whole-jar From c321c93d752292f98c085816de2b1fe962cd2184 Mon Sep 17 00:00:00 2001 From: Peter Schrammel Date: Thu, 2 Jan 2025 19:15:57 +0100 Subject: [PATCH 14/47] Compile jbmc/array-cell-sensitivity1 test sources Add pom.xml for compilation, move sources, remove obsolete pre-compiled class files. --- .../jbmc/array-cell-sensitivity1/Test.class | Bin 642 -> 0 bytes .../jbmc/array-cell-sensitivity1/pom.xml | 30 ++++++++++++++++++ .../{ => src/main/java}/Test.java | 0 .../test-max-array-size-10.desc | 2 +- .../test-max-array-size-9.desc | 2 +- .../test-no-array-field-sensitivity.desc | 2 +- .../jbmc/array-cell-sensitivity1/test.desc | 2 +- jbmc/regression/jbmc/pom.xml | 1 + 8 files changed, 35 insertions(+), 4 deletions(-) delete mode 100644 jbmc/regression/jbmc/array-cell-sensitivity1/Test.class create mode 100644 jbmc/regression/jbmc/array-cell-sensitivity1/pom.xml rename jbmc/regression/jbmc/array-cell-sensitivity1/{ => src/main/java}/Test.java (100%) diff --git a/jbmc/regression/jbmc/array-cell-sensitivity1/Test.class b/jbmc/regression/jbmc/array-cell-sensitivity1/Test.class deleted file mode 100644 index 57c9912d5717ec487cb350fe476f2aadae84af14..0000000000000000000000000000000000000000 GIT binary patch literal 0 HcmV?d00001 literal 642 zcmZWlO-~d-5PdZ>yS+OMvMjpdiYN;jbQAW%O=2{t3CZdnASB?acebMg!;F~^^|x^G z=vhr9QKNT%lQF&?5Duo(T~)8EUcIVcf4=?zu#P)E6c(DO;fBJZ4;KpxH+|f~l0r`~ zx1#ghWJQ!F`Qs?pa0FQ9`r2Ww}(D946^o0PeQR89Unoh2;P% zxGiX1WRAuMCM-DF1+*D+DT2<#FdE_OZmBD(+ZX^R_!Z7h=Wm4Hyk* zg|>F@1oDxNgK56?3KU$TADkv&1}#QS%%V-i7MCP*XqQ|5cYoOLdZWJA9esjxjCS8! z>%Pa-H@JHz@P1lqx1#P)5&QAfNv4Q3(4!*Ts&h(*Ib5!C7IB4`;3}gAc8+W3 l`qwLQz-+tr1@&Vn?*lydGo1ftu_QG(!9zQ7mw|)pe*x}bZCL;S diff --git a/jbmc/regression/jbmc/array-cell-sensitivity1/pom.xml b/jbmc/regression/jbmc/array-cell-sensitivity1/pom.xml new file mode 100644 index 00000000000..8148be54c60 --- /dev/null +++ b/jbmc/regression/jbmc/array-cell-sensitivity1/pom.xml @@ -0,0 +1,30 @@ + + + 4.0.0 + org.cprover.regression + regression.jbmc.array-cell-sensitivity1 + 1.0-SNAPSHOT + + + org.cprover.regression + regression.jbmc + 1.0-SNAPSHOT + + + + + + maven-jar-plugin + + + default-jar + none + + + + + + + diff --git a/jbmc/regression/jbmc/array-cell-sensitivity1/Test.java b/jbmc/regression/jbmc/array-cell-sensitivity1/src/main/java/Test.java similarity index 100% rename from jbmc/regression/jbmc/array-cell-sensitivity1/Test.java rename to jbmc/regression/jbmc/array-cell-sensitivity1/src/main/java/Test.java diff --git a/jbmc/regression/jbmc/array-cell-sensitivity1/test-max-array-size-10.desc b/jbmc/regression/jbmc/array-cell-sensitivity1/test-max-array-size-10.desc index 34336440f7a..ea0b6b1ce36 100644 --- a/jbmc/regression/jbmc/array-cell-sensitivity1/test-max-array-size-10.desc +++ b/jbmc/regression/jbmc/array-cell-sensitivity1/test-max-array-size-10.desc @@ -1,6 +1,6 @@ CORE Test ---function Test.main --show-vcc --max-field-sensitivity-array-size 10 +--function Test.main --show-vcc --max-field-sensitivity-array-size 10 -cp target/classes symex_dynamic::dynamic_array#2\[\[0\]\] = symex_dynamic::dynamic_array#2\[\[1\]\] = symex_dynamic::dynamic_array#2\[\[2\]\] = diff --git a/jbmc/regression/jbmc/array-cell-sensitivity1/test-max-array-size-9.desc b/jbmc/regression/jbmc/array-cell-sensitivity1/test-max-array-size-9.desc index db0ec927037..dfb2ea1b7e0 100644 --- a/jbmc/regression/jbmc/array-cell-sensitivity1/test-max-array-size-9.desc +++ b/jbmc/regression/jbmc/array-cell-sensitivity1/test-max-array-size-9.desc @@ -1,6 +1,6 @@ CORE Test ---function Test.main --show-vcc --max-field-sensitivity-array-size 9 +--function Test.main --show-vcc --max-field-sensitivity-array-size 9 -cp target/classes ^EXIT=0$ ^SIGNAL=0$ symex_dynamic::dynamic_array#[0-9]\[1\] diff --git a/jbmc/regression/jbmc/array-cell-sensitivity1/test-no-array-field-sensitivity.desc b/jbmc/regression/jbmc/array-cell-sensitivity1/test-no-array-field-sensitivity.desc index 2fbb2dd7dc3..6cc50795e6c 100644 --- a/jbmc/regression/jbmc/array-cell-sensitivity1/test-no-array-field-sensitivity.desc +++ b/jbmc/regression/jbmc/array-cell-sensitivity1/test-no-array-field-sensitivity.desc @@ -1,6 +1,6 @@ CORE Test ---function Test.main --show-vcc --no-array-field-sensitivity +--function Test.main --show-vcc --no-array-field-sensitivity -cp target/classes ^EXIT=0$ ^SIGNAL=0$ symex_dynamic::dynamic_array#[0-9]\[1\] diff --git a/jbmc/regression/jbmc/array-cell-sensitivity1/test.desc b/jbmc/regression/jbmc/array-cell-sensitivity1/test.desc index 5061f9230e4..165a8c26b67 100644 --- a/jbmc/regression/jbmc/array-cell-sensitivity1/test.desc +++ b/jbmc/regression/jbmc/array-cell-sensitivity1/test.desc @@ -1,6 +1,6 @@ CORE Test ---function Test.main --show-vcc +--function Test.main --show-vcc -cp target/classes symex_dynamic::dynamic_array#2\[\[0\]\] = symex_dynamic::dynamic_array#2\[\[1\]\] = symex_dynamic::dynamic_array#2\[\[2\]\] = diff --git a/jbmc/regression/jbmc/pom.xml b/jbmc/regression/jbmc/pom.xml index 1d61b9d1292..64e35e3493d 100644 --- a/jbmc/regression/jbmc/pom.xml +++ b/jbmc/regression/jbmc/pom.xml @@ -29,6 +29,7 @@ ArithmeticException7 array1 array2 + array-cell-sensitivity1 classpath-jar-load-whole-jar From 8a1652edefb7af65f4caa4747a05d4ce32d7f52a Mon Sep 17 00:00:00 2001 From: Peter Schrammel Date: Thu, 2 Jan 2025 19:16:20 +0100 Subject: [PATCH 15/47] Compile jbmc/array-cell-sensitivity2 test sources Add pom.xml for compilation, move sources, remove obsolete pre-compiled class files. --- .../jbmc/array-cell-sensitivity2/Test.class | Bin 1179 -> 0 bytes .../jbmc/array-cell-sensitivity2/pom.xml | 30 ++++++++++++++++++ .../{ => src/main/java}/Test.java | 0 .../jbmc/array-cell-sensitivity2/test.desc | 2 +- jbmc/regression/jbmc/pom.xml | 1 + 5 files changed, 32 insertions(+), 1 deletion(-) delete mode 100644 jbmc/regression/jbmc/array-cell-sensitivity2/Test.class create mode 100644 jbmc/regression/jbmc/array-cell-sensitivity2/pom.xml rename jbmc/regression/jbmc/array-cell-sensitivity2/{ => src/main/java}/Test.java (100%) diff --git a/jbmc/regression/jbmc/array-cell-sensitivity2/Test.class b/jbmc/regression/jbmc/array-cell-sensitivity2/Test.class deleted file mode 100644 index ae3d24793dc7256a0dad28f2e22c9a0f3ecfa12c..0000000000000000000000000000000000000000 GIT binary patch literal 0 HcmV?d00001 literal 1179 zcmb_cOHUI~7(I99&P-dTP{8u?t*C_-klNHlh>xHqBn6EnB;sn?PGq3WkZG&_1mn^r z3t77Mfg}=jum4FrcUma!T-Y}Ee&4xgzQ_6Q^ylxd-vJa*NFafXg^4&cOeVNwl$BLW z&cajz7BUG;W5&XD0aj zcWb1t37GSq?=^1==$VOC23iPeu0UVO^WEjvR>cih6j@-P6jYu1suOz3?|`zo?llP?h`R#T`O-dEwaT#{i=!z(x|iHhN&&=tD|iL@{RSj{kh- z-jN;;!Y~Le%-YC<=~G?GqsoR`W!ZgQXrWFW1%_&F!wcQoaS#^UZ1I31uHhnQl;9L~ z2$h=_+d(go8c}6*PFN=KL3(rK3+~CueTYfp8?-&>9|&kT#Z?Vog^>KFY1wTuhA>Po zjuDKu18FHTV#Ib;jM4$Lr~8mgoqaj0=gL_*RnC2eu8$epJFs%^(E;R`*#)K|M(l4u zj-{+Fq8Fts8nS5WMJt<@c|MUgqScI6D=+t8e1y4!K_)chE_x1Nv7p!w)tVl)R-`Uq z$p+g}p4*}ZCJL=lk= Q1~mIF|08gfaWq`}1H4JKL;wH) diff --git a/jbmc/regression/jbmc/array-cell-sensitivity2/pom.xml b/jbmc/regression/jbmc/array-cell-sensitivity2/pom.xml new file mode 100644 index 00000000000..10c5aab568d --- /dev/null +++ b/jbmc/regression/jbmc/array-cell-sensitivity2/pom.xml @@ -0,0 +1,30 @@ + + + 4.0.0 + org.cprover.regression + regression.jbmc.array-cell-sensitivity2 + 1.0-SNAPSHOT + + + org.cprover.regression + regression.jbmc + 1.0-SNAPSHOT + + + + + + maven-jar-plugin + + + default-jar + none + + + + + + + diff --git a/jbmc/regression/jbmc/array-cell-sensitivity2/Test.java b/jbmc/regression/jbmc/array-cell-sensitivity2/src/main/java/Test.java similarity index 100% rename from jbmc/regression/jbmc/array-cell-sensitivity2/Test.java rename to jbmc/regression/jbmc/array-cell-sensitivity2/src/main/java/Test.java diff --git a/jbmc/regression/jbmc/array-cell-sensitivity2/test.desc b/jbmc/regression/jbmc/array-cell-sensitivity2/test.desc index ce987c5326b..57597c18830 100644 --- a/jbmc/regression/jbmc/array-cell-sensitivity2/test.desc +++ b/jbmc/regression/jbmc/array-cell-sensitivity2/test.desc @@ -1,6 +1,6 @@ CORE Test ---function Test.main --show-vcc +--function Test.main --show-vcc -cp target/classes symex_dynamic::dynamic_object\$3#3\.\.data = symex_dynamic::dynamic_object\$1#3\.\.data = ^EXIT=0$ diff --git a/jbmc/regression/jbmc/pom.xml b/jbmc/regression/jbmc/pom.xml index 64e35e3493d..a2fb9fbb6ad 100644 --- a/jbmc/regression/jbmc/pom.xml +++ b/jbmc/regression/jbmc/pom.xml @@ -30,6 +30,7 @@ array1 array2 array-cell-sensitivity1 + array-cell-sensitivity2 classpath-jar-load-whole-jar From 753e24c36275131c51aa6399e45ef8fd6076765a Mon Sep 17 00:00:00 2001 From: Peter Schrammel Date: Thu, 2 Jan 2025 19:16:57 +0100 Subject: [PATCH 16/47] Compile jbmc/array-cell-sensitivity-negative-size test sources Add pom.xml for compilation, move sources, remove obsolete pre-compiled class files. --- .../Test.class | Bin 644 -> 0 bytes .../pom.xml | 30 ++++++++++++++++++ .../{ => src/main/java}/Test.java | 0 .../test.desc | 2 +- jbmc/regression/jbmc/pom.xml | 1 + 5 files changed, 32 insertions(+), 1 deletion(-) delete mode 100644 jbmc/regression/jbmc/array-cell-sensitivity-negative-size/Test.class create mode 100644 jbmc/regression/jbmc/array-cell-sensitivity-negative-size/pom.xml rename jbmc/regression/jbmc/array-cell-sensitivity-negative-size/{ => src/main/java}/Test.java (100%) diff --git a/jbmc/regression/jbmc/array-cell-sensitivity-negative-size/Test.class b/jbmc/regression/jbmc/array-cell-sensitivity-negative-size/Test.class deleted file mode 100644 index 1811bee9941c1d9b5fd9569b86a1e22c53e66eae..0000000000000000000000000000000000000000 GIT binary patch literal 0 HcmV?d00001 literal 644 zcmZWmK~EDw6#ia!x6>{Qv;}b$0Tm8V6S;7c7y&Ucsdy+ck=u0pQU}TwXSYQBDf|J> zXd;P5y>aj#c`?3Og(jLwX5PH-y>Gtn&5vK7zX4doVu&hkD#TSN+)}t5!gu#sg*zeU zFt4ycm|D_V#x^&DG<#|?-RX0eKzoGpx=Bs`nBXn1ydwBpgDw*$TPEe5;bDjEt}7-4 z$s0}%2s6vAeSNG~`#SBdK2LM*v3=w^$J@D14qoV^qCo@@D(gxAFMHS?3~j>CjN_{A za+W`IG!Y_<6YBp_MhG!Rh)2N2m4R(*2bQojf_Av4b92la*6NeCdC%ML5F^R`6XU1~(`bn{t4+W4J?Fo;PkponVok)p1knQ;luSd=3cPqzVQNC6>1(BHg(RTfP@hma dh4RnfdmrIB)qlvZR6CLYrRa(CcB6o2egh?DeO>?n diff --git a/jbmc/regression/jbmc/array-cell-sensitivity-negative-size/pom.xml b/jbmc/regression/jbmc/array-cell-sensitivity-negative-size/pom.xml new file mode 100644 index 00000000000..37b3521a42e --- /dev/null +++ b/jbmc/regression/jbmc/array-cell-sensitivity-negative-size/pom.xml @@ -0,0 +1,30 @@ + + + 4.0.0 + org.cprover.regression + regression.jbmc.array-cell-sensitivity-negative-size + 1.0-SNAPSHOT + + + org.cprover.regression + regression.jbmc + 1.0-SNAPSHOT + + + + + + maven-jar-plugin + + + default-jar + none + + + + + + + diff --git a/jbmc/regression/jbmc/array-cell-sensitivity-negative-size/Test.java b/jbmc/regression/jbmc/array-cell-sensitivity-negative-size/src/main/java/Test.java similarity index 100% rename from jbmc/regression/jbmc/array-cell-sensitivity-negative-size/Test.java rename to jbmc/regression/jbmc/array-cell-sensitivity-negative-size/src/main/java/Test.java diff --git a/jbmc/regression/jbmc/array-cell-sensitivity-negative-size/test.desc b/jbmc/regression/jbmc/array-cell-sensitivity-negative-size/test.desc index 605cd7040d4..2e1d8af1f57 100644 --- a/jbmc/regression/jbmc/array-cell-sensitivity-negative-size/test.desc +++ b/jbmc/regression/jbmc/array-cell-sensitivity-negative-size/test.desc @@ -1,6 +1,6 @@ CORE Test ---function Test.check +--function Test.check -cp target/classes line 5 Array size should be >= 0: FAILURE ^EXIT=10$ ^SIGNAL=0$ diff --git a/jbmc/regression/jbmc/pom.xml b/jbmc/regression/jbmc/pom.xml index a2fb9fbb6ad..0b27f5213f7 100644 --- a/jbmc/regression/jbmc/pom.xml +++ b/jbmc/regression/jbmc/pom.xml @@ -31,6 +31,7 @@ array2 array-cell-sensitivity1 array-cell-sensitivity2 + array-cell-sensitivity-negative-size classpath-jar-load-whole-jar From bc0df89213c7fa13a1bf1b0701d5a35efc9a1ac0 Mon Sep 17 00:00:00 2001 From: Peter Schrammel Date: Thu, 2 Jan 2025 19:18:05 +0100 Subject: [PATCH 17/47] Compile jbmc/array-cell-sensitivity-static-fields test sources Add pom.xml for compilation, move sources, remove obsolete pre-compiled class files. --- .../Test.class | Bin 862 -> 0 bytes .../Util.class | Bin 321 -> 0 bytes .../pom.xml | 30 ++++++++++++++++++ .../{ => src/main/java}/Test.java | 0 .../test-char-array-ref-static-values.desc | 2 +- .../test-char-array-ref.desc | 2 +- .../test-char-array-static-values.desc | 2 +- .../test-char-array1.desc | 2 +- jbmc/regression/jbmc/pom.xml | 1 + 9 files changed, 35 insertions(+), 4 deletions(-) delete mode 100644 jbmc/regression/jbmc/array-cell-sensitivity-static-fields/Test.class delete mode 100644 jbmc/regression/jbmc/array-cell-sensitivity-static-fields/Util.class create mode 100644 jbmc/regression/jbmc/array-cell-sensitivity-static-fields/pom.xml rename jbmc/regression/jbmc/array-cell-sensitivity-static-fields/{ => src/main/java}/Test.java (100%) diff --git a/jbmc/regression/jbmc/array-cell-sensitivity-static-fields/Test.class b/jbmc/regression/jbmc/array-cell-sensitivity-static-fields/Test.class deleted file mode 100644 index a41151d6a03b4e4b041718a03994d54bd215b4cd..0000000000000000000000000000000000000000 GIT binary patch literal 0 HcmV?d00001 literal 862 zcmZ9KOK;Oq5QWe6BTgK*b<#Esp-JciND870vaAqMC=!T=L|Y`v%CRrt5)x!PAXfa3 zZeYh2h(r-cu;)i1&UM=))RyO7AJ3inX2yU1{`du;g{wAfoX^3+vNBZ*H5lf# zX5f%c9kp=D!DTcoG#zZ({e%Tfq)v~u3zPyGhmj1%fk~eX`GJMA55`^+ z_5@5-14XlOhc&X{7H0zJ$SF+ja*70S%Zixq2ACfO+9KboTm@Hi;|SslH*7s^CKdBM zynsdSmFrs`RoC`cXgZ%vYme4&B^Uh=i%M>}!3X4j!gz87^Y^sg{!iCFGmw_1D#7Hw zNa}e~EuhJSZIpN`R;{^2h@~;a`w2wmEQCtm{)j@Fc5MQYVx8(!a8nR9whgGL-J{p=vatIXBf1&ZTaZe=M<>k^lez diff --git a/jbmc/regression/jbmc/array-cell-sensitivity-static-fields/Util.class b/jbmc/regression/jbmc/array-cell-sensitivity-static-fields/Util.class deleted file mode 100644 index 4eeec1101214289a09a31022d09de403d7ba6b19..0000000000000000000000000000000000000000 GIT binary patch literal 0 HcmV?d00001 literal 321 zcmX9&%}T>y5S;yzG@7P1tsqz)5Oyc*kJIl=O?0)>bz601r-GPA>8&w;gptP5alk7lXG+So^Gnib&f@(Jz z$0v)MVLa>WVM@k|uJmk9Y#y}+fuPdMbaZ{Jr-g2#CUAO_#Vm>sle~YqAJ4O$k-pU~ zOjvXdvm_OGIn_z^__A|49K}&4P=f$lP`oOCiopT!G*+8LAzIrnkY^SGo4Hhw+=3;> ze{0CG++w5gW_68yzwv-t+xN78ejnZ`dHnrsKT%eN!5TM!?IwSj^(t|libK|g`bNn{ NS-w!Gxm!$C{s6BCG%WxC diff --git a/jbmc/regression/jbmc/array-cell-sensitivity-static-fields/pom.xml b/jbmc/regression/jbmc/array-cell-sensitivity-static-fields/pom.xml new file mode 100644 index 00000000000..a39539c7970 --- /dev/null +++ b/jbmc/regression/jbmc/array-cell-sensitivity-static-fields/pom.xml @@ -0,0 +1,30 @@ + + + 4.0.0 + org.cprover.regression + regression.jbmc.array-cell-sensitivity-static-fields + 1.0-SNAPSHOT + + + org.cprover.regression + regression.jbmc + 1.0-SNAPSHOT + + + + + + maven-jar-plugin + + + default-jar + none + + + + + + + diff --git a/jbmc/regression/jbmc/array-cell-sensitivity-static-fields/Test.java b/jbmc/regression/jbmc/array-cell-sensitivity-static-fields/src/main/java/Test.java similarity index 100% rename from jbmc/regression/jbmc/array-cell-sensitivity-static-fields/Test.java rename to jbmc/regression/jbmc/array-cell-sensitivity-static-fields/src/main/java/Test.java diff --git a/jbmc/regression/jbmc/array-cell-sensitivity-static-fields/test-char-array-ref-static-values.desc b/jbmc/regression/jbmc/array-cell-sensitivity-static-fields/test-char-array-ref-static-values.desc index 6cb0a122f1e..51515b0e110 100644 --- a/jbmc/regression/jbmc/array-cell-sensitivity-static-fields/test-char-array-ref-static-values.desc +++ b/jbmc/regression/jbmc/array-cell-sensitivity-static-fields/test-char-array-ref-static-values.desc @@ -1,6 +1,6 @@ CORE symex-driven-lazy-loading-expected-failure Test ---function Test.charArrayRef --property 'java::Test.charArrayRef:()[C.assertion.2' --static-values static-values.json +--function Test.charArrayRef --property 'java::Test.charArrayRef:()[C.assertion.2' --static-values static-values.json -cp target/classes Generated 0 VCC[(]s[)], 0 remaining after simplification assertion at file Test.java line 31 .*: SUCCESS ^EXIT=0$ diff --git a/jbmc/regression/jbmc/array-cell-sensitivity-static-fields/test-char-array-ref.desc b/jbmc/regression/jbmc/array-cell-sensitivity-static-fields/test-char-array-ref.desc index 4598fef0877..2dacde1593d 100644 --- a/jbmc/regression/jbmc/array-cell-sensitivity-static-fields/test-char-array-ref.desc +++ b/jbmc/regression/jbmc/array-cell-sensitivity-static-fields/test-char-array-ref.desc @@ -1,6 +1,6 @@ CORE symex-driven-lazy-loading-expected-failure Test ---function Test.charArrayRef --property 'java::Test.charArrayRef:()[C.assertion.1' +--function Test.charArrayRef --property 'java::Test.charArrayRef:()[C.assertion.1' -cp target/classes Generated 0 VCC[(]s[)], 0 remaining after simplification assertion at file Test.java line 29 .*: SUCCESS ^EXIT=0$ diff --git a/jbmc/regression/jbmc/array-cell-sensitivity-static-fields/test-char-array-static-values.desc b/jbmc/regression/jbmc/array-cell-sensitivity-static-fields/test-char-array-static-values.desc index a31e295710f..cf6668f17fd 100644 --- a/jbmc/regression/jbmc/array-cell-sensitivity-static-fields/test-char-array-static-values.desc +++ b/jbmc/regression/jbmc/array-cell-sensitivity-static-fields/test-char-array-static-values.desc @@ -1,6 +1,6 @@ CORE symex-driven-lazy-loading-expected-failure Test ---function Test.charArray --property 'java::Test.charArray:()[C.assertion.2' --static-values static-values.json +--function Test.charArray --property 'java::Test.charArray:()[C.assertion.2' --static-values static-values.json -cp target/classes Generated 0 VCC[(]s[)], 0 remaining after simplification assertion at file Test.java line 21 .*: SUCCESS ^EXIT=0$ diff --git a/jbmc/regression/jbmc/array-cell-sensitivity-static-fields/test-char-array1.desc b/jbmc/regression/jbmc/array-cell-sensitivity-static-fields/test-char-array1.desc index e70aaf0604e..7a28f184269 100644 --- a/jbmc/regression/jbmc/array-cell-sensitivity-static-fields/test-char-array1.desc +++ b/jbmc/regression/jbmc/array-cell-sensitivity-static-fields/test-char-array1.desc @@ -1,6 +1,6 @@ CORE symex-driven-lazy-loading-expected-failure Test ---function Test.charArray --property 'java::Test.charArray:()[C.assertion.1' +--function Test.charArray --property 'java::Test.charArray:()[C.assertion.1' -cp target/classes Generated 0 VCC[(]s[)], 0 remaining after simplification assertion at file Test.java line 20 .*: SUCCESS ^EXIT=0$ diff --git a/jbmc/regression/jbmc/pom.xml b/jbmc/regression/jbmc/pom.xml index 0b27f5213f7..d34557cafc2 100644 --- a/jbmc/regression/jbmc/pom.xml +++ b/jbmc/regression/jbmc/pom.xml @@ -32,6 +32,7 @@ array-cell-sensitivity1 array-cell-sensitivity2 array-cell-sensitivity-negative-size + array-cell-sensitivity-static-fields classpath-jar-load-whole-jar From dde14a4aead5a40b90cf162eb1f981401b63d92d Mon Sep 17 00:00:00 2001 From: Peter Schrammel Date: Thu, 2 Jan 2025 19:18:53 +0100 Subject: [PATCH 18/47] Compile jbmc/array-clone test sources Add pom.xml for compilation, move sources, remove obsolete pre-compiled class files. --- .../jbmc/array-clone/ArrayClone.class | Bin 2879 -> 0 bytes jbmc/regression/jbmc/array-clone/pom.xml | 30 ++++++++++++++++++ .../{ => src/main/java}/ArrayClone.java | 0 .../jbmc/array-clone/testBoolean.desc | 2 +- .../regression/jbmc/array-clone/testByte.desc | 2 +- .../jbmc/array-clone/testDouble.desc | 2 +- .../jbmc/array-clone/testFloat.desc | 2 +- jbmc/regression/jbmc/array-clone/testInt.desc | 2 +- .../regression/jbmc/array-clone/testLong.desc | 2 +- .../jbmc/array-clone/testObject.desc | 2 +- .../jbmc/array-clone/testReference.desc | 2 +- .../jbmc/array-clone/testShort.desc | 2 +- jbmc/regression/jbmc/pom.xml | 1 + 13 files changed, 40 insertions(+), 9 deletions(-) delete mode 100644 jbmc/regression/jbmc/array-clone/ArrayClone.class create mode 100644 jbmc/regression/jbmc/array-clone/pom.xml rename jbmc/regression/jbmc/array-clone/{ => src/main/java}/ArrayClone.java (100%) diff --git a/jbmc/regression/jbmc/array-clone/ArrayClone.class b/jbmc/regression/jbmc/array-clone/ArrayClone.class deleted file mode 100644 index 2e985bf8761d908185f5919bc27726c84ec54244..0000000000000000000000000000000000000000 GIT binary patch literal 0 HcmV?d00001 literal 2879 zcmchZ-BTM?7{;H?ZnCh1kMP}6P%3R9Tayqzq<}3DK%t?01gRkx&Jxx(G|f68sQo{5 z9DC!HdTpI)XDni_bsTT~XLNkdZnB9avsaEgXZD=)o_F`Wzw^B3?Ed=qPZt2D@qva` zEU8%5;KP!J6(m%ITiIDvv8F*4gXp8KSowid#tW!i_ z1u=^26119`*%5?}-5}n;n-T_V@XJ*t*NR1}$e?ON&blyxm^(}xW(;$L>A{3xE~wZG zB87bkz2g(jRvo z_routl;KalK;SvL!x#F+H)wkem3}S1*v8(l9M|Rew+&_`t}6}ZuCV@H%~QlH+wqQY zcZ&8ED1-}Omi;ZX;F$4##vLa(`WfpLe1r*v*&D?}Y8NKkZT32#{3T@Yv-J0O^QpI+ zQnm`pRz@$`luk=fYGt(jPn7MX=wSR^qzsX=o0L7I?7c)8aVaC0DBD!DIh0YC@;9!W z(DI4@yd^Cw`)S3$FTjFjw0nb1>GD*gs>+nEG?=~R8(^vp65}c*8p0B;QKDg-V8jIr z+VaI1X0I(@tR8GaMLUZFHrWh}>L~{VI}l(UWgelPc{!uYGflu|bfv-U4K_-!>kN5} zU^fVMlfmC2*!U%|xC<7)1lFmd(*c`m2Br~gn_$}ltgDQWH&{fMBTc{}y3%0w2Ga?4 zn_v-wMF|!o*d)Q?m%yf7u<1)+Ar&D9Y{muqqjIcR{`0o9tnH+gUUcsWwB9oMJka{W za#WY2UwmCVB5Z;C!b((E8tvY2Gu&mfJT>NcPTWBP^T=QU1uVL79WV$!OSpcd=`~vq zr>p2=85j_!$vZCG@0ES_)PEjG%fa2W(!MLu`pX#bMvLik?8_!-FZcEf{ zh2bZ#j8%rehCJ3?w4jYPXX_@==IYV7(*{@^v^y?Zoo;Gc?%Wf)4eklJt7Qy%!%gb) z + + 4.0.0 + org.cprover.regression + regression.jbmc.array-clone + 1.0-SNAPSHOT + + + org.cprover.regression + regression.jbmc + 1.0-SNAPSHOT + + + + + + maven-jar-plugin + + + default-jar + none + + + + + + + diff --git a/jbmc/regression/jbmc/array-clone/ArrayClone.java b/jbmc/regression/jbmc/array-clone/src/main/java/ArrayClone.java similarity index 100% rename from jbmc/regression/jbmc/array-clone/ArrayClone.java rename to jbmc/regression/jbmc/array-clone/src/main/java/ArrayClone.java diff --git a/jbmc/regression/jbmc/array-clone/testBoolean.desc b/jbmc/regression/jbmc/array-clone/testBoolean.desc index 14819080eb0..724c42bf5d1 100644 --- a/jbmc/regression/jbmc/array-clone/testBoolean.desc +++ b/jbmc/regression/jbmc/array-clone/testBoolean.desc @@ -1,6 +1,6 @@ CORE ArrayClone ---function ArrayClone.cloneBooleanArray +--function ArrayClone.cloneBooleanArray -cp target/classes ^EXIT=0$ ^SIGNAL=0$ ^VERIFICATION SUCCESSFUL$ diff --git a/jbmc/regression/jbmc/array-clone/testByte.desc b/jbmc/regression/jbmc/array-clone/testByte.desc index 2e0d2012dd4..0df7b22c221 100644 --- a/jbmc/regression/jbmc/array-clone/testByte.desc +++ b/jbmc/regression/jbmc/array-clone/testByte.desc @@ -1,6 +1,6 @@ CORE ArrayClone ---function ArrayClone.cloneByteArray +--function ArrayClone.cloneByteArray -cp target/classes ^EXIT=0$ ^SIGNAL=0$ ^VERIFICATION SUCCESSFUL$ diff --git a/jbmc/regression/jbmc/array-clone/testDouble.desc b/jbmc/regression/jbmc/array-clone/testDouble.desc index 58d52f46a4f..3a49658300f 100644 --- a/jbmc/regression/jbmc/array-clone/testDouble.desc +++ b/jbmc/regression/jbmc/array-clone/testDouble.desc @@ -1,6 +1,6 @@ CORE ArrayClone ---function ArrayClone.cloneDoubleArray +--function ArrayClone.cloneDoubleArray -cp target/classes ^EXIT=0$ ^SIGNAL=0$ ^VERIFICATION SUCCESSFUL$ diff --git a/jbmc/regression/jbmc/array-clone/testFloat.desc b/jbmc/regression/jbmc/array-clone/testFloat.desc index 73117b32e43..23188c99cb6 100644 --- a/jbmc/regression/jbmc/array-clone/testFloat.desc +++ b/jbmc/regression/jbmc/array-clone/testFloat.desc @@ -1,6 +1,6 @@ CORE ArrayClone ---function ArrayClone.cloneFloatArray +--function ArrayClone.cloneFloatArray -cp target/classes ^EXIT=0$ ^SIGNAL=0$ ^VERIFICATION SUCCESSFUL$ diff --git a/jbmc/regression/jbmc/array-clone/testInt.desc b/jbmc/regression/jbmc/array-clone/testInt.desc index ea0b0552131..c091b6f5778 100644 --- a/jbmc/regression/jbmc/array-clone/testInt.desc +++ b/jbmc/regression/jbmc/array-clone/testInt.desc @@ -1,6 +1,6 @@ CORE ArrayClone ---function ArrayClone.cloneIntArray +--function ArrayClone.cloneIntArray -cp target/classes ^EXIT=0$ ^SIGNAL=0$ ^VERIFICATION SUCCESSFUL$ diff --git a/jbmc/regression/jbmc/array-clone/testLong.desc b/jbmc/regression/jbmc/array-clone/testLong.desc index e1904c51acf..7f242d279c6 100644 --- a/jbmc/regression/jbmc/array-clone/testLong.desc +++ b/jbmc/regression/jbmc/array-clone/testLong.desc @@ -1,6 +1,6 @@ CORE ArrayClone ---function ArrayClone.cloneLongArray +--function ArrayClone.cloneLongArray -cp target/classes ^EXIT=0$ ^SIGNAL=0$ ^VERIFICATION SUCCESSFUL$ diff --git a/jbmc/regression/jbmc/array-clone/testObject.desc b/jbmc/regression/jbmc/array-clone/testObject.desc index ae7d25c7587..d0dcc481b5b 100644 --- a/jbmc/regression/jbmc/array-clone/testObject.desc +++ b/jbmc/regression/jbmc/array-clone/testObject.desc @@ -1,6 +1,6 @@ CORE ArrayClone ---function ArrayClone.cloneObjectArray +--function ArrayClone.cloneObjectArray -cp target/classes ^EXIT=0$ ^SIGNAL=0$ ^VERIFICATION SUCCESSFUL$ diff --git a/jbmc/regression/jbmc/array-clone/testReference.desc b/jbmc/regression/jbmc/array-clone/testReference.desc index bd1ed3407d3..0d258793c34 100644 --- a/jbmc/regression/jbmc/array-clone/testReference.desc +++ b/jbmc/regression/jbmc/array-clone/testReference.desc @@ -1,6 +1,6 @@ CORE ArrayClone ---function ArrayClone.cloneReferenceArray +--function ArrayClone.cloneReferenceArray -cp target/classes ^EXIT=0$ ^SIGNAL=0$ ^VERIFICATION SUCCESSFUL$ diff --git a/jbmc/regression/jbmc/array-clone/testShort.desc b/jbmc/regression/jbmc/array-clone/testShort.desc index 18341d3f9b3..5d7e0d7e937 100644 --- a/jbmc/regression/jbmc/array-clone/testShort.desc +++ b/jbmc/regression/jbmc/array-clone/testShort.desc @@ -1,6 +1,6 @@ CORE ArrayClone ---function ArrayClone.cloneShortArray +--function ArrayClone.cloneShortArray -cp target/classes ^EXIT=0$ ^SIGNAL=0$ ^VERIFICATION SUCCESSFUL$ diff --git a/jbmc/regression/jbmc/pom.xml b/jbmc/regression/jbmc/pom.xml index d34557cafc2..4bcbc30ff0a 100644 --- a/jbmc/regression/jbmc/pom.xml +++ b/jbmc/regression/jbmc/pom.xml @@ -33,6 +33,7 @@ array-cell-sensitivity2 array-cell-sensitivity-negative-size array-cell-sensitivity-static-fields + array-clone classpath-jar-load-whole-jar From fef2fa69b36060ebef90dd8639d60cd5e86d7491 Mon Sep 17 00:00:00 2001 From: Peter Schrammel Date: Thu, 2 Jan 2025 19:19:43 +0100 Subject: [PATCH 19/47] Compile jbmc/array_nonconstsize_nonconstaccess test sources Add pom.xml for compilation, move sources, remove obsolete pre-compiled class files. --- .../array_nonconstsize_nonconstaccess/A.class | Bin 192 -> 0 bytes .../FloatMultidim1.class | Bin 609 -> 0 bytes .../FloatMultidim2.class | Bin 609 -> 0 bytes .../RefMultidim1.class | Bin 658 -> 0 bytes .../RefMultidim2.class | Bin 658 -> 0 bytes .../RefMultidimConstsize.class | Bin 626 -> 0 bytes .../RefSingledim.class | Bin 647 -> 0 bytes .../array_nonconstsize_nonconstaccess/pom.xml | 30 ++++++++++++++++++ .../{ => src/main/java}/A.java | 0 .../{ => src/main/java}/FloatMultidim1.java | 0 .../{ => src/main/java}/FloatMultidim2.java | 0 .../{ => src/main/java}/RefMultidim1.java | 0 .../{ => src/main/java}/RefMultidim2.java | 0 .../main/java}/RefMultidimConstsize.java | 0 .../{ => src/main/java}/RefSingledim.java | 0 .../test_float_multidim_1.desc | 2 +- .../test_float_multidim_2.desc | 2 +- .../test_ref_multidim_1.desc | 2 +- .../test_ref_multidim_2.desc | 2 +- .../test_ref_multidim_constsize.desc | 2 +- .../test_ref_singledim.desc | 2 +- jbmc/regression/jbmc/pom.xml | 1 + 22 files changed, 37 insertions(+), 6 deletions(-) delete mode 100644 jbmc/regression/jbmc/array_nonconstsize_nonconstaccess/A.class delete mode 100644 jbmc/regression/jbmc/array_nonconstsize_nonconstaccess/FloatMultidim1.class delete mode 100644 jbmc/regression/jbmc/array_nonconstsize_nonconstaccess/FloatMultidim2.class delete mode 100644 jbmc/regression/jbmc/array_nonconstsize_nonconstaccess/RefMultidim1.class delete mode 100644 jbmc/regression/jbmc/array_nonconstsize_nonconstaccess/RefMultidim2.class delete mode 100644 jbmc/regression/jbmc/array_nonconstsize_nonconstaccess/RefMultidimConstsize.class delete mode 100644 jbmc/regression/jbmc/array_nonconstsize_nonconstaccess/RefSingledim.class create mode 100644 jbmc/regression/jbmc/array_nonconstsize_nonconstaccess/pom.xml rename jbmc/regression/jbmc/array_nonconstsize_nonconstaccess/{ => src/main/java}/A.java (100%) rename jbmc/regression/jbmc/array_nonconstsize_nonconstaccess/{ => src/main/java}/FloatMultidim1.java (100%) rename jbmc/regression/jbmc/array_nonconstsize_nonconstaccess/{ => src/main/java}/FloatMultidim2.java (100%) rename jbmc/regression/jbmc/array_nonconstsize_nonconstaccess/{ => src/main/java}/RefMultidim1.java (100%) rename jbmc/regression/jbmc/array_nonconstsize_nonconstaccess/{ => src/main/java}/RefMultidim2.java (100%) rename jbmc/regression/jbmc/array_nonconstsize_nonconstaccess/{ => src/main/java}/RefMultidimConstsize.java (100%) rename jbmc/regression/jbmc/array_nonconstsize_nonconstaccess/{ => src/main/java}/RefSingledim.java (100%) diff --git a/jbmc/regression/jbmc/array_nonconstsize_nonconstaccess/A.class b/jbmc/regression/jbmc/array_nonconstsize_nonconstaccess/A.class deleted file mode 100644 index 14f1d91ebe75e467d02a40f1a87fcb2b7db21a55..0000000000000000000000000000000000000000 GIT binary patch literal 0 HcmV?d00001 literal 192 zcmX^0Z`VEs1_l!bel7-P1|D_>UUmjPMh3=2Aa-M9V6(~0%Pg^DWMJ0N3}a+qan4Uk zWn|#@$;?ajE6q(xEec6Y$^nXS1?QI*C8xS&f;eoBdRd8Oi98H!4D3K-92pq|Kz#k2 z#JqHU|D>$cnI_(lQ-h diff --git a/jbmc/regression/jbmc/array_nonconstsize_nonconstaccess/FloatMultidim1.class b/jbmc/regression/jbmc/array_nonconstsize_nonconstaccess/FloatMultidim1.class deleted file mode 100644 index ba36f3ebae809d73a9451f7d3c3772823678e10c..0000000000000000000000000000000000000000 GIT binary patch literal 0 HcmV?d00001 literal 609 zcmY*WT}vBL5IwVdH@mKDK8zn}W10rUsszR2OR0p4HXt-D#Zss~ZL(LncFoG}#{b}7 z@WF>7_-b3IV4?M;edtdTDV-a?=*!H`%$YOi-2L-{cZd=Ch zG?=kljGbPa+1zXrhSpQR^Reac-3*$O?szB{7%{}b4#czA>=A%DN~roAIODQmuOt%Pis zFc!!}#WJ{KW!Y(u2kdnNHGVCJACU4Tt%JWzkQT>rh^q=`;%v>Hfj(;>vK%x0rXJ;x z=cu6vyec?9rwbUZ@)2rf=MyH%)-M=bi(@#VaRSS1)GJSg_x20SL*(keG58(g!x^lf z^;2Fq`Uj?1jn-l@WtQV8Z2pf9s;sfb>Yi}-86Ph&Di3jmstw}`M3=A%j2pglu-KOh i6oxb3U?0L3ClKaWnA*+tv0FEq%!1*)(8h}W@yI`IYHSez diff --git a/jbmc/regression/jbmc/array_nonconstsize_nonconstaccess/FloatMultidim2.class b/jbmc/regression/jbmc/array_nonconstsize_nonconstaccess/FloatMultidim2.class deleted file mode 100644 index a2ca10913d17524e6b348795d1049d3ca8f19b05..0000000000000000000000000000000000000000 GIT binary patch literal 0 HcmV?d00001 literal 609 zcmY*WT}vBL5IwVdH@mKDK1|hUOw&NAT7rW3QYyis282ctOQG>;lf9K|*R1Sr`XBli zeCR_d_}ULpXuPtmLKzUKO~@>(o=O`8b9U}EL99lBB;;PIp4{vobY%QW zgBkmlv9lX!GvU4XQN4P zjvD%bR|V(i^czO2{1LUX^9j>d`40@P#b-F8aSY3B)Wu@O+x`ag2)X)S4F809a|-KM z{R^)fg9A@kjn-l@WtQU@Z2pf9s;sfb>Snn6jE@%>m4~=M)rN5aqH|aU#*N-OSQ0T4K_JjZ&6NIg2dL zNK`yX1D^FTg>w?qgwdHGNmQKbZYQ~;lb{u;kU$%R%(Cw2v_`OJ=bjM6N;g!5{JQR_ z2fdw^iXR&?bGHcY?AqMs=6d}WVW^n~?dOf)#Q=7f+tEPCYj%5aTdiudt@uc7HF{C1 zL%nn3+IH|V@G*=$!5Iiq-N$)c@Zn>KP%?~#DCj&}s2>@=8^_(4;Qy~AG2`PRE)fbR zJ07;SRXb&?0gqJsJl5tEX^#O8zkzAKz8qgK6-vepcQ(kl+eCIZ{+J>@ zh|pI*(1Hc^MIZc0Qp7tkZDpA|clMk)bI#1KKVQBASjJ@^Ig|uW3rzd4QOa^DXOYDj zfr<}dz_UJPa86*BFg_O~iHcL*>n68#60{=~5@>^vSU)}+%1APe{W%PbG>nsFw#nc&huvQVhDRHooFcJw|f1!qt>+9R(zzkn*Au% zq28%o+YVj^5~Iiy+@TOPB+lc4gv1D;WEe|P(0#VlI5K=Ej(agd{;wo3Cvg#%2!)d! z58Kcg8KoPUF54jkvo83$op1($7}WQLdBx+SBm(t$mIl zah0v#VAFTm$pkYCa1JpeU>$iR^Cr(4XQT z=yO|CP|zoR@IP64C#ZQT!`wS}&Y5%1-21#8-Jx?}dp9)Nzd)C$ah= z-yiwkeGe~?CD_g8R&|ZFs~+Ys@4>?mp{N-vq2D=NsXm$h6h+;LF!Db|fdvnXcumL+ zUVdpE$#%lhKJQKb&;Y81JPX2DAY&ED;JF9?D(Nx6gV@I`k21rfrd(0G;*$x|t~uto zDsd*x_PYzvFHJa>3j?J*mvSBs0)a^v zIgM0Y+{7(`+k~;{FiB*bs(zF_R!P|I$u5C53AtqzskBZo=NDcQtkr&35(?`olFtUa zZ5hANWae%W#Qf8R*XxakgyB{icHT6@y$ltYA~?&P-ajd~)gQzixu*1B@wwb;sc4%w zs@?lL;oH!|Fh*Fh;o%PMdKiL7C~0J|7e?EQjSH(!;k~YPECO9ibxEAqTld~%pJeXvXq$yilfdU^7|0h0W9+?Y@O?T;YBVjX2bASbi|1a GzWx`5{%?-} diff --git a/jbmc/regression/jbmc/array_nonconstsize_nonconstaccess/pom.xml b/jbmc/regression/jbmc/array_nonconstsize_nonconstaccess/pom.xml new file mode 100644 index 00000000000..425ace656cc --- /dev/null +++ b/jbmc/regression/jbmc/array_nonconstsize_nonconstaccess/pom.xml @@ -0,0 +1,30 @@ + + + 4.0.0 + org.cprover.regression + regression.jbmc.array_nonconstsize_nonconstaccess + 1.0-SNAPSHOT + + + org.cprover.regression + regression.jbmc + 1.0-SNAPSHOT + + + + + + maven-jar-plugin + + + default-jar + none + + + + + + + diff --git a/jbmc/regression/jbmc/array_nonconstsize_nonconstaccess/A.java b/jbmc/regression/jbmc/array_nonconstsize_nonconstaccess/src/main/java/A.java similarity index 100% rename from jbmc/regression/jbmc/array_nonconstsize_nonconstaccess/A.java rename to jbmc/regression/jbmc/array_nonconstsize_nonconstaccess/src/main/java/A.java diff --git a/jbmc/regression/jbmc/array_nonconstsize_nonconstaccess/FloatMultidim1.java b/jbmc/regression/jbmc/array_nonconstsize_nonconstaccess/src/main/java/FloatMultidim1.java similarity index 100% rename from jbmc/regression/jbmc/array_nonconstsize_nonconstaccess/FloatMultidim1.java rename to jbmc/regression/jbmc/array_nonconstsize_nonconstaccess/src/main/java/FloatMultidim1.java diff --git a/jbmc/regression/jbmc/array_nonconstsize_nonconstaccess/FloatMultidim2.java b/jbmc/regression/jbmc/array_nonconstsize_nonconstaccess/src/main/java/FloatMultidim2.java similarity index 100% rename from jbmc/regression/jbmc/array_nonconstsize_nonconstaccess/FloatMultidim2.java rename to jbmc/regression/jbmc/array_nonconstsize_nonconstaccess/src/main/java/FloatMultidim2.java diff --git a/jbmc/regression/jbmc/array_nonconstsize_nonconstaccess/RefMultidim1.java b/jbmc/regression/jbmc/array_nonconstsize_nonconstaccess/src/main/java/RefMultidim1.java similarity index 100% rename from jbmc/regression/jbmc/array_nonconstsize_nonconstaccess/RefMultidim1.java rename to jbmc/regression/jbmc/array_nonconstsize_nonconstaccess/src/main/java/RefMultidim1.java diff --git a/jbmc/regression/jbmc/array_nonconstsize_nonconstaccess/RefMultidim2.java b/jbmc/regression/jbmc/array_nonconstsize_nonconstaccess/src/main/java/RefMultidim2.java similarity index 100% rename from jbmc/regression/jbmc/array_nonconstsize_nonconstaccess/RefMultidim2.java rename to jbmc/regression/jbmc/array_nonconstsize_nonconstaccess/src/main/java/RefMultidim2.java diff --git a/jbmc/regression/jbmc/array_nonconstsize_nonconstaccess/RefMultidimConstsize.java b/jbmc/regression/jbmc/array_nonconstsize_nonconstaccess/src/main/java/RefMultidimConstsize.java similarity index 100% rename from jbmc/regression/jbmc/array_nonconstsize_nonconstaccess/RefMultidimConstsize.java rename to jbmc/regression/jbmc/array_nonconstsize_nonconstaccess/src/main/java/RefMultidimConstsize.java diff --git a/jbmc/regression/jbmc/array_nonconstsize_nonconstaccess/RefSingledim.java b/jbmc/regression/jbmc/array_nonconstsize_nonconstaccess/src/main/java/RefSingledim.java similarity index 100% rename from jbmc/regression/jbmc/array_nonconstsize_nonconstaccess/RefSingledim.java rename to jbmc/regression/jbmc/array_nonconstsize_nonconstaccess/src/main/java/RefSingledim.java diff --git a/jbmc/regression/jbmc/array_nonconstsize_nonconstaccess/test_float_multidim_1.desc b/jbmc/regression/jbmc/array_nonconstsize_nonconstaccess/test_float_multidim_1.desc index 47ea2e8dc8e..05a7550ab70 100644 --- a/jbmc/regression/jbmc/array_nonconstsize_nonconstaccess/test_float_multidim_1.desc +++ b/jbmc/regression/jbmc/array_nonconstsize_nonconstaccess/test_float_multidim_1.desc @@ -1,6 +1,6 @@ CORE FloatMultidim1 ---function FloatMultidim1.f --unwind 3 +--function FloatMultidim1.f --unwind 3 -cp target/classes ^EXIT=10$ ^SIGNAL=0$ assertion at file FloatMultidim1.java line 14 .*: FAILURE diff --git a/jbmc/regression/jbmc/array_nonconstsize_nonconstaccess/test_float_multidim_2.desc b/jbmc/regression/jbmc/array_nonconstsize_nonconstaccess/test_float_multidim_2.desc index 3fa0879cae4..fae3a56bf8c 100644 --- a/jbmc/regression/jbmc/array_nonconstsize_nonconstaccess/test_float_multidim_2.desc +++ b/jbmc/regression/jbmc/array_nonconstsize_nonconstaccess/test_float_multidim_2.desc @@ -1,6 +1,6 @@ CORE FloatMultidim2 ---function FloatMultidim2.f --unwind 3 +--function FloatMultidim2.f --unwind 3 -cp target/classes ^EXIT=10$ ^SIGNAL=0$ assertion at file FloatMultidim2.java line 14 .*: FAILURE diff --git a/jbmc/regression/jbmc/array_nonconstsize_nonconstaccess/test_ref_multidim_1.desc b/jbmc/regression/jbmc/array_nonconstsize_nonconstaccess/test_ref_multidim_1.desc index 1c4932e2ea8..4df4bd346fa 100644 --- a/jbmc/regression/jbmc/array_nonconstsize_nonconstaccess/test_ref_multidim_1.desc +++ b/jbmc/regression/jbmc/array_nonconstsize_nonconstaccess/test_ref_multidim_1.desc @@ -1,6 +1,6 @@ CORE RefMultidim1 ---function RefMultidim1.f --unwind 3 +--function RefMultidim1.f --unwind 3 -cp target/classes ^EXIT=10$ ^SIGNAL=0$ assertion at file RefMultidim1.java line 15 .*: FAILURE diff --git a/jbmc/regression/jbmc/array_nonconstsize_nonconstaccess/test_ref_multidim_2.desc b/jbmc/regression/jbmc/array_nonconstsize_nonconstaccess/test_ref_multidim_2.desc index da2111478eb..04c798bab59 100644 --- a/jbmc/regression/jbmc/array_nonconstsize_nonconstaccess/test_ref_multidim_2.desc +++ b/jbmc/regression/jbmc/array_nonconstsize_nonconstaccess/test_ref_multidim_2.desc @@ -1,6 +1,6 @@ CORE RefMultidim2 ---function RefMultidim2.f --unwind 3 +--function RefMultidim2.f --unwind 3 -cp target/classes ^EXIT=10$ ^SIGNAL=0$ assertion at file RefMultidim2.java line 15 .*: FAILURE diff --git a/jbmc/regression/jbmc/array_nonconstsize_nonconstaccess/test_ref_multidim_constsize.desc b/jbmc/regression/jbmc/array_nonconstsize_nonconstaccess/test_ref_multidim_constsize.desc index fc471ccf70c..0339e784649 100644 --- a/jbmc/regression/jbmc/array_nonconstsize_nonconstaccess/test_ref_multidim_constsize.desc +++ b/jbmc/regression/jbmc/array_nonconstsize_nonconstaccess/test_ref_multidim_constsize.desc @@ -1,6 +1,6 @@ CORE RefMultidimConstsize ---function RefMultidimConstsize.f --unwind 3 +--function RefMultidimConstsize.f --unwind 3 -cp target/classes ^EXIT=10$ ^SIGNAL=0$ assertion at file RefMultidimConstsize.java line 7 .*: FAILURE diff --git a/jbmc/regression/jbmc/array_nonconstsize_nonconstaccess/test_ref_singledim.desc b/jbmc/regression/jbmc/array_nonconstsize_nonconstaccess/test_ref_singledim.desc index 023b53a65ca..bb308b4445f 100644 --- a/jbmc/regression/jbmc/array_nonconstsize_nonconstaccess/test_ref_singledim.desc +++ b/jbmc/regression/jbmc/array_nonconstsize_nonconstaccess/test_ref_singledim.desc @@ -1,6 +1,6 @@ CORE RefSingledim ---function RefSingledim.f --unwind 3 +--function RefSingledim.f --unwind 3 -cp target/classes ^EXIT=10$ ^SIGNAL=0$ assertion at file RefSingledim.java line 15 .*: FAILURE diff --git a/jbmc/regression/jbmc/pom.xml b/jbmc/regression/jbmc/pom.xml index 4bcbc30ff0a..31e2ff1eb45 100644 --- a/jbmc/regression/jbmc/pom.xml +++ b/jbmc/regression/jbmc/pom.xml @@ -34,6 +34,7 @@ array-cell-sensitivity-negative-size array-cell-sensitivity-static-fields array-clone + array_nonconstsize_nonconstaccess classpath-jar-load-whole-jar From c6b5963a1a5118ae2e17985fa49702fd0310f0e3 Mon Sep 17 00:00:00 2001 From: Peter Schrammel Date: Thu, 2 Jan 2025 19:20:28 +0100 Subject: [PATCH 20/47] Compile jbmc/ArrayIndexOutOfBoundsException1 test sources Add pom.xml for compilation, move sources, remove obsolete pre-compiled class files. --- .../ArrayIndexOutOfBoundsExceptionTest.class | Bin 875 -> 0 bytes .../ArrayIndexOutOfBoundsException1/pom.xml | 30 ++++++++++++++++++ .../ArrayIndexOutOfBoundsExceptionTest.java | 0 .../ArrayIndexOutOfBoundsException1/test.desc | 2 +- jbmc/regression/jbmc/pom.xml | 1 + 5 files changed, 32 insertions(+), 1 deletion(-) delete mode 100644 jbmc/regression/jbmc/ArrayIndexOutOfBoundsException1/ArrayIndexOutOfBoundsExceptionTest.class create mode 100644 jbmc/regression/jbmc/ArrayIndexOutOfBoundsException1/pom.xml rename jbmc/regression/jbmc/ArrayIndexOutOfBoundsException1/{ => src/main/java}/ArrayIndexOutOfBoundsExceptionTest.java (100%) diff --git a/jbmc/regression/jbmc/ArrayIndexOutOfBoundsException1/ArrayIndexOutOfBoundsExceptionTest.class b/jbmc/regression/jbmc/ArrayIndexOutOfBoundsException1/ArrayIndexOutOfBoundsExceptionTest.class deleted file mode 100644 index ca15fe999ec3297420eeb127a4394f9c1e01b4c6..0000000000000000000000000000000000000000 GIT binary patch literal 0 HcmV?d00001 literal 875 zcmaJfgc5Pf4ivE#TUO`wDZ=m#lHgG4U9wL+9qq>4ZesVdQ)HujRbq;|D-P`L6l z`UiS0NK^s@cYYLN)@n&5P%b+=vor6_+nHa#zy1KQhNcS#^EMU=$YasQk_$`w4_wr- zY~vxJQWr@gRT{=o@;ppLZy*B#?Gy4FVHBoM2xen-k6>-Zfh62$hmm|eJnl)gtCI=k zcI=D6o=~CoFN0Qk7$$^zds8X#VJ8aYs54AEZ=c1(C`h(PzC6*CyD~}F8T(j-5n;A* z&^{9HMQb3Ueyf|RFzT;sZW09JV24|gBcIT`mNgk)V++;iPAdO_CQNlx;lFz&PO`T7 zqX^E1Ke!a`cH^P)<%>|uT$#+Il|0tXdnm#qG{!^@Tm8($jjpJ{!po^d*ho4 z(yI8JVz0%P*yfrSpmV+$nC3H|1(}ZTI+YVp!VKF2%BXNe7k^|hgKf?J?zSJ + + 4.0.0 + org.cprover.regression + regression.jbmc.ArrayIndexOutOfBoundsException1 + 1.0-SNAPSHOT + + + org.cprover.regression + regression.jbmc + 1.0-SNAPSHOT + + + + + + maven-jar-plugin + + + default-jar + none + + + + + + + diff --git a/jbmc/regression/jbmc/ArrayIndexOutOfBoundsException1/ArrayIndexOutOfBoundsExceptionTest.java b/jbmc/regression/jbmc/ArrayIndexOutOfBoundsException1/src/main/java/ArrayIndexOutOfBoundsExceptionTest.java similarity index 100% rename from jbmc/regression/jbmc/ArrayIndexOutOfBoundsException1/ArrayIndexOutOfBoundsExceptionTest.java rename to jbmc/regression/jbmc/ArrayIndexOutOfBoundsException1/src/main/java/ArrayIndexOutOfBoundsExceptionTest.java diff --git a/jbmc/regression/jbmc/ArrayIndexOutOfBoundsException1/test.desc b/jbmc/regression/jbmc/ArrayIndexOutOfBoundsException1/test.desc index c6cca9da7d7..e41f46b73a0 100644 --- a/jbmc/regression/jbmc/ArrayIndexOutOfBoundsException1/test.desc +++ b/jbmc/regression/jbmc/ArrayIndexOutOfBoundsException1/test.desc @@ -1,6 +1,6 @@ CORE ArrayIndexOutOfBoundsExceptionTest ---throw-runtime-exceptions +--throw-runtime-exceptions -cp target/classes ^EXIT=10$ ^SIGNAL=0$ ^.*assertion at file ArrayIndexOutOfBoundsExceptionTest.java line 8 function.*: FAILURE$ diff --git a/jbmc/regression/jbmc/pom.xml b/jbmc/regression/jbmc/pom.xml index 31e2ff1eb45..28f147cdeee 100644 --- a/jbmc/regression/jbmc/pom.xml +++ b/jbmc/regression/jbmc/pom.xml @@ -35,6 +35,7 @@ array-cell-sensitivity-static-fields array-clone array_nonconstsize_nonconstaccess + ArrayIndexOutOfBoundsException1 classpath-jar-load-whole-jar From 087c1b2c4f83548acb9bae48a26c4a8b5e217b9b Mon Sep 17 00:00:00 2001 From: Peter Schrammel Date: Thu, 2 Jan 2025 19:20:43 +0100 Subject: [PATCH 21/47] Compile jbmc/ArrayIndexOutOfBoundsException2 test sources Add pom.xml for compilation, move sources, remove obsolete pre-compiled class files. --- .../ArrayIndexOutOfBoundsExceptionTest.class | Bin 875 -> 0 bytes .../ArrayIndexOutOfBoundsException2/pom.xml | 30 ++++++++++++++++++ .../ArrayIndexOutOfBoundsExceptionTest.java | 0 .../ArrayIndexOutOfBoundsException2/test.desc | 2 +- jbmc/regression/jbmc/pom.xml | 1 + 5 files changed, 32 insertions(+), 1 deletion(-) delete mode 100644 jbmc/regression/jbmc/ArrayIndexOutOfBoundsException2/ArrayIndexOutOfBoundsExceptionTest.class create mode 100644 jbmc/regression/jbmc/ArrayIndexOutOfBoundsException2/pom.xml rename jbmc/regression/jbmc/ArrayIndexOutOfBoundsException2/{ => src/main/java}/ArrayIndexOutOfBoundsExceptionTest.java (100%) diff --git a/jbmc/regression/jbmc/ArrayIndexOutOfBoundsException2/ArrayIndexOutOfBoundsExceptionTest.class b/jbmc/regression/jbmc/ArrayIndexOutOfBoundsException2/ArrayIndexOutOfBoundsExceptionTest.class deleted file mode 100644 index 3de63e25a0fbd797d481ae5044d5c401a74ce156..0000000000000000000000000000000000000000 GIT binary patch literal 0 HcmV?d00001 literal 875 zcmaJfgc5PcInvE#TUO`wDZ=m&wOL253&wIE6Zsa>sY6t4V? z{(+tg5|seKogammwOUdMl*`V}?3?#ycIMabuRj2+q2<8FyoH4#3RtwT6FnkNQ&WYA~VF zi99jf6DrXDMbJ#%1~H-0*;Gn=*a>|(>ZVEe&C@6i{djxi$zv_KE8}FHxsOB;5@wqR zokQ_nw1*-bw0nsP!oj-MCPBy@>~JY^Ht%Ykew6)D2fWCE>h zVcA6!D}?fxr`tc2Ucw_Ahqi`1ZT@Iq#(|Rl=A{yULz40Xk9r@Ayeu~F50z`WHoh4k z-4&lx?6uhv+kERBbjFt)rui&nL6+mYhB5$U%&;w@f+|OJ@<&D+Z0pu{r}NNWeRRqT z^a;iZO5b3p4&8%fGV5U;|0_y~pc?#3`4CCL%=9njsoclz#e}|nM?*0K+ C + + 4.0.0 + org.cprover.regression + regression.jbmc.ArrayIndexOutOfBoundsException2 + 1.0-SNAPSHOT + + + org.cprover.regression + regression.jbmc + 1.0-SNAPSHOT + + + + + + maven-jar-plugin + + + default-jar + none + + + + + + + diff --git a/jbmc/regression/jbmc/ArrayIndexOutOfBoundsException2/ArrayIndexOutOfBoundsExceptionTest.java b/jbmc/regression/jbmc/ArrayIndexOutOfBoundsException2/src/main/java/ArrayIndexOutOfBoundsExceptionTest.java similarity index 100% rename from jbmc/regression/jbmc/ArrayIndexOutOfBoundsException2/ArrayIndexOutOfBoundsExceptionTest.java rename to jbmc/regression/jbmc/ArrayIndexOutOfBoundsException2/src/main/java/ArrayIndexOutOfBoundsExceptionTest.java diff --git a/jbmc/regression/jbmc/ArrayIndexOutOfBoundsException2/test.desc b/jbmc/regression/jbmc/ArrayIndexOutOfBoundsException2/test.desc index c6cca9da7d7..e41f46b73a0 100644 --- a/jbmc/regression/jbmc/ArrayIndexOutOfBoundsException2/test.desc +++ b/jbmc/regression/jbmc/ArrayIndexOutOfBoundsException2/test.desc @@ -1,6 +1,6 @@ CORE ArrayIndexOutOfBoundsExceptionTest ---throw-runtime-exceptions +--throw-runtime-exceptions -cp target/classes ^EXIT=10$ ^SIGNAL=0$ ^.*assertion at file ArrayIndexOutOfBoundsExceptionTest.java line 8 function.*: FAILURE$ diff --git a/jbmc/regression/jbmc/pom.xml b/jbmc/regression/jbmc/pom.xml index 28f147cdeee..e2ca8004866 100644 --- a/jbmc/regression/jbmc/pom.xml +++ b/jbmc/regression/jbmc/pom.xml @@ -36,6 +36,7 @@ array-clone array_nonconstsize_nonconstaccess ArrayIndexOutOfBoundsException1 + ArrayIndexOutOfBoundsException2 classpath-jar-load-whole-jar From 90675601f2e2ed57fbcf87ddaf7e3a1539c5adcf Mon Sep 17 00:00:00 2001 From: Peter Schrammel Date: Thu, 2 Jan 2025 19:21:44 +0100 Subject: [PATCH 22/47] Compile jbmc/ArrayIndexOutOfBoundsException3 test sources Add pom.xml for compilation, move sources, remove obsolete pre-compiled class files. --- .../ArrayIndexOutOfBoundsExceptionTest.class | Bin 642 -> 0 bytes .../lang/ArrayIndexOutOfBoundsException.class | Bin 263 -> 0 bytes .../java/lang/IndexOutOfBoundsException.class | Bin 244 -> 0 bytes .../java/lang/RuntimeException.class | Bin 219 -> 0 bytes .../ArrayIndexOutOfBoundsException3/pom.xml | 30 ++++++++++++++++++ .../ArrayIndexOutOfBoundsExceptionTest.java | 0 .../lang/ArrayIndexOutOfBoundsException.java | 0 .../java/lang/IndexOutOfBoundsException.java | 0 .../java}/java/lang/RuntimeException.java | 0 .../ArrayIndexOutOfBoundsException3/test.desc | 2 +- jbmc/regression/jbmc/pom.xml | 1 + 11 files changed, 32 insertions(+), 1 deletion(-) delete mode 100644 jbmc/regression/jbmc/ArrayIndexOutOfBoundsException3/ArrayIndexOutOfBoundsExceptionTest.class delete mode 100644 jbmc/regression/jbmc/ArrayIndexOutOfBoundsException3/java/lang/ArrayIndexOutOfBoundsException.class delete mode 100644 jbmc/regression/jbmc/ArrayIndexOutOfBoundsException3/java/lang/IndexOutOfBoundsException.class delete mode 100644 jbmc/regression/jbmc/ArrayIndexOutOfBoundsException3/java/lang/RuntimeException.class create mode 100644 jbmc/regression/jbmc/ArrayIndexOutOfBoundsException3/pom.xml rename jbmc/regression/jbmc/ArrayIndexOutOfBoundsException3/{ => src/main/java}/ArrayIndexOutOfBoundsExceptionTest.java (100%) rename jbmc/regression/jbmc/ArrayIndexOutOfBoundsException3/{ => src/main/java}/java/lang/ArrayIndexOutOfBoundsException.java (100%) rename jbmc/regression/jbmc/ArrayIndexOutOfBoundsException3/{ => src/main/java}/java/lang/IndexOutOfBoundsException.java (100%) rename jbmc/regression/jbmc/ArrayIndexOutOfBoundsException3/{ => src/main/java}/java/lang/RuntimeException.java (100%) diff --git a/jbmc/regression/jbmc/ArrayIndexOutOfBoundsException3/ArrayIndexOutOfBoundsExceptionTest.class b/jbmc/regression/jbmc/ArrayIndexOutOfBoundsException3/ArrayIndexOutOfBoundsExceptionTest.class deleted file mode 100644 index b500a095ac41cfbe1c2e8b734362ae73c37f89a3..0000000000000000000000000000000000000000 GIT binary patch literal 0 HcmV?d00001 literal 642 zcmah`O;6iE5PcInS;rU%q0sQzQdKG+Qn_#gRRv0=ia-uQNYGw3_7*J!8?Eh%{uTZJ zXIiO91(iEL3U$_$~vK`phH4sO~*QWM{wpB_6hE05-GxPQ^#sIKkX>9XOkH?l{zMj z&wp+n%WrbIE90Z(c4l;Zv}y|n+nEeccH~)+&teGPTG;(Z?zfZNgzBTVRBzUek>5YX zkvebXS?lXYlE+cHbsnlSD{xPx*<0HqzyJc)-tX7T2~dSkX!N1=r}?&wNetoD|Ck{?m4>%VXxPg0cjq=@9 zQRXp!iH{|kWGe8#yC}1cDkFk>dmQ&M!iYd=TcAF~q0yeGm4XHssaJkMTtK*&aGjrU WtiVU!CxMouj8gF4j`6I3$NmCTb^1}=66ZgvJ9Mg}&U%)HDJJ4Oa(4b3n{1{UZ1lvG9rexJ;| zRKL>Pq|~C2#H1Xc2v=}^X;E^jTPBF3>{wKkSm~LUl3L+kTH>GPlwX>cQtVohoLW$l znV+YZl~|U@!@$D8%E+JrV(aH5=B4Z7*90^bp%kal42ld)K<9%1BM<_u0FrD#o-CNp ez`&}toq=&9SehM3vH^t|fEpMXIDj-011A75@IS2p diff --git a/jbmc/regression/jbmc/ArrayIndexOutOfBoundsException3/java/lang/IndexOutOfBoundsException.class b/jbmc/regression/jbmc/ArrayIndexOutOfBoundsException3/java/lang/IndexOutOfBoundsException.class deleted file mode 100644 index 07ac2ac49f62e772ff6fc217c0988551758bf695..0000000000000000000000000000000000000000 GIT binary patch literal 0 HcmV?d00001 literal 244 zcmZ`z&kF%z5Pie`V3E6`!o_@q9aovO`70Xb3%}_^% ge@%io*_6>@R!uozw(p=@y0#fD9)k}EIj$MxKisM~FaQ7m diff --git a/jbmc/regression/jbmc/ArrayIndexOutOfBoundsException3/java/lang/RuntimeException.class b/jbmc/regression/jbmc/ArrayIndexOutOfBoundsException3/java/lang/RuntimeException.class deleted file mode 100644 index 2f0ac26544c602aa8e73f1ca35724acb4aa9c8a5..0000000000000000000000000000000000000000 GIT binary patch literal 0 HcmV?d00001 literal 219 zcmX^0Z`VEs1_l!bUM>b^1}=66ZgvJ9Mg}&U%)HDJJ4Oa(4b3n{1{UZ1lvG9rexJ;| zRKL>Pq|~C2#H1Xc2v=}^X;E^jTPBDj8dREBl9`+8T9KSuP?DLSr!T}UWDrJ3!ZkA}GB5$11Okje2s8vpvH^LrU_Ju_tJZb~#*JWUb|A?H Q6lMTwU}WF`(o77T0A{Z)TL1t6 diff --git a/jbmc/regression/jbmc/ArrayIndexOutOfBoundsException3/pom.xml b/jbmc/regression/jbmc/ArrayIndexOutOfBoundsException3/pom.xml new file mode 100644 index 00000000000..4b7162373f1 --- /dev/null +++ b/jbmc/regression/jbmc/ArrayIndexOutOfBoundsException3/pom.xml @@ -0,0 +1,30 @@ + + + 4.0.0 + org.cprover.regression + regression.jbmc.ArrayIndexOutOfBoundsException3 + 1.0-SNAPSHOT + + + org.cprover.regression + regression.jbmc + 1.0-SNAPSHOT + + + + + + maven-jar-plugin + + + default-jar + none + + + + + + + diff --git a/jbmc/regression/jbmc/ArrayIndexOutOfBoundsException3/ArrayIndexOutOfBoundsExceptionTest.java b/jbmc/regression/jbmc/ArrayIndexOutOfBoundsException3/src/main/java/ArrayIndexOutOfBoundsExceptionTest.java similarity index 100% rename from jbmc/regression/jbmc/ArrayIndexOutOfBoundsException3/ArrayIndexOutOfBoundsExceptionTest.java rename to jbmc/regression/jbmc/ArrayIndexOutOfBoundsException3/src/main/java/ArrayIndexOutOfBoundsExceptionTest.java diff --git a/jbmc/regression/jbmc/ArrayIndexOutOfBoundsException3/java/lang/ArrayIndexOutOfBoundsException.java b/jbmc/regression/jbmc/ArrayIndexOutOfBoundsException3/src/main/java/java/lang/ArrayIndexOutOfBoundsException.java similarity index 100% rename from jbmc/regression/jbmc/ArrayIndexOutOfBoundsException3/java/lang/ArrayIndexOutOfBoundsException.java rename to jbmc/regression/jbmc/ArrayIndexOutOfBoundsException3/src/main/java/java/lang/ArrayIndexOutOfBoundsException.java diff --git a/jbmc/regression/jbmc/ArrayIndexOutOfBoundsException3/java/lang/IndexOutOfBoundsException.java b/jbmc/regression/jbmc/ArrayIndexOutOfBoundsException3/src/main/java/java/lang/IndexOutOfBoundsException.java similarity index 100% rename from jbmc/regression/jbmc/ArrayIndexOutOfBoundsException3/java/lang/IndexOutOfBoundsException.java rename to jbmc/regression/jbmc/ArrayIndexOutOfBoundsException3/src/main/java/java/lang/IndexOutOfBoundsException.java diff --git a/jbmc/regression/jbmc/ArrayIndexOutOfBoundsException3/java/lang/RuntimeException.java b/jbmc/regression/jbmc/ArrayIndexOutOfBoundsException3/src/main/java/java/lang/RuntimeException.java similarity index 100% rename from jbmc/regression/jbmc/ArrayIndexOutOfBoundsException3/java/lang/RuntimeException.java rename to jbmc/regression/jbmc/ArrayIndexOutOfBoundsException3/src/main/java/java/lang/RuntimeException.java diff --git a/jbmc/regression/jbmc/ArrayIndexOutOfBoundsException3/test.desc b/jbmc/regression/jbmc/ArrayIndexOutOfBoundsException3/test.desc index c6cca9da7d7..e41f46b73a0 100644 --- a/jbmc/regression/jbmc/ArrayIndexOutOfBoundsException3/test.desc +++ b/jbmc/regression/jbmc/ArrayIndexOutOfBoundsException3/test.desc @@ -1,6 +1,6 @@ CORE ArrayIndexOutOfBoundsExceptionTest ---throw-runtime-exceptions +--throw-runtime-exceptions -cp target/classes ^EXIT=10$ ^SIGNAL=0$ ^.*assertion at file ArrayIndexOutOfBoundsExceptionTest.java line 8 function.*: FAILURE$ diff --git a/jbmc/regression/jbmc/pom.xml b/jbmc/regression/jbmc/pom.xml index e2ca8004866..52a6e1b3cba 100644 --- a/jbmc/regression/jbmc/pom.xml +++ b/jbmc/regression/jbmc/pom.xml @@ -37,6 +37,7 @@ array_nonconstsize_nonconstaccess ArrayIndexOutOfBoundsException1 ArrayIndexOutOfBoundsException2 + ArrayIndexOutOfBoundsException3 classpath-jar-load-whole-jar From 2ed897b3528cd91f8d549ea82c86e076dab0f8db Mon Sep 17 00:00:00 2001 From: Peter Schrammel Date: Thu, 2 Jan 2025 19:22:31 +0100 Subject: [PATCH 23/47] Compile jbmc/arraylength1 test sources Add pom.xml for compilation, move sources, remove obsolete pre-compiled class files. --- .../jbmc/arraylength1/arraylength1.class | Bin 566 -> 0 bytes jbmc/regression/jbmc/arraylength1/pom.xml | 30 ++++++++++++++++++ .../{ => src/main/java}/arraylength1.java | 0 jbmc/regression/jbmc/arraylength1/test.desc | 2 +- jbmc/regression/jbmc/pom.xml | 1 + 5 files changed, 32 insertions(+), 1 deletion(-) delete mode 100644 jbmc/regression/jbmc/arraylength1/arraylength1.class create mode 100644 jbmc/regression/jbmc/arraylength1/pom.xml rename jbmc/regression/jbmc/arraylength1/{ => src/main/java}/arraylength1.java (100%) diff --git a/jbmc/regression/jbmc/arraylength1/arraylength1.class b/jbmc/regression/jbmc/arraylength1/arraylength1.class deleted file mode 100644 index 5bf22d010d3c8579d38b0785f237b994828e518a..0000000000000000000000000000000000000000 GIT binary patch literal 0 HcmV?d00001 literal 566 zcmYk2&rcIU6vw}Be{|Yqm2E4v3Kb31IYJ!jhQ_#a2K52M@ZVvFWRQZBb=uj69E3 zGR%%&Jh!wE0Tx0OQ6kjm_}4Sfd&Z0mA^cw`&}md>3@C;9Q`xJ&l4(EZoBVJc0MqBAgsifyc4Wk^(y@VufK5XG);o ryh(vFCoA_xnt4Z{T=9RPZ~@_cgXdnunG + + 4.0.0 + org.cprover.regression + regression.jbmc.arraylength1 + 1.0-SNAPSHOT + + + org.cprover.regression + regression.jbmc + 1.0-SNAPSHOT + + + + + + maven-jar-plugin + + + default-jar + none + + + + + + + diff --git a/jbmc/regression/jbmc/arraylength1/arraylength1.java b/jbmc/regression/jbmc/arraylength1/src/main/java/arraylength1.java similarity index 100% rename from jbmc/regression/jbmc/arraylength1/arraylength1.java rename to jbmc/regression/jbmc/arraylength1/src/main/java/arraylength1.java diff --git a/jbmc/regression/jbmc/arraylength1/test.desc b/jbmc/regression/jbmc/arraylength1/test.desc index 4d7c9a21f30..7d896f47bc4 100644 --- a/jbmc/regression/jbmc/arraylength1/test.desc +++ b/jbmc/regression/jbmc/arraylength1/test.desc @@ -1,6 +1,6 @@ CORE arraylength1 - +-cp target/classes ^EXIT=0$ ^SIGNAL=0$ ^VERIFICATION SUCCESSFUL$ diff --git a/jbmc/regression/jbmc/pom.xml b/jbmc/regression/jbmc/pom.xml index 52a6e1b3cba..a55f3918bba 100644 --- a/jbmc/regression/jbmc/pom.xml +++ b/jbmc/regression/jbmc/pom.xml @@ -38,6 +38,7 @@ ArrayIndexOutOfBoundsException1 ArrayIndexOutOfBoundsException2 ArrayIndexOutOfBoundsException3 + arraylength1 classpath-jar-load-whole-jar From d5b088df7cf15779dc7d75db59cda7c567707251 Mon Sep 17 00:00:00 2001 From: Peter Schrammel Date: Thu, 2 Jan 2025 19:22:53 +0100 Subject: [PATCH 24/47] Compile jbmc/arrayread1 test sources Add pom.xml for compilation, move sources, remove obsolete pre-compiled class files. --- .../jbmc/arrayread1/arrayread1.class | Bin 612 -> 0 bytes jbmc/regression/jbmc/arrayread1/pom.xml | 30 ++++++++++++++++++ .../{ => src/main/java}/arrayread1.java | 0 jbmc/regression/jbmc/arrayread1/test.desc | 2 +- jbmc/regression/jbmc/pom.xml | 1 + 5 files changed, 32 insertions(+), 1 deletion(-) delete mode 100644 jbmc/regression/jbmc/arrayread1/arrayread1.class create mode 100644 jbmc/regression/jbmc/arrayread1/pom.xml rename jbmc/regression/jbmc/arrayread1/{ => src/main/java}/arrayread1.java (100%) diff --git a/jbmc/regression/jbmc/arrayread1/arrayread1.class b/jbmc/regression/jbmc/arrayread1/arrayread1.class deleted file mode 100644 index 66779a1478bee6ac321ceb08912dba6ac2307ddd..0000000000000000000000000000000000000000 GIT binary patch literal 0 HcmV?d00001 literal 612 zcmY*WT~8B16g{)M?UwD*55QWBMS(&<6N!X3iNRD&NUA0=TF0dEZZn1JUa4_}~aC~I9A?XSJLbNo*0o^~~eB}N}%FUt6(I`0g^ro9D5J*{LdW!*+hB)N>yWrhz+Wvz*yw1&McTS z&n_SaJkSkeHU$NrmNCV%p?;&7#k^c|e!v;je!*%zx7W{L58<4mJcNCN{1q}^E|9%8 zT2`u6;YtCQnmJl9iXN6|Wtu40p1n1@o?-F9$kj&L9w<*)=WtKqIzQpqXY4vsy>n<( OGO+wDGe;#YKl}$3kZ>6Q diff --git a/jbmc/regression/jbmc/arrayread1/pom.xml b/jbmc/regression/jbmc/arrayread1/pom.xml new file mode 100644 index 00000000000..49a97ed7dfa --- /dev/null +++ b/jbmc/regression/jbmc/arrayread1/pom.xml @@ -0,0 +1,30 @@ + + + 4.0.0 + org.cprover.regression + regression.jbmc.arrayread1 + 1.0-SNAPSHOT + + + org.cprover.regression + regression.jbmc + 1.0-SNAPSHOT + + + + + + maven-jar-plugin + + + default-jar + none + + + + + + + diff --git a/jbmc/regression/jbmc/arrayread1/arrayread1.java b/jbmc/regression/jbmc/arrayread1/src/main/java/arrayread1.java similarity index 100% rename from jbmc/regression/jbmc/arrayread1/arrayread1.java rename to jbmc/regression/jbmc/arrayread1/src/main/java/arrayread1.java diff --git a/jbmc/regression/jbmc/arrayread1/test.desc b/jbmc/regression/jbmc/arrayread1/test.desc index 147a0556846..bb36a860d0a 100644 --- a/jbmc/regression/jbmc/arrayread1/test.desc +++ b/jbmc/regression/jbmc/arrayread1/test.desc @@ -1,6 +1,6 @@ CORE arrayread1 ---unwind 3 --no-propagation --function arrayread1.main +--unwind 3 --no-propagation --function arrayread1.main -cp target/classes ^EXIT=0$ ^SIGNAL=0$ ^VERIFICATION SUCCESSFUL$ diff --git a/jbmc/regression/jbmc/pom.xml b/jbmc/regression/jbmc/pom.xml index a55f3918bba..2fdedfc2ef3 100644 --- a/jbmc/regression/jbmc/pom.xml +++ b/jbmc/regression/jbmc/pom.xml @@ -39,6 +39,7 @@ ArrayIndexOutOfBoundsException2 ArrayIndexOutOfBoundsException3 arraylength1 + arrayread1 classpath-jar-load-whole-jar From 14bfce7c1b5d320d192ca17a75d08b06f8092283 Mon Sep 17 00:00:00 2001 From: Peter Schrammel Date: Thu, 2 Jan 2025 19:23:22 +0100 Subject: [PATCH 25/47] Compile jbmc/assert1 test sources Add pom.xml for compilation, move sources, remove obsolete pre-compiled class files. --- jbmc/regression/jbmc/assert1/assert1.class | Bin 735 -> 0 bytes jbmc/regression/jbmc/assert1/pom.xml | 30 ++++++++++++++++++ .../assert1/{ => src/main/java}/assert1.java | 0 jbmc/regression/jbmc/assert1/test.desc | 2 +- jbmc/regression/jbmc/pom.xml | 1 + 5 files changed, 32 insertions(+), 1 deletion(-) delete mode 100644 jbmc/regression/jbmc/assert1/assert1.class create mode 100644 jbmc/regression/jbmc/assert1/pom.xml rename jbmc/regression/jbmc/assert1/{ => src/main/java}/assert1.java (100%) diff --git a/jbmc/regression/jbmc/assert1/assert1.class b/jbmc/regression/jbmc/assert1/assert1.class deleted file mode 100644 index eb6fad5bf34e5d1d6f0d2b36fee49c9d73f4de23..0000000000000000000000000000000000000000 GIT binary patch literal 0 HcmV?d00001 literal 735 zcmZ`%T~8B16g|^+JMFTyODVNT!J?>3K^hHjqS2tnnyQHX_GP%MlPNG1%4euKue*oht!R6~KWO*jQ27UUbYZC%i@}>`;wa50iVTJA zfp-pW_JSlF$j3@US!Y~sZE7G3Hf9;@6f}vI*M2E{HyCRF4GRv|EL=dDp+0T`<)%u@QzAPa;nPrD8L3dZ6J9inIH3Rm?W0K-Q=+?Kc3mqWD@%)1gP4=GL?@%u zXpO+WkU`f)dp>nC6j8-I**f(Da%pkr6q&s$vLhJX^%LapHf-}F7QTWXV~*@kD4n9P zS1FEQ{%qLQ|HgE?OxkW4oNR-*a^hA*4JHlD!foRIgm~8|O7HA9HaIS_MS5ZNiGr<^ iDll7_Ie~Qyp8Jek_8a&Veym2r7|2-nwdRGi`=!4XC5nvz diff --git a/jbmc/regression/jbmc/assert1/pom.xml b/jbmc/regression/jbmc/assert1/pom.xml new file mode 100644 index 00000000000..65489ced2c9 --- /dev/null +++ b/jbmc/regression/jbmc/assert1/pom.xml @@ -0,0 +1,30 @@ + + + 4.0.0 + org.cprover.regression + regression.jbmc.assert1 + 1.0-SNAPSHOT + + + org.cprover.regression + regression.jbmc + 1.0-SNAPSHOT + + + + + + maven-jar-plugin + + + default-jar + none + + + + + + + diff --git a/jbmc/regression/jbmc/assert1/assert1.java b/jbmc/regression/jbmc/assert1/src/main/java/assert1.java similarity index 100% rename from jbmc/regression/jbmc/assert1/assert1.java rename to jbmc/regression/jbmc/assert1/src/main/java/assert1.java diff --git a/jbmc/regression/jbmc/assert1/test.desc b/jbmc/regression/jbmc/assert1/test.desc index 45ce9e12416..4be9690f6e5 100644 --- a/jbmc/regression/jbmc/assert1/test.desc +++ b/jbmc/regression/jbmc/assert1/test.desc @@ -1,6 +1,6 @@ CORE assert1 - +-cp target/classes ^EXIT=0$ ^SIGNAL=0$ ^VERIFICATION SUCCESSFUL$ diff --git a/jbmc/regression/jbmc/pom.xml b/jbmc/regression/jbmc/pom.xml index 2fdedfc2ef3..3a3cb16d3cb 100644 --- a/jbmc/regression/jbmc/pom.xml +++ b/jbmc/regression/jbmc/pom.xml @@ -40,6 +40,7 @@ ArrayIndexOutOfBoundsException3 arraylength1 arrayread1 + assert1 classpath-jar-load-whole-jar From 8b68ff49cbc88efaf275d3588d8e37188fde0b9d Mon Sep 17 00:00:00 2001 From: Peter Schrammel Date: Thu, 2 Jan 2025 19:23:38 +0100 Subject: [PATCH 26/47] Compile jbmc/assert2 test sources Add pom.xml for compilation, move sources, remove obsolete pre-compiled class files. --- jbmc/regression/jbmc/assert2/assert2.class | Bin 700 -> 0 bytes jbmc/regression/jbmc/assert2/pom.xml | 30 ++++++++++++++++++ .../assert2/{ => src/main/java}/assert2.java | 0 jbmc/regression/jbmc/assert2/test.desc | 2 +- jbmc/regression/jbmc/pom.xml | 1 + 5 files changed, 32 insertions(+), 1 deletion(-) delete mode 100644 jbmc/regression/jbmc/assert2/assert2.class create mode 100644 jbmc/regression/jbmc/assert2/pom.xml rename jbmc/regression/jbmc/assert2/{ => src/main/java}/assert2.java (100%) diff --git a/jbmc/regression/jbmc/assert2/assert2.class b/jbmc/regression/jbmc/assert2/assert2.class deleted file mode 100644 index 80fbe0c0be169a7b39f9d55ff037bf9b2178939f..0000000000000000000000000000000000000000 GIT binary patch literal 0 HcmV?d00001 literal 700 zcmYjPO>fgc5PciR+1RzoN7FPdEf^@^rjUe6oLUg5fYd60L=aNT$%&U}i(@0(LHw59 z5C_hH)JRl*RSh=BukfqU2qQOul zYn66JyWX6DeIbLUMQb4oG8m{~fozrf2KlVGeS+M64cY{HcjFj^dn*;~_eU&$1wTSf zIiFykptxT(CNO_0&|C&uhk7_VG2+C)z#>ev$g5M-0Q-X$$07|5jdOZ;Gaf*79&^XA cj==Muk=MR~&tRuq6^xFY{Xi*N%DOK919_i=i2wiq diff --git a/jbmc/regression/jbmc/assert2/pom.xml b/jbmc/regression/jbmc/assert2/pom.xml new file mode 100644 index 00000000000..329a0df9730 --- /dev/null +++ b/jbmc/regression/jbmc/assert2/pom.xml @@ -0,0 +1,30 @@ + + + 4.0.0 + org.cprover.regression + regression.jbmc.assert2 + 1.0-SNAPSHOT + + + org.cprover.regression + regression.jbmc + 1.0-SNAPSHOT + + + + + + maven-jar-plugin + + + default-jar + none + + + + + + + diff --git a/jbmc/regression/jbmc/assert2/assert2.java b/jbmc/regression/jbmc/assert2/src/main/java/assert2.java similarity index 100% rename from jbmc/regression/jbmc/assert2/assert2.java rename to jbmc/regression/jbmc/assert2/src/main/java/assert2.java diff --git a/jbmc/regression/jbmc/assert2/test.desc b/jbmc/regression/jbmc/assert2/test.desc index 9a000461b72..a3981bdefdf 100644 --- a/jbmc/regression/jbmc/assert2/test.desc +++ b/jbmc/regression/jbmc/assert2/test.desc @@ -1,6 +1,6 @@ CORE assert2 - +-cp target/classes ^EXIT=10$ ^SIGNAL=0$ ^VERIFICATION FAILED$ diff --git a/jbmc/regression/jbmc/pom.xml b/jbmc/regression/jbmc/pom.xml index 3a3cb16d3cb..c79fadda992 100644 --- a/jbmc/regression/jbmc/pom.xml +++ b/jbmc/regression/jbmc/pom.xml @@ -41,6 +41,7 @@ arraylength1 arrayread1 assert1 + assert2 classpath-jar-load-whole-jar From 068d80aa2bb07e5caea637f045f0bfcf66c26456 Mon Sep 17 00:00:00 2001 From: Peter Schrammel Date: Thu, 2 Jan 2025 19:23:58 +0100 Subject: [PATCH 27/47] Compile jbmc/assert3 test sources Add pom.xml for compilation, move sources, remove obsolete pre-compiled class files. --- jbmc/regression/jbmc/assert3/assert3.class | Bin 503 -> 0 bytes jbmc/regression/jbmc/assert3/pom.xml | 30 ++++++++++++++++++ .../assert3/{ => src/main/java}/assert3.java | 0 jbmc/regression/jbmc/assert3/test.desc | 2 +- .../jbmc/assert3/test_throw_no_uncaught.desc | 2 +- jbmc/regression/jbmc/pom.xml | 1 + 6 files changed, 33 insertions(+), 2 deletions(-) delete mode 100644 jbmc/regression/jbmc/assert3/assert3.class create mode 100644 jbmc/regression/jbmc/assert3/pom.xml rename jbmc/regression/jbmc/assert3/{ => src/main/java}/assert3.java (100%) diff --git a/jbmc/regression/jbmc/assert3/assert3.class b/jbmc/regression/jbmc/assert3/assert3.class deleted file mode 100644 index d3f15d765213f7c79ef4566371c9ace1cd6af9bd..0000000000000000000000000000000000000000 GIT binary patch literal 0 HcmV?d00001 literal 503 zcmYjN+e$(~6kX$O)U?#RWooyVqd{6dRzgI9VFek1^fc;0#&k{`kJ0Z$U(icJLcRAT z{Y258Q&Agc_GR{3d+mAqe0~A2g|#qdkmktvDb-dE!-K587C3T2EQZ06=O}O#83Maf zNvFo(HAPW#@eJXnHMTqEk<|Ez7>!KZ+1}9T2qK6w#9XGaBL|gpp}N*k*Oww##tK9B zZ_K_6m6kfRZObOjvbI^RR(1C(1OH+E<#UytwfknrA=$>UR>zfj=hPJyXw5o9%J{d% zcQ0*0gZ1ZW^UxuUV3?(-K%SBJmnUG46wnXR9dL^bA;b`;ShsfJgO_}13QsEu?*#tF z`V#_s`MCG}9!c#U5S@az62S>VubR%|(&dPdW{?6-gdt=|O_4H#lqBdS1oi=gV_u6% Hy0Fw2DBxVt diff --git a/jbmc/regression/jbmc/assert3/pom.xml b/jbmc/regression/jbmc/assert3/pom.xml new file mode 100644 index 00000000000..35755aae8e2 --- /dev/null +++ b/jbmc/regression/jbmc/assert3/pom.xml @@ -0,0 +1,30 @@ + + + 4.0.0 + org.cprover.regression + regression.jbmc.assert3 + 1.0-SNAPSHOT + + + org.cprover.regression + regression.jbmc + 1.0-SNAPSHOT + + + + + + maven-jar-plugin + + + default-jar + none + + + + + + + diff --git a/jbmc/regression/jbmc/assert3/assert3.java b/jbmc/regression/jbmc/assert3/src/main/java/assert3.java similarity index 100% rename from jbmc/regression/jbmc/assert3/assert3.java rename to jbmc/regression/jbmc/assert3/src/main/java/assert3.java diff --git a/jbmc/regression/jbmc/assert3/test.desc b/jbmc/regression/jbmc/assert3/test.desc index 19d5157d04b..16a01c15b58 100644 --- a/jbmc/regression/jbmc/assert3/test.desc +++ b/jbmc/regression/jbmc/assert3/test.desc @@ -1,6 +1,6 @@ CORE assert3 - +-cp target/classes ^EXIT=10$ ^SIGNAL=0$ ^VERIFICATION FAILED$ diff --git a/jbmc/regression/jbmc/assert3/test_throw_no_uncaught.desc b/jbmc/regression/jbmc/assert3/test_throw_no_uncaught.desc index 8e320065b11..2f106df135e 100644 --- a/jbmc/regression/jbmc/assert3/test_throw_no_uncaught.desc +++ b/jbmc/regression/jbmc/assert3/test_throw_no_uncaught.desc @@ -1,6 +1,6 @@ CORE assert3 ---throw-assertion-error --disable-uncaught-exception-check +--throw-assertion-error --disable-uncaught-exception-check -cp target/classes ^EXIT=0$ ^SIGNAL=0$ ^VERIFICATION SUCCESSFUL$ diff --git a/jbmc/regression/jbmc/pom.xml b/jbmc/regression/jbmc/pom.xml index c79fadda992..030b5675b38 100644 --- a/jbmc/regression/jbmc/pom.xml +++ b/jbmc/regression/jbmc/pom.xml @@ -42,6 +42,7 @@ arrayread1 assert1 assert2 + assert3 classpath-jar-load-whole-jar From 46797db83dcab6cd79689008a66f143f56c19dd8 Mon Sep 17 00:00:00 2001 From: Peter Schrammel Date: Thu, 2 Jan 2025 19:24:13 +0100 Subject: [PATCH 28/47] Compile jbmc/assert4 test sources Add pom.xml for compilation, move sources, remove obsolete pre-compiled class files. --- jbmc/regression/jbmc/assert4/assert4.class | Bin 698 -> 0 bytes jbmc/regression/jbmc/assert4/pom.xml | 30 ++++++++++++++++++ .../assert4/{ => src/main/java}/assert4.java | 0 jbmc/regression/jbmc/assert4/test.desc | 2 +- jbmc/regression/jbmc/pom.xml | 1 + 5 files changed, 32 insertions(+), 1 deletion(-) delete mode 100644 jbmc/regression/jbmc/assert4/assert4.class create mode 100644 jbmc/regression/jbmc/assert4/pom.xml rename jbmc/regression/jbmc/assert4/{ => src/main/java}/assert4.java (100%) diff --git a/jbmc/regression/jbmc/assert4/assert4.class b/jbmc/regression/jbmc/assert4/assert4.class deleted file mode 100644 index cfefa40fc199a6aa1520b84a5fa7b662c40f6229..0000000000000000000000000000000000000000 GIT binary patch literal 0 HcmV?d00001 literal 698 zcmYjPO>fgc5Pg%x*~D>(o2DU!6w*>4O+RwUje=ZPKmDhdc_--)P=XWi%v0>o~Dul+o?4zlcCt()&A>Q}-fLpOoSZe>L z^ddG@TA35s^BA9-;>t*c(w*_*Uc?DsFwh}dJeV@iitL6~!d{ktRt;v(-U?e{Yjh@{ zuk7%+c+IDWgd%EKVqb^4$fe2K=g1t?ke$HjZ=NB4ziFGFu>1|;6pKx}_8H}K6b`Dz z3Cv#_GLu5qq2GM+<|a diff --git a/jbmc/regression/jbmc/assert4/pom.xml b/jbmc/regression/jbmc/assert4/pom.xml new file mode 100644 index 00000000000..1df6fd6987a --- /dev/null +++ b/jbmc/regression/jbmc/assert4/pom.xml @@ -0,0 +1,30 @@ + + + 4.0.0 + org.cprover.regression + regression.jbmc.assert4 + 1.0-SNAPSHOT + + + org.cprover.regression + regression.jbmc + 1.0-SNAPSHOT + + + + + + maven-jar-plugin + + + default-jar + none + + + + + + + diff --git a/jbmc/regression/jbmc/assert4/assert4.java b/jbmc/regression/jbmc/assert4/src/main/java/assert4.java similarity index 100% rename from jbmc/regression/jbmc/assert4/assert4.java rename to jbmc/regression/jbmc/assert4/src/main/java/assert4.java diff --git a/jbmc/regression/jbmc/assert4/test.desc b/jbmc/regression/jbmc/assert4/test.desc index 461bde7c38a..31a59524f20 100644 --- a/jbmc/regression/jbmc/assert4/test.desc +++ b/jbmc/regression/jbmc/assert4/test.desc @@ -1,6 +1,6 @@ CORE assert4 - +-cp target/classes ^EXIT=10$ ^SIGNAL=0$ ^VERIFICATION FAILED$ diff --git a/jbmc/regression/jbmc/pom.xml b/jbmc/regression/jbmc/pom.xml index 030b5675b38..6ca72e8e543 100644 --- a/jbmc/regression/jbmc/pom.xml +++ b/jbmc/regression/jbmc/pom.xml @@ -43,6 +43,7 @@ assert1 assert2 assert3 + assert4 classpath-jar-load-whole-jar From 40965b04f2e448db0471f3336238298b1e229748 Mon Sep 17 00:00:00 2001 From: Peter Schrammel Date: Thu, 2 Jan 2025 19:24:28 +0100 Subject: [PATCH 29/47] Compile jbmc/assert5 test sources Add pom.xml for compilation, move sources, remove obsolete pre-compiled class files. --- jbmc/regression/jbmc/assert5/assert5.class | Bin 699 -> 0 bytes jbmc/regression/jbmc/assert5/pom.xml | 30 ++++++++++++++++++ .../assert5/{ => src/main/java}/assert5.java | 0 jbmc/regression/jbmc/assert5/test.desc | 2 +- jbmc/regression/jbmc/pom.xml | 1 + 5 files changed, 32 insertions(+), 1 deletion(-) delete mode 100644 jbmc/regression/jbmc/assert5/assert5.class create mode 100644 jbmc/regression/jbmc/assert5/pom.xml rename jbmc/regression/jbmc/assert5/{ => src/main/java}/assert5.java (100%) diff --git a/jbmc/regression/jbmc/assert5/assert5.class b/jbmc/regression/jbmc/assert5/assert5.class deleted file mode 100644 index cd56f3a62d6994223d66068603e10131e16fd7d8..0000000000000000000000000000000000000000 GIT binary patch literal 0 HcmV?d00001 literal 699 zcmYjPO>fgc5PciR+1Pc+2Wc8g3kC|fDI`HECkg@;kct9G1R=GYHt`Z|acpEeh~LsH zNSpzwk*EZBehGg9#H`yiSn}@7?97|@cJ|lb?>_)+qHUvu^BgNCx%z9_$YE747c4B` zB8OYVB^yOt=D1>G4Ocm?F`Qi!Nh0G^MPc$#C1MarpMmW$6t+~T(t8YsxBiMDza9CK zq1;oUd^Q;mWc*Sm)4^D%kfGtd?(K{Bq7#U4)aj?O3P*QzVX2>r;oGO;U6xN28H!uO z-~`<6N0WFcA1e*z9CNwd)<6y_s4`SC&`GL-&I=Lx(OAc?JMggX;0($P&3W4gGcAwe zIEopn%2kOwils4^Y?6 zN0g3G+^tzt*grLBE(2{qKOB=7abjR$2{zi~H7II<{Xv^!i3W$}DZR~%2T-jo9KtyO a&wobV_y#^lol(^&CUVYwE$Cd + + 4.0.0 + org.cprover.regression + regression.jbmc.assert5 + 1.0-SNAPSHOT + + + org.cprover.regression + regression.jbmc + 1.0-SNAPSHOT + + + + + + maven-jar-plugin + + + default-jar + none + + + + + + + diff --git a/jbmc/regression/jbmc/assert5/assert5.java b/jbmc/regression/jbmc/assert5/src/main/java/assert5.java similarity index 100% rename from jbmc/regression/jbmc/assert5/assert5.java rename to jbmc/regression/jbmc/assert5/src/main/java/assert5.java diff --git a/jbmc/regression/jbmc/assert5/test.desc b/jbmc/regression/jbmc/assert5/test.desc index 02dc9fa50a1..a7e4a6f48d5 100644 --- a/jbmc/regression/jbmc/assert5/test.desc +++ b/jbmc/regression/jbmc/assert5/test.desc @@ -1,6 +1,6 @@ CORE assert5 - +-cp target/classes ^EXIT=0$ ^SIGNAL=0$ ^VERIFICATION SUCCESSFUL$ diff --git a/jbmc/regression/jbmc/pom.xml b/jbmc/regression/jbmc/pom.xml index 6ca72e8e543..e78ace00ef0 100644 --- a/jbmc/regression/jbmc/pom.xml +++ b/jbmc/regression/jbmc/pom.xml @@ -44,6 +44,7 @@ assert2 assert3 assert4 + assert5 classpath-jar-load-whole-jar From cf4c3e4b8963d064d249ef4efd706f71927f5d2c Mon Sep 17 00:00:00 2001 From: Peter Schrammel Date: Thu, 2 Jan 2025 19:24:43 +0100 Subject: [PATCH 30/47] Compile jbmc/assert6 test sources Add pom.xml for compilation, move sources, remove obsolete pre-compiled class files. --- jbmc/regression/jbmc/assert6/assert6.class | Bin 503 -> 0 bytes jbmc/regression/jbmc/assert6/pom.xml | 30 ++++++++++++++++++ .../assert6/{ => src/main/java}/assert6.java | 0 jbmc/regression/jbmc/assert6/test.desc | 2 +- jbmc/regression/jbmc/pom.xml | 1 + 5 files changed, 32 insertions(+), 1 deletion(-) delete mode 100644 jbmc/regression/jbmc/assert6/assert6.class create mode 100644 jbmc/regression/jbmc/assert6/pom.xml rename jbmc/regression/jbmc/assert6/{ => src/main/java}/assert6.java (100%) diff --git a/jbmc/regression/jbmc/assert6/assert6.class b/jbmc/regression/jbmc/assert6/assert6.class deleted file mode 100644 index 82ff1d37483390652c29ba0e57fe5905295ad72e..0000000000000000000000000000000000000000 GIT binary patch literal 0 HcmV?d00001 literal 503 zcmYjN+e$(~6kX$O)U?#RWooyVqd^)(FO?8cU|2y$AU%zGkTIPT$7A$6^#{EqB-DFf z(oYoaITf{GW?yEnwb!1v&*v8aTUZNY25F9rpHgk*Fg(cWYk?yd#9|m6d5!`{ks+`v zm2_$hUZZr$;5)FoCc|7qD)V$aY@7ClXb-638w#ly(#BPzFK$I;AXKl?bZn`5I~o{m zI-+xZB5vG%8qW}JT4TFo9!ZUlh|$Qjo$U>cjv#_4L(F9wJ91Dt7piLwb$uyO)C zeD~58G+2M0HV+-r2!>gT3gj7ie|ZA-NCEv2-2u1A5JC)bigjxjK6uHOrtq|q@J`@w ztUn>Jmydhj?~&B*0nsUVD-oO^^s4DRE?tfYX$C3aL>NMb)D$T*NJ)ZTLSP>-IOesO Iqzg-Z0W(Kj*Z=?k diff --git a/jbmc/regression/jbmc/assert6/pom.xml b/jbmc/regression/jbmc/assert6/pom.xml new file mode 100644 index 00000000000..204345594ad --- /dev/null +++ b/jbmc/regression/jbmc/assert6/pom.xml @@ -0,0 +1,30 @@ + + + 4.0.0 + org.cprover.regression + regression.jbmc.assert6 + 1.0-SNAPSHOT + + + org.cprover.regression + regression.jbmc + 1.0-SNAPSHOT + + + + + + maven-jar-plugin + + + default-jar + none + + + + + + + diff --git a/jbmc/regression/jbmc/assert6/assert6.java b/jbmc/regression/jbmc/assert6/src/main/java/assert6.java similarity index 100% rename from jbmc/regression/jbmc/assert6/assert6.java rename to jbmc/regression/jbmc/assert6/src/main/java/assert6.java diff --git a/jbmc/regression/jbmc/assert6/test.desc b/jbmc/regression/jbmc/assert6/test.desc index fc3a3f08b34..459b70ed04c 100644 --- a/jbmc/regression/jbmc/assert6/test.desc +++ b/jbmc/regression/jbmc/assert6/test.desc @@ -1,6 +1,6 @@ CORE assert6 - +-cp target/classes ^EXIT=0$ ^SIGNAL=0$ ^VERIFICATION SUCCESSFUL$ diff --git a/jbmc/regression/jbmc/pom.xml b/jbmc/regression/jbmc/pom.xml index e78ace00ef0..1bf97aa1627 100644 --- a/jbmc/regression/jbmc/pom.xml +++ b/jbmc/regression/jbmc/pom.xml @@ -45,6 +45,7 @@ assert3 assert4 assert5 + assert6 classpath-jar-load-whole-jar From 2811d0ef7a8007095e5e275d2b36e67d6a4978ba Mon Sep 17 00:00:00 2001 From: Peter Schrammel Date: Thu, 2 Jan 2025 19:25:01 +0100 Subject: [PATCH 31/47] Compile jbmc/assert7 test sources Add pom.xml for compilation, move sources, remove obsolete pre-compiled class files. --- jbmc/regression/jbmc/assert7/Test.class | Bin 300 -> 0 bytes jbmc/regression/jbmc/assert7/pom.xml | 30 ++++++++++++++++++ .../assert7/{ => src/main/java}/Test.java | 0 jbmc/regression/jbmc/assert7/test.desc | 2 +- jbmc/regression/jbmc/pom.xml | 1 + 5 files changed, 32 insertions(+), 1 deletion(-) delete mode 100644 jbmc/regression/jbmc/assert7/Test.class create mode 100644 jbmc/regression/jbmc/assert7/pom.xml rename jbmc/regression/jbmc/assert7/{ => src/main/java}/Test.java (100%) diff --git a/jbmc/regression/jbmc/assert7/Test.class b/jbmc/regression/jbmc/assert7/Test.class deleted file mode 100644 index fbf9949d0e6ab0258388c62969571aa5c59c48a0..0000000000000000000000000000000000000000 GIT binary patch literal 0 HcmV?d00001 literal 300 zcmYL_L2JT55QX2wXf#@r_E35$^dhK-dhuo{l%l859+X1qX_GFpq8r$({;!^d7WxDH zQPP=Svar0z@Vz(7p3dLD0H(N#(L_H&5+e{zBU}<%55^k*NN5a4Z-nr<{M3XbGgiOs zce!>em2Y_x?v$~F>)}VXQ3o~ID!ZO6y)$+_lVH3o_pZD}OIs4=qH5n>zDU zRoZz|+PQP3<6>b6X-&N58(nzZA>;?k3HWji2yJ$^ti;+JA3;hI{M-T>Jr&sWssM diff --git a/jbmc/regression/jbmc/assert7/pom.xml b/jbmc/regression/jbmc/assert7/pom.xml new file mode 100644 index 00000000000..acb58d24590 --- /dev/null +++ b/jbmc/regression/jbmc/assert7/pom.xml @@ -0,0 +1,30 @@ + + + 4.0.0 + org.cprover.regression + regression.jbmc.assert7 + 1.0-SNAPSHOT + + + org.cprover.regression + regression.jbmc + 1.0-SNAPSHOT + + + + + + maven-jar-plugin + + + default-jar + none + + + + + + + diff --git a/jbmc/regression/jbmc/assert7/Test.java b/jbmc/regression/jbmc/assert7/src/main/java/Test.java similarity index 100% rename from jbmc/regression/jbmc/assert7/Test.java rename to jbmc/regression/jbmc/assert7/src/main/java/Test.java diff --git a/jbmc/regression/jbmc/assert7/test.desc b/jbmc/regression/jbmc/assert7/test.desc index dfca31f92d2..a7844ed0c9d 100644 --- a/jbmc/regression/jbmc/assert7/test.desc +++ b/jbmc/regression/jbmc/assert7/test.desc @@ -1,6 +1,6 @@ CORE Test - +-cp target/classes ^EXIT=0$ ^SIGNAL=0$ ^VERIFICATION SUCCESSFUL$ diff --git a/jbmc/regression/jbmc/pom.xml b/jbmc/regression/jbmc/pom.xml index 1bf97aa1627..62f87d39cb7 100644 --- a/jbmc/regression/jbmc/pom.xml +++ b/jbmc/regression/jbmc/pom.xml @@ -46,6 +46,7 @@ assert4 assert5 assert6 + assert7 classpath-jar-load-whole-jar From 0bac843a30e8b0f7fbed30c8998b2692452a1444 Mon Sep 17 00:00:00 2001 From: Peter Schrammel Date: Thu, 2 Jan 2025 19:25:37 +0100 Subject: [PATCH 32/47] Compile jbmc/assert-no-exceptions-thrown test sources Add pom.xml for compilation, move sources, remove obsolete pre-compiled class files. --- .../MyException.class | Bin 192 -> 0 bytes .../assert-no-exceptions-thrown/Test.class | Bin 964 -> 0 bytes .../assert-no-exceptions-thrown/Thrower.class | Bin 1455 -> 0 bytes .../jbmc/assert-no-exceptions-thrown/pom.xml | 30 ++++++++++++++++++ .../{ => src/main/java}/Test.java | 0 .../{ => src/main/java}/Thrower.java | 0 .../test-thrower.desc | 2 +- .../test-with-throw.desc | 2 +- .../assert-no-exceptions-thrown/test.desc | 2 +- jbmc/regression/jbmc/pom.xml | 1 + 10 files changed, 34 insertions(+), 3 deletions(-) delete mode 100644 jbmc/regression/jbmc/assert-no-exceptions-thrown/MyException.class delete mode 100644 jbmc/regression/jbmc/assert-no-exceptions-thrown/Test.class delete mode 100644 jbmc/regression/jbmc/assert-no-exceptions-thrown/Thrower.class create mode 100644 jbmc/regression/jbmc/assert-no-exceptions-thrown/pom.xml rename jbmc/regression/jbmc/assert-no-exceptions-thrown/{ => src/main/java}/Test.java (100%) rename jbmc/regression/jbmc/assert-no-exceptions-thrown/{ => src/main/java}/Thrower.java (100%) diff --git a/jbmc/regression/jbmc/assert-no-exceptions-thrown/MyException.class b/jbmc/regression/jbmc/assert-no-exceptions-thrown/MyException.class deleted file mode 100644 index 5578fa11a8f315cee834ac189ccca4cbadae3b8c..0000000000000000000000000000000000000000 GIT binary patch literal 0 HcmV?d00001 literal 192 zcmX^0Z`VEs1_l!bUM>b^1}=66ZgvJ9Mg}&U%)HDJJ4Oa(4b3n{1{UZ1lvG9rexJ;| zRKL>Pq|~C2#H1Xc2v=}^X;E^jTPBFZ8IoFDqL-CemdL}v!obSN!0lVH^YiK$a|!28pn0ZD(NI2$p6Cl5Ai>kQ4`y I$Hc%105{kpi2wiq diff --git a/jbmc/regression/jbmc/assert-no-exceptions-thrown/Test.class b/jbmc/regression/jbmc/assert-no-exceptions-thrown/Test.class deleted file mode 100644 index 9b30d4d418e8e5e87211093334a7f249582c8833..0000000000000000000000000000000000000000 GIT binary patch literal 0 HcmV?d00001 literal 964 zcmZWnOHUJF6g^)%4?3NeQWS@lw}?QM8q>H!QbbHlco-lgvYSr7$UteybgJ-ISh4Gd z4VsA2ME3p?e}gf`^9_$GZ0_qjbI-Z=&W}G|zXK?tXd#VJ6Jr))%HOx3DL-z(z^DZq z4-zyJCLUU_)XSuWDNLIv2=tD-&87@Ozfo_#^qX#_CaVHsOTd`*>wY*V5TBgd6wnqL zRVmQDh=&3J)#U~=~T*u!&u2Si0em=k<#;%9b@#B+!x+5 zuOFl5BN9hSnML;Gd0x9!YUA0`|DZO;Z&k84DyN8(r+^u%P`(`T7O+M|7gNn~x!^21 z_hoTo4)qVx7BI}O`cb6n=Zwq9W1jP_GF~HM9Yb(25>4x%>o*+n3)vSY@@bj@Wd_sS r(9re4O3@8~o~->DsUw(L8(RDm66$ytVy=#-R;VLpm(_`fqvw&ob0Vyk diff --git a/jbmc/regression/jbmc/assert-no-exceptions-thrown/Thrower.class b/jbmc/regression/jbmc/assert-no-exceptions-thrown/Thrower.class deleted file mode 100644 index ed6f21fd4e383252f3fe82263b317877a38a25a5..0000000000000000000000000000000000000000 GIT binary patch literal 0 HcmV?d00001 literal 1455 zcmZux&vV;E7=0VdURhRaM^4%#)Pa`J+OC_FCWVruC64P-Q^n5UPMKtegJN%81xF70 z5lZ6x?On@&upW#&A+_ZMAnXct@W@?TvI>KF$i6@%A)%tkF+79`2Y>qO6y4dRW z>ub$k;I_mqTUOKWK5%=V3U^u-({Tnl2IyEug$`1wR2hbky++b*GGqoo(|2vB!w@gm z8p~B3Ror42DpR&nFE=T~>Z`Q<9&R(78KhOZ)QpPd`PGLlu`PSTFg1YdqGS2?jwrjX z^;y$?BqFrQ2rcM#S9>N@c147xg{RdmZw_6cBAH}JD&1s8=jlgf*U+x7?+xw5I zV*;<}sNsEvu}IR9j8)g|xeUDDNRB%?Osu@rpT@?fXpv|WgZvKy$G5klS5oN;_pEL} zs*nY0)Vq953d(onX5+rpyjJ)h)frNL&y*@sFDZK@A7veCvp@zDp9EIdV;GHE=kRC? z1#)0|aJo<#dSP35wkz7@qsx-F{D4Z(0oQSstUgX(4acW(ib_JC+SH>auedk z1F$EOh*xP&gqsXWyhbHLD*K&MIT2FEkXihhC5roqeMwvqW>E=>XK7reQKiwKv1Tad zQ^eO|2S}`xegv=YVb)O1#P`~~GOno8-y(U(&`dSf4Ob~M^VbiE&&LhjWb=vf#6C`Z zxQE@9(oZ<~7!zM3yNi*FhO&>5U8J63bnO7Ao)emmps8bMCW7k6(BTNG9Yc)>s=kaq zp-XdY!^6pbO!s4^ABX$Vz);xOM`71v)Jlbr1WKSk7Pa{rG+ajtOH`?XG;SkDM9cHc7Q@`VV?I2OsD0IWFJ}6z~{Dd_@%xa0$Os)!%R#f8YxK#4OWD zmUARX4*Cm}I9|`DlgZRF$J7f<(wxiX{w7ex8=)nnHReJO0K>-VeT?mbD|=94-ykb( Va(J5~o5;#>4CzbKOy@)R!oS46JbnNG diff --git a/jbmc/regression/jbmc/assert-no-exceptions-thrown/pom.xml b/jbmc/regression/jbmc/assert-no-exceptions-thrown/pom.xml new file mode 100644 index 00000000000..ac82dea6dcd --- /dev/null +++ b/jbmc/regression/jbmc/assert-no-exceptions-thrown/pom.xml @@ -0,0 +1,30 @@ + + + 4.0.0 + org.cprover.regression + regression.jbmc.assert-no-exceptions-thrown + 1.0-SNAPSHOT + + + org.cprover.regression + regression.jbmc + 1.0-SNAPSHOT + + + + + + maven-jar-plugin + + + default-jar + none + + + + + + + diff --git a/jbmc/regression/jbmc/assert-no-exceptions-thrown/Test.java b/jbmc/regression/jbmc/assert-no-exceptions-thrown/src/main/java/Test.java similarity index 100% rename from jbmc/regression/jbmc/assert-no-exceptions-thrown/Test.java rename to jbmc/regression/jbmc/assert-no-exceptions-thrown/src/main/java/Test.java diff --git a/jbmc/regression/jbmc/assert-no-exceptions-thrown/Thrower.java b/jbmc/regression/jbmc/assert-no-exceptions-thrown/src/main/java/Thrower.java similarity index 100% rename from jbmc/regression/jbmc/assert-no-exceptions-thrown/Thrower.java rename to jbmc/regression/jbmc/assert-no-exceptions-thrown/src/main/java/Thrower.java diff --git a/jbmc/regression/jbmc/assert-no-exceptions-thrown/test-thrower.desc b/jbmc/regression/jbmc/assert-no-exceptions-thrown/test-thrower.desc index bae55e9bae2..322add66010 100644 --- a/jbmc/regression/jbmc/assert-no-exceptions-thrown/test-thrower.desc +++ b/jbmc/regression/jbmc/assert-no-exceptions-thrown/test-thrower.desc @@ -1,6 +1,6 @@ CORE Thrower ---function Thrower.test --assert-no-exceptions-thrown --throw-runtime-exceptions +--function Thrower.test --assert-no-exceptions-thrown --throw-runtime-exceptions -cp target/classes line 39 assertion at file Thrower.java line 39 .*: FAILURE line 42 assertion at file Thrower.java line 42 .*: FAILURE line 45 assertion at file Thrower.java line 45 .*: FAILURE diff --git a/jbmc/regression/jbmc/assert-no-exceptions-thrown/test-with-throw.desc b/jbmc/regression/jbmc/assert-no-exceptions-thrown/test-with-throw.desc index 55fc3ff7220..a62f286ec54 100644 --- a/jbmc/regression/jbmc/assert-no-exceptions-thrown/test-with-throw.desc +++ b/jbmc/regression/jbmc/assert-no-exceptions-thrown/test-with-throw.desc @@ -1,6 +1,6 @@ CORE Test ---function Test.check +--function Test.check -cp target/classes line 22 assertion at file Test.java line 22 .*: FAILURE line 24 assertion at file Test.java line 24 .*: FAILURE line 26 assertion at file Test.java line 26 .*: FAILURE diff --git a/jbmc/regression/jbmc/assert-no-exceptions-thrown/test.desc b/jbmc/regression/jbmc/assert-no-exceptions-thrown/test.desc index e1536ea9097..c893a47825f 100644 --- a/jbmc/regression/jbmc/assert-no-exceptions-thrown/test.desc +++ b/jbmc/regression/jbmc/assert-no-exceptions-thrown/test.desc @@ -1,6 +1,6 @@ CORE Test ---function Test.check --assert-no-exceptions-thrown +--function Test.check --assert-no-exceptions-thrown -cp target/classes line 6 assertion at file Test.java line 6 .*: FAILURE line 8 assertion at file Test.java line 8 .*: FAILURE line 10 assertion at file Test.java line 10 .*: FAILURE diff --git a/jbmc/regression/jbmc/pom.xml b/jbmc/regression/jbmc/pom.xml index 62f87d39cb7..af8d4eaa459 100644 --- a/jbmc/regression/jbmc/pom.xml +++ b/jbmc/regression/jbmc/pom.xml @@ -47,6 +47,7 @@ assert5 assert6 assert7 + assert-no-exceptions-thrown classpath-jar-load-whole-jar From 76ab93702ef967c8f5995699f4a59b0079719c32 Mon Sep 17 00:00:00 2001 From: Peter Schrammel Date: Thu, 2 Jan 2025 19:26:24 +0100 Subject: [PATCH 33/47] Compile jbmc/assertion_error_constructors test sources Add pom.xml for compilation, move sources, remove obsolete pre-compiled class files. --- .../AssertionIssue.class | Bin 556 -> 0 bytes .../jbmc/assertion_error_constructors/pom.xml | 30 ++++++++++++++++++ .../{ => src/main/java}/AssertionIssue.java | 0 .../assertion_error_constructors/test.desc | 2 +- jbmc/regression/jbmc/pom.xml | 1 + 5 files changed, 32 insertions(+), 1 deletion(-) delete mode 100644 jbmc/regression/jbmc/assertion_error_constructors/AssertionIssue.class create mode 100644 jbmc/regression/jbmc/assertion_error_constructors/pom.xml rename jbmc/regression/jbmc/assertion_error_constructors/{ => src/main/java}/AssertionIssue.java (100%) diff --git a/jbmc/regression/jbmc/assertion_error_constructors/AssertionIssue.class b/jbmc/regression/jbmc/assertion_error_constructors/AssertionIssue.class deleted file mode 100644 index a9312303951fc670042fcc5d3a7346dcfd005cda..0000000000000000000000000000000000000000 GIT binary patch literal 0 HcmV?d00001 literal 556 zcmZWmO;5r=5Pb`ULPg|56h8xr2jBn)j~Ej}G$Cp903qSn;s%zKZL%#Af0ic_N%ZcI zGR{_0H11($=gphZhoFEVeI=v_uNjh!=7_=Q`H!4o&lZy3FBdLXLp@Jgwm)&ak)wpJ ze?TLg3DPLov3@@Ymb}Z554Cj+Ggt$EsV4kRXt8qKi1_Wf^W@~PgB(Lu-#eZor=6H| ztCX)8&IkU2lcSv0R$PX)kSirz@42>8zMQrh>hVM*d+~pLZE{Ml`%9z^wyqEEoKHfA zR>R(cgHVxe_ZJdtcbg;BVbZVACjqASptws_hccs_YOTRuqIRBQIs)k{(_K@EfC7q? vvna*GO+xi4Zjcz4k{cM~HBxJ&-wC80D1HkW + + 4.0.0 + org.cprover.regression + regression.jbmc.assertion_error_constructors + 1.0-SNAPSHOT + + + org.cprover.regression + regression.jbmc + 1.0-SNAPSHOT + + + + + + maven-jar-plugin + + + default-jar + none + + + + + + + diff --git a/jbmc/regression/jbmc/assertion_error_constructors/AssertionIssue.java b/jbmc/regression/jbmc/assertion_error_constructors/src/main/java/AssertionIssue.java similarity index 100% rename from jbmc/regression/jbmc/assertion_error_constructors/AssertionIssue.java rename to jbmc/regression/jbmc/assertion_error_constructors/src/main/java/AssertionIssue.java diff --git a/jbmc/regression/jbmc/assertion_error_constructors/test.desc b/jbmc/regression/jbmc/assertion_error_constructors/test.desc index f138c827612..9c70224212b 100644 --- a/jbmc/regression/jbmc/assertion_error_constructors/test.desc +++ b/jbmc/regression/jbmc/assertion_error_constructors/test.desc @@ -1,6 +1,6 @@ CORE AssertionIssue ---function AssertionIssue.throwAssertion +--function AssertionIssue.throwAssertion -cp target/classes ^EXIT=10$ ^SIGNAL=0$ ^VERIFICATION FAILED$ diff --git a/jbmc/regression/jbmc/pom.xml b/jbmc/regression/jbmc/pom.xml index af8d4eaa459..6264ab2489a 100644 --- a/jbmc/regression/jbmc/pom.xml +++ b/jbmc/regression/jbmc/pom.xml @@ -48,6 +48,7 @@ assert6 assert7 assert-no-exceptions-thrown + assertion_error_constructors classpath-jar-load-whole-jar From 3de1908a25d842722c50733457906c26a16c8be2 Mon Sep 17 00:00:00 2001 From: Peter Schrammel Date: Fri, 3 Jan 2025 11:53:49 +0100 Subject: [PATCH 34/47] Make Java regression test compilation depend on models-library First build java-models-library which also downloads cprover-api.jar. Then compile java-regression. --- jbmc/CMakeLists.txt | 2 ++ jbmc/src/jbmc/CMakeLists.txt | 4 ++-- 2 files changed, 4 insertions(+), 2 deletions(-) diff --git a/jbmc/CMakeLists.txt b/jbmc/CMakeLists.txt index 561f89a5799..e5e05070c50 100644 --- a/jbmc/CMakeLists.txt +++ b/jbmc/CMakeLists.txt @@ -56,3 +56,5 @@ add_custom_command(OUTPUT ${java_regression_compiled_sources} add_custom_target(java-regression ALL DEPENDS ${java_regression_compiled_sources} ) + +add_dependencies(java-regression java-models-library) diff --git a/jbmc/src/jbmc/CMakeLists.txt b/jbmc/src/jbmc/CMakeLists.txt index c1735e3ed94..3772687126a 100644 --- a/jbmc/src/jbmc/CMakeLists.txt +++ b/jbmc/src/jbmc/CMakeLists.txt @@ -32,8 +32,8 @@ add_executable(jbmc jbmc_main.cpp) target_link_libraries(jbmc jbmc-lib) install(TARGETS jbmc DESTINATION ${CMAKE_INSTALL_BINDIR}) -# make sure java-models-library and java-regression is built at least once -add_dependencies(jbmc java-models-library java-regression) +# make sure java-models-library (on which java-regression depends) is built at least once +add_dependencies(jbmc java-regression) # Man page if(NOT WIN32) From c8fe05c985651a3a74c41aafbf1d0d2a4b3acc51 Mon Sep 17 00:00:00 2001 From: Peter Schrammel Date: Thu, 2 Jan 2025 20:42:38 +0100 Subject: [PATCH 35/47] Compile jbmc/assume1 test sources Add pom.xml for compilation, move sources, remove obsolete pre-compiled class files. --- jbmc/regression/jbmc/assume1/Assume1.class | Bin 660 -> 0 bytes jbmc/regression/jbmc/assume1/pom.xml | 37 ++++++++++++++++++ .../assume1/{ => src/main/java}/Assume1.java | 0 jbmc/regression/jbmc/assume1/test.desc | 2 +- jbmc/regression/jbmc/pom.xml | 1 + jbmc/regression/pom.xml | 12 ++++++ 6 files changed, 51 insertions(+), 1 deletion(-) delete mode 100644 jbmc/regression/jbmc/assume1/Assume1.class create mode 100644 jbmc/regression/jbmc/assume1/pom.xml rename jbmc/regression/jbmc/assume1/{ => src/main/java}/Assume1.java (100%) diff --git a/jbmc/regression/jbmc/assume1/Assume1.class b/jbmc/regression/jbmc/assume1/Assume1.class deleted file mode 100644 index b9a49bc9971d81889935e4cefba60fffd292840c..0000000000000000000000000000000000000000 GIT binary patch literal 0 HcmV?d00001 literal 660 zcmZWmO>fgc5PcIn-o!OcnwAp6M*}U8a==3BjS3Y7kSc`_sZ}L%K-xIlvc=6-Yp3G3 zRN{uj8IULf3GVzT#H_KJ1Bda<&b)c^X8ill_n!bZupXj@PKYbGT1S9u0@p+M=m@NY z=;DUJO~T@u%ra$jZ6?`coyk$E#snG?f=xZq`9p%&Ti+x2eKS^s#z0Th^Xbt@*7KOOz00JZztI_?K6sR6(<62N0n_Xo!!*5Z$42kiwh0$@a+$n+CXdU$+GdiL zW5XRYwTXJF-H@o{xpyc}WP~|H0;>_$a4SL`A))OGaVjSVF+=|?^u$_Y38L&3xE_MCyTXUjp+<#ekzJV;{JJ~}gyD@9*r(7c}k5#6v8lMm4h4LvE z_-aGGa=`xppk~|2fJNYCk`r@=WkFXJv2CWPzIoh1@<+xu*ezL z{F>3O*6jozApDQ;y>F;|hIfia=RM|rz<+gy>MzIZ6} + + 4.0.0 + org.cprover.regression + regression.jbmc.assume1 + 1.0-SNAPSHOT + + + org.cprover.regression + regression.jbmc + 1.0-SNAPSHOT + + + + + org.cprover.util + cprover-api + + + + + + + maven-jar-plugin + + + default-jar + none + + + + + + + diff --git a/jbmc/regression/jbmc/assume1/Assume1.java b/jbmc/regression/jbmc/assume1/src/main/java/Assume1.java similarity index 100% rename from jbmc/regression/jbmc/assume1/Assume1.java rename to jbmc/regression/jbmc/assume1/src/main/java/Assume1.java diff --git a/jbmc/regression/jbmc/assume1/test.desc b/jbmc/regression/jbmc/assume1/test.desc index 5cfc6ec2841..9078c1ab3da 100644 --- a/jbmc/regression/jbmc/assume1/test.desc +++ b/jbmc/regression/jbmc/assume1/test.desc @@ -1,6 +1,6 @@ CORE Assume1 ---function Assume1.foo +--function Assume1.foo -cp target/classes ^EXIT=0$ ^SIGNAL=0$ ^VERIFICATION SUCCESSFUL$ diff --git a/jbmc/regression/jbmc/pom.xml b/jbmc/regression/jbmc/pom.xml index 6264ab2489a..355ebd303bf 100644 --- a/jbmc/regression/jbmc/pom.xml +++ b/jbmc/regression/jbmc/pom.xml @@ -49,6 +49,7 @@ assert7 assert-no-exceptions-thrown assertion_error_constructors + assume1 classpath-jar-load-whole-jar diff --git a/jbmc/regression/pom.xml b/jbmc/regression/pom.xml index 16dab954a94..8054d3a1f3d 100644 --- a/jbmc/regression/pom.xml +++ b/jbmc/regression/pom.xml @@ -20,6 +20,18 @@ book-examples + + + + org.cprover.util + cprover-api + 1.0.0 + system + ${maven.multiModuleProjectDirectory}/../lib/java-models-library/target/cprover-api.jar + + + + From 76423e04bb50a9caee2f391053d62e58c75d6bc2 Mon Sep 17 00:00:00 2001 From: Peter Schrammel Date: Thu, 2 Jan 2025 20:54:50 +0100 Subject: [PATCH 36/47] Compile jbmc/assume2 test sources Add pom.xml for compilation, move sources, remove obsolete pre-compiled class files. --- jbmc/regression/jbmc/assume2/Assume2.class | Bin 661 -> 0 bytes jbmc/regression/jbmc/assume2/pom.xml | 37 ++++++++++++++++++ .../assume2/{ => src/main/java}/Assume2.java | 0 jbmc/regression/jbmc/assume2/test.desc | 2 +- jbmc/regression/jbmc/pom.xml | 1 + 5 files changed, 39 insertions(+), 1 deletion(-) delete mode 100644 jbmc/regression/jbmc/assume2/Assume2.class create mode 100644 jbmc/regression/jbmc/assume2/pom.xml rename jbmc/regression/jbmc/assume2/{ => src/main/java}/Assume2.java (100%) diff --git a/jbmc/regression/jbmc/assume2/Assume2.class b/jbmc/regression/jbmc/assume2/Assume2.class deleted file mode 100644 index 36e09875d7d72406f27d2512b116cd7a586871d6..0000000000000000000000000000000000000000 GIT binary patch literal 0 HcmV?d00001 literal 661 zcmZWmO>fgc5PcIn-qzUno^WK~BuixK(09eCnga*11F5qH_0G9+VNAS@VxDw$i zdIHx7iz_nEl`XWH<_~o)$C;WCXhaCs^;8%430{A7hu{y)L=l=pJylO<`(tId9hlG_ znp9>x(rS0F9{u9A&I#f0L7va{)!lnc^U4^e>2EqVddp{%aAvEJ>6<6=pz3R^r&%Q% zZJC)()nn~M;)>_ao;;K><`4^9kFkOqF+xOyjw>XYobDzJ{X5VjYmFs{s#oAy0JN~cv4J)g`NcKA zWVEaGy1{!0{{wvQD{7zM9ii0~?=bfr{)=POe>!5XB%Uwz1-CcYTlkMa4`;E&xMe;8 pyl{h-7<2B#=~^iTEVP3!5J#2XXL$d+b`*8g;te-jhc7jp{{vk5b}Ik? diff --git a/jbmc/regression/jbmc/assume2/pom.xml b/jbmc/regression/jbmc/assume2/pom.xml new file mode 100644 index 00000000000..7bddbf26f38 --- /dev/null +++ b/jbmc/regression/jbmc/assume2/pom.xml @@ -0,0 +1,37 @@ + + + 4.0.0 + org.cprover.regression + regression.jbmc.assume2 + 1.0-SNAPSHOT + + + org.cprover.regression + regression.jbmc + 1.0-SNAPSHOT + + + + + org.cprover.util + cprover-api + + + + + + + maven-jar-plugin + + + default-jar + none + + + + + + + diff --git a/jbmc/regression/jbmc/assume2/Assume2.java b/jbmc/regression/jbmc/assume2/src/main/java/Assume2.java similarity index 100% rename from jbmc/regression/jbmc/assume2/Assume2.java rename to jbmc/regression/jbmc/assume2/src/main/java/Assume2.java diff --git a/jbmc/regression/jbmc/assume2/test.desc b/jbmc/regression/jbmc/assume2/test.desc index 10be6fca773..1efbe6bdef5 100644 --- a/jbmc/regression/jbmc/assume2/test.desc +++ b/jbmc/regression/jbmc/assume2/test.desc @@ -1,6 +1,6 @@ CORE Assume2 ---function Assume2.foo +--function Assume2.foo -cp target/classes ^EXIT=10$ ^SIGNAL=0$ ^VERIFICATION FAILED$ diff --git a/jbmc/regression/jbmc/pom.xml b/jbmc/regression/jbmc/pom.xml index 355ebd303bf..e90f8014305 100644 --- a/jbmc/regression/jbmc/pom.xml +++ b/jbmc/regression/jbmc/pom.xml @@ -50,6 +50,7 @@ assert-no-exceptions-thrown assertion_error_constructors assume1 + assume2 classpath-jar-load-whole-jar From b4c7470a31d070d9a392effde408becfc250a076 Mon Sep 17 00:00:00 2001 From: Peter Schrammel Date: Thu, 2 Jan 2025 20:55:25 +0100 Subject: [PATCH 37/47] Compile jbmc/assume3 test sources Add pom.xml for compilation, move sources, remove obsolete pre-compiled class files. --- jbmc/regression/jbmc/assume3/Assume3.class | Bin 684 -> 0 bytes jbmc/regression/jbmc/assume3/pom.xml | 37 ++++++++++++++++++ .../assume3/{ => src/main/java}/Assume3.java | 0 jbmc/regression/jbmc/assume3/test.desc | 2 +- jbmc/regression/jbmc/pom.xml | 1 + 5 files changed, 39 insertions(+), 1 deletion(-) delete mode 100644 jbmc/regression/jbmc/assume3/Assume3.class create mode 100644 jbmc/regression/jbmc/assume3/pom.xml rename jbmc/regression/jbmc/assume3/{ => src/main/java}/Assume3.java (100%) diff --git a/jbmc/regression/jbmc/assume3/Assume3.class b/jbmc/regression/jbmc/assume3/Assume3.class deleted file mode 100644 index 916ad4065fb77e04ba492a6f7499799ea22c85f7..0000000000000000000000000000000000000000 GIT binary patch literal 0 HcmV?d00001 literal 684 zcmZuvO>fgc5PcIn-qjFF61OtQv!_%-mcDc`H0~3xAqC{AfGBid#E$Dx0p|qd2PXj?l4be zx-X5k>w42I-|B+k51$mpVy+(UaD%zj8DYKuW_T!%Wt_@v7LQ7!v)N8HK$;m-qW_c$ z=SHPW-o21Vb^q3GlGgHqQNA#VdakXQu%7q8jtH@WP~dimP236LBOvsavl;rw_%ma2 zLl8Ar;BJU}=o30i@XN`eN=lZOn^~M3nfzFpc<`!!rOU4pOeM?WroX zQPZ=bY^YptflqhLx8dVCzK834g7dFP%Wt9)KDJhRylCLkZyo7^Z2$lO diff --git a/jbmc/regression/jbmc/assume3/pom.xml b/jbmc/regression/jbmc/assume3/pom.xml new file mode 100644 index 00000000000..0e6f183f5b2 --- /dev/null +++ b/jbmc/regression/jbmc/assume3/pom.xml @@ -0,0 +1,37 @@ + + + 4.0.0 + org.cprover.regression + regression.jbmc.assume3 + 1.0-SNAPSHOT + + + org.cprover.regression + regression.jbmc + 1.0-SNAPSHOT + + + + + org.cprover.util + cprover-api + + + + + + + maven-jar-plugin + + + default-jar + none + + + + + + + diff --git a/jbmc/regression/jbmc/assume3/Assume3.java b/jbmc/regression/jbmc/assume3/src/main/java/Assume3.java similarity index 100% rename from jbmc/regression/jbmc/assume3/Assume3.java rename to jbmc/regression/jbmc/assume3/src/main/java/Assume3.java diff --git a/jbmc/regression/jbmc/assume3/test.desc b/jbmc/regression/jbmc/assume3/test.desc index 04509cf4cbc..e3d7203f32e 100644 --- a/jbmc/regression/jbmc/assume3/test.desc +++ b/jbmc/regression/jbmc/assume3/test.desc @@ -1,6 +1,6 @@ CORE Assume3 - +-cp target/classes ^EXIT=0$ ^SIGNAL=0$ ^VERIFICATION SUCCESSFUL$ diff --git a/jbmc/regression/jbmc/pom.xml b/jbmc/regression/jbmc/pom.xml index e90f8014305..d24d664c287 100644 --- a/jbmc/regression/jbmc/pom.xml +++ b/jbmc/regression/jbmc/pom.xml @@ -51,6 +51,7 @@ assertion_error_constructors assume1 assume2 + assume3 classpath-jar-load-whole-jar From aa4e88f7310b10e3c58b3fdd9b61730b2d6bf658 Mon Sep 17 00:00:00 2001 From: Peter Schrammel Date: Thu, 2 Jan 2025 20:56:39 +0100 Subject: [PATCH 38/47] Compile jbmc/assume-inputs-integral test sources Add pom.xml for compilation, move sources, remove obsolete pre-compiled class files. --- .../jbmc/assume-inputs-integral/My.class | Bin 3207 -> 0 bytes .../jbmc/assume-inputs-integral/Other.class | Bin 321 -> 0 bytes .../OtherNoClinit.class | Bin 296 -> 0 bytes .../assume-inputs-integral/arg_assume.desc | 2 +- .../class_arr_assume.desc | 2 +- .../assume-inputs-integral/class_assume.desc | 2 +- .../assume-inputs-integral/field_assume.desc | 2 +- .../field_assume_static.desc | 2 +- .../field_assume_static_no_clinit.desc | 2 +- .../jbmc/assume-inputs-integral/pom.xml | 30 ++++++++++++++++++ .../{ => src/main/java}/My.java | 0 .../{ => src/main/java}/Other.java | 0 .../{ => src/main/java}/OtherNoClinit.java | 0 jbmc/regression/jbmc/pom.xml | 1 + 14 files changed, 37 insertions(+), 6 deletions(-) delete mode 100644 jbmc/regression/jbmc/assume-inputs-integral/My.class delete mode 100644 jbmc/regression/jbmc/assume-inputs-integral/Other.class delete mode 100644 jbmc/regression/jbmc/assume-inputs-integral/OtherNoClinit.class create mode 100644 jbmc/regression/jbmc/assume-inputs-integral/pom.xml rename jbmc/regression/jbmc/assume-inputs-integral/{ => src/main/java}/My.java (100%) rename jbmc/regression/jbmc/assume-inputs-integral/{ => src/main/java}/Other.java (100%) rename jbmc/regression/jbmc/assume-inputs-integral/{ => src/main/java}/OtherNoClinit.java (100%) diff --git a/jbmc/regression/jbmc/assume-inputs-integral/My.class b/jbmc/regression/jbmc/assume-inputs-integral/My.class deleted file mode 100644 index e508f3a323b88859f79542fb8ba87a5df3bd5cf9..0000000000000000000000000000000000000000 GIT binary patch literal 0 HcmV?d00001 literal 3207 zcmb7`TX0iF7{~vcCOvJM&^AqzP%dIYDFwNSD6~*YLMYG{XiI@s(9<+PN@(CTMT$ZJ z6@dXo5Eww6afTUYL>UDJyba!8;6ao(ee%&a^+lh=|DNPrQo|r;CONzRZ!h2X+i!Qz zt$#kd31AM^xiKDLXTy;NJBl$D5d}-!a3ZWA>Kxt&IPb~7;je(ghCh~G_V50+Nx{;> z;osStPvJeIF#LB$DMk~P$-m`tJeJ00N-Jckxfm_-uL-TP+Nxls8>_HdL7RYkQ!=Hd zqltL3S3pDsN_ta+J;}JCLAOz9MGhEu(9fzswgf4p^YTTfi;kc|a=&8e80>{PXc ztY<}MdP`z}otj&Q>I6LfgWKX-g3TJW%>u5PXhaTKq&u!l#fEbG)|v_@Wl)@2)iiZTAJb!u*{wU} zO34WXOpjPDs*maY2*cf;8q{LMFGE*ahNkzaJ5>*+pw@%Qs1XQBVMbEz-#nwyAiG4< zQXHn#GDYR8a_KB3qA#n0b`KuG1P>lXwFeVrX%eaxba?O>9v5)53@KRSK_}McbYI!i z7msm7m(GU}^|uwUZSJtdDG=z54EHb?{4y9*PTiQ{E1^GAR5G^R^@7fG-5 zHyzV;ItG-5Wc<1gi30*tS)0MP;M-Mu1L9*A9GJ%cLR}Pif@M#p0j9GtP>h+FMTMP3 z4>w%_wL8^5$EkBDzk-5u`2KS^*WZBa%W9uuiXT~Gktv?H#9~uCXo!>jaGx;--ELF8 zrrKpwOHDOmQ_D?tx~WzlJ99Sc>u5vNJufk8l0$*cp$&eWfC4WnF^bSjiLQ(U%FzHH zqNqRz+dNBa9|F)2#6E;@2%~WtRd^R;@Bw>W#W;M;h5CVcBbf%sncOftyL5N(Bo|BY zY?Hj*m43g!l8@g@-cMm}mUkO@%f-4|dkq!&kn6fd{X-)lUAMrW%F!+Mdu+Pjj=wk8 zV6DK4T!Xa;vvUpBIy?~ha$*HHm75zX#LTT`-p*v^&S%y(5q=v}?|ClHR)QR2Qoh2p zJi!+4a8WK1=yjs}j?jL>)3)@z%i1#>R{}0UaVQuJhWL2NbDpsogq?5YefU<|vf9qK z(wCoar7u6iCn>ilx@SSh+U7pR~+gA{@;k{|(ij=MFy=a#$xX10X#dgS& zLw2-kj&6}%mZMu>XXWS*&2<$w>}nnYZQR)H%+3zx-5L_?L@U*-~u+{GM>X1P;m<}8`s;}V>in+7zhNIx-#Tv_H6GGq^sr?icjjI8Ho22;7-_QRUp&%e zxiHx<=`K9*Og^ArQ)wpMAg`{SJe^N-ciA!F#p_}W-Vil7F6QD*5ylCz8Yjg@yd{!2 zEq3FqIE3^1o|qs%H^kxWo{*)5Jk>c2OAWj$9C~*7P&TQms>(Y~rr1PT^75-_k-1&w n$R2#kePgd<+&L)Di*OcPMZtf+f8@4v!QojXzmghRabWSkTa2+c diff --git a/jbmc/regression/jbmc/assume-inputs-integral/Other.class b/jbmc/regression/jbmc/assume-inputs-integral/Other.class deleted file mode 100644 index f9446d51619ddd43cf53a6cc0ac65a790e528c69..0000000000000000000000000000000000000000 GIT binary patch literal 0 HcmV?d00001 literal 321 zcmXw!yH3ME5Jm4eet=`hgGWsX6u6-SMT&@0S)?FJL$$USveDv|mNoxH6^Vim;G+=Z zO(=nV;XUZveMAPtn6kg3|)0>U>5E)YR36Up+VaIYUn%8_$Ze-6}j}Q?%AV%W#0Eeu^!9!Rx hb~$TDqU$Z_lTCml&asDlEBkEMfB}YF5k|gi{0HdzJ9_{C diff --git a/jbmc/regression/jbmc/assume-inputs-integral/OtherNoClinit.class b/jbmc/regression/jbmc/assume-inputs-integral/OtherNoClinit.class deleted file mode 100644 index 95a3408e1db642855d66872460d49304f04be5a2..0000000000000000000000000000000000000000 GIT binary patch literal 0 HcmV?d00001 literal 296 zcmY*UyKcfT6g?O6DB;Z)bSwKpR5zqAF!y3Eijpkr1p+DGB3D zRdUz7=dyki93#v!QwV(&wQ}=68Q8PBI``h5WxX?N?aEe! + + 4.0.0 + org.cprover.regression + regression.jbmc.assume-inputs-integral + 1.0-SNAPSHOT + + + org.cprover.regression + regression.jbmc + 1.0-SNAPSHOT + + + + + + maven-jar-plugin + + + default-jar + none + + + + + + + diff --git a/jbmc/regression/jbmc/assume-inputs-integral/My.java b/jbmc/regression/jbmc/assume-inputs-integral/src/main/java/My.java similarity index 100% rename from jbmc/regression/jbmc/assume-inputs-integral/My.java rename to jbmc/regression/jbmc/assume-inputs-integral/src/main/java/My.java diff --git a/jbmc/regression/jbmc/assume-inputs-integral/Other.java b/jbmc/regression/jbmc/assume-inputs-integral/src/main/java/Other.java similarity index 100% rename from jbmc/regression/jbmc/assume-inputs-integral/Other.java rename to jbmc/regression/jbmc/assume-inputs-integral/src/main/java/Other.java diff --git a/jbmc/regression/jbmc/assume-inputs-integral/OtherNoClinit.java b/jbmc/regression/jbmc/assume-inputs-integral/src/main/java/OtherNoClinit.java similarity index 100% rename from jbmc/regression/jbmc/assume-inputs-integral/OtherNoClinit.java rename to jbmc/regression/jbmc/assume-inputs-integral/src/main/java/OtherNoClinit.java diff --git a/jbmc/regression/jbmc/pom.xml b/jbmc/regression/jbmc/pom.xml index d24d664c287..1bef6c82283 100644 --- a/jbmc/regression/jbmc/pom.xml +++ b/jbmc/regression/jbmc/pom.xml @@ -52,6 +52,7 @@ assume1 assume2 assume3 + assume-inputs-integral classpath-jar-load-whole-jar From b5bc805bef59aefc74878671581114c379148be4 Mon Sep 17 00:00:00 2001 From: Peter Schrammel Date: Thu, 2 Jan 2025 20:58:02 +0100 Subject: [PATCH 39/47] Compile jbmc/assume-inputs-interval test sources Add pom.xml for compilation, move sources, remove obsolete pre-compiled class files. --- .../jbmc/assume-inputs-interval/My.class | Bin 3780 -> 0 bytes .../jbmc/assume-inputs-interval/Other.class | Bin 414 -> 0 bytes .../OtherNoClinit.class | Bin 229 -> 0 bytes .../assume-inputs-interval/arg_assume.desc | 2 +- .../arg_assume_invalid2.desc | 2 +- .../arg_assume_invalid3.desc | 2 +- .../arg_assume_invalid4.desc | 2 +- .../arg_assume_invalid5.desc | 2 +- .../arg_assume_neg.desc | 2 +- .../arg_assume_singleton.desc | 2 +- .../arg_assume_union.desc | 2 +- .../class_arr_assume.desc | 2 +- .../assume-inputs-interval/class_assume.desc | 2 +- .../class_assume_lower.desc | 2 +- .../class_assume_upper.desc | 2 +- .../assume-inputs-interval/field_assume.desc | 2 +- .../field_assume_static.desc | 2 +- .../field_assume_static_no_clinit.desc | 2 +- .../jbmc/assume-inputs-interval/pom.xml | 30 ++++++++++++++++++ .../{ => src/main/java}/My.java | 0 .../{ => src/main/java}/Other.java | 0 .../{ => src/main/java}/OtherNoClinit.java | 0 jbmc/regression/jbmc/pom.xml | 1 + 23 files changed, 46 insertions(+), 15 deletions(-) delete mode 100644 jbmc/regression/jbmc/assume-inputs-interval/My.class delete mode 100644 jbmc/regression/jbmc/assume-inputs-interval/Other.class delete mode 100644 jbmc/regression/jbmc/assume-inputs-interval/OtherNoClinit.class create mode 100644 jbmc/regression/jbmc/assume-inputs-interval/pom.xml rename jbmc/regression/jbmc/assume-inputs-interval/{ => src/main/java}/My.java (100%) rename jbmc/regression/jbmc/assume-inputs-interval/{ => src/main/java}/Other.java (100%) rename jbmc/regression/jbmc/assume-inputs-interval/{ => src/main/java}/OtherNoClinit.java (100%) diff --git a/jbmc/regression/jbmc/assume-inputs-interval/My.class b/jbmc/regression/jbmc/assume-inputs-interval/My.class deleted file mode 100644 index 006b62236c4e722ab9e920f504500360c8eb9559..0000000000000000000000000000000000000000 GIT binary patch literal 0 HcmV?d00001 literal 3780 zcmb7GYiv|S6#i!0?Y7%3eeA0&@+cH2P+A@ZQ4so|g#x8O0g?B1yOb@n6qd`CY78T- zqhlGB_Lhb_JEKM_mP~X`k9CHrpEP%=K-QF4B9@vekWn^bu|Q^BvW-s3pA$<&=XR}c zjT#H3uz)AgwLWUZBH?(A(M~Uv)wVRwYM3tPORoV%G~?y@<}skKpK zvXpbK>Gg81*(+_mwy(L#y0}z_PE4<1n9F$7GRqpx4QXK1*bt5{O3)xGU1q}BQzGVU z8slzBb{P?JAXRrYZK~)9ZwPzv0H%5{8B+v`B~Td;C)z7(lxOM#)IJ~^I!x< zdN2y*9*jnX2bCD(!B~v*V7wfylA{yk=tMbsuN<9(aW1rba3Ag$a5QalVXX%-bdYar zyXMx8XoMCzO~=rCW^Y-ZZ;94PKMDleqMb1#+NKqiuIu6eDO-v`jObxZpg#OlZ!?vs zy4h2Ev!?-OPaDjhX0XqemY6+_F?-r$_B6@tX_eX2F!qp!0R_d(Q7G zE{z^gXwX@d^QxM^(?UIa)dGeE7P&RLT%pBTKIFcpR;ah&{C#SLF&5}Uo`(A>Sb7?{ z>PvFuFgfZr1IQ020`MY;V*ZAqFM~fs%KMSxdoYIt&&L3)!a%e!=nRzLQ4Gco48bmj z;64n+0nR$kAnajSU10uPW>{V2D%TiRzcP#dK!p&f6xkRf0vIa>V4Nt&crgK0q7D

W+y!CqT*thVD;d^Fl% zpFI{d?X<^dMZ+Cw?;yQkLS{1v0!+^VOwe*Vyo!FUrDtcM0ZTB0XXi{L(1;C0p2BSG zW-uH;6OLjoPNNy;F%MT599OXb*LlePhK2YWi-Z%4g%?Xi36`2P<|8lQmrrpZ7$_!z zf*YjE$4vzKm7|57K)-VIO#}v%>`ep)l}Bjz*Qu0H3T*faE2!ESULj(r(jiQU2F(yH~*;u`4n_H#?LlT zOJ1?S{+hdUHc(3*w!i^)=62a|i@2194z%&M!UkKk&9KlxcGfCw_+69s7+iRqg>5rS z>lT*DCwR5k%3OSsDY1?DvmMJ!s&#gkd*_sJ*d5BP(ASvF@X(zv*TB0Shnp+q~l!ZNHxJNS;( zB*dd0c%622)2=sY*M8b{ke8xErXEgY_mg@_o}EyjIon=shnPyRj1IA_F-?j0;(D3k z3OARzqkk5_M^oRV`;YLDeT&EEQ67!Qc)-5H8hf1e^aOc-m#O<6Q}lfvt|xi8_K@Av zJY3IE`Yb-cIVS6eOx92EBi|&y9=J<_c_ClkpkSUPcQ&hY?~Uvl-79Zo+d>8Z97^9( z^qCWKC@8Az2z950S~QZWgsL@^rJ&IoD$v*+y>P#IPrblc`HcR!$V7C%&L3 zE;BH{r2b#=H2InZ?Hd-aE9k_x%!}_#Yjfc86%`g0dGlEHnsgjjnT7&|MWtskv>UEW cmZOXwIIK&Kx`;}jIpOeB%j@b~emKzlKi8j2w*UYD diff --git a/jbmc/regression/jbmc/assume-inputs-interval/Other.class b/jbmc/regression/jbmc/assume-inputs-interval/Other.class deleted file mode 100644 index a9003bedf4233ccb1227c260b1038cb20a6e2a3a..0000000000000000000000000000000000000000 GIT binary patch literal 0 HcmV?d00001 literal 414 zcmX|7%TB{E5S&fhq)iJg<^5ETz=2%2fslBp5~!kwqFy*TiD_JgSaK62K8q6)2R?w0 zLTpUigLihuv$K|ee!so}oa4wx1^XTjJRA}l;d?IoN~SS^ZV3J?(I#IABSKweOM1`# zRA-aL^#l7~QZ1H-KA{=wB21T&cdT&2wK4M{=b2O7OO>hoicmQ|8563vI+ld?KxOi= zcnzg_5}ZNk4s;~au`sISbFrEyYDVw|!#t7Zg5NOGg^74&IpSOOY%1PF3tg-eYE~h1 zN-ao5HVKB|R7N>^aQH6(k53gfu7GP9P)EaZA5DubtXNz{+hPZ6jKqhRFm7-cFqTT~ d^b_>Kje||Dt`!Me+_(M>*v1Ys!mf4g{Q*2DO8fu- diff --git a/jbmc/regression/jbmc/assume-inputs-interval/OtherNoClinit.class b/jbmc/regression/jbmc/assume-inputs-interval/OtherNoClinit.class deleted file mode 100644 index d33240864743c5a53ff092a7eb2b7a5675642c45..0000000000000000000000000000000000000000 GIT binary patch literal 0 HcmV?d00001 literal 229 zcmY+8y9&ZU5Jm6gsZpcY3zll3jiuNKf*`R_>^I4x8`cEE#{aSsEc^gJO5EMfW@hd= zT$s=I^#-s+KZ1*Hh+c@85Q|c61(*3zF(onr?Fhk2ltQfu?qqr8{?9RFf5E6QShA=R0Az67@9MXbk3S&6>DS*&| e2j5;WWlMmO-lVBNdx9QTxAhDxG%C``LFWfd5G;cL diff --git a/jbmc/regression/jbmc/assume-inputs-interval/arg_assume.desc b/jbmc/regression/jbmc/assume-inputs-interval/arg_assume.desc index 3175712d29b..89d2682b2e6 100644 --- a/jbmc/regression/jbmc/assume-inputs-interval/arg_assume.desc +++ b/jbmc/regression/jbmc/assume-inputs-interval/arg_assume.desc @@ -1,6 +1,6 @@ CORE My ---function My.numericalArg --java-assume-inputs-interval [1:3] +--function My.numericalArg --java-assume-inputs-interval [1:3] -cp target/classes ^EXIT=10$ ^SIGNAL=0$ ^VERIFICATION FAILED$ diff --git a/jbmc/regression/jbmc/assume-inputs-interval/arg_assume_invalid2.desc b/jbmc/regression/jbmc/assume-inputs-interval/arg_assume_invalid2.desc index 6d535889918..3d93fb3ed9c 100644 --- a/jbmc/regression/jbmc/assume-inputs-interval/arg_assume_invalid2.desc +++ b/jbmc/regression/jbmc/assume-inputs-interval/arg_assume_invalid2.desc @@ -1,6 +1,6 @@ CORE My ---function My.numericalArg --java-assume-inputs-interval 2:] +--function My.numericalArg --java-assume-inputs-interval 2:] -cp target/classes ^EXIT=1$ ^SIGNAL=0$ ^Invalid User Input diff --git a/jbmc/regression/jbmc/assume-inputs-interval/arg_assume_invalid3.desc b/jbmc/regression/jbmc/assume-inputs-interval/arg_assume_invalid3.desc index 7e8b719fe8e..b106f88ed35 100644 --- a/jbmc/regression/jbmc/assume-inputs-interval/arg_assume_invalid3.desc +++ b/jbmc/regression/jbmc/assume-inputs-interval/arg_assume_invalid3.desc @@ -1,6 +1,6 @@ CORE My ---function My.numericalArg --java-assume-inputs-interval [-:1] +--function My.numericalArg --java-assume-inputs-interval [-:1] -cp target/classes ^EXIT=1$ ^SIGNAL=0$ ^Invalid User Input diff --git a/jbmc/regression/jbmc/assume-inputs-interval/arg_assume_invalid4.desc b/jbmc/regression/jbmc/assume-inputs-interval/arg_assume_invalid4.desc index 0d1f6789e55..bd24489455b 100644 --- a/jbmc/regression/jbmc/assume-inputs-interval/arg_assume_invalid4.desc +++ b/jbmc/regression/jbmc/assume-inputs-interval/arg_assume_invalid4.desc @@ -1,6 +1,6 @@ CORE My ---function My.numericalArg --java-assume-inputs-interval [3:1] +--function My.numericalArg --java-assume-inputs-interval [3:1] -cp target/classes ^EXIT=1$ ^SIGNAL=0$ ^Invalid User Input diff --git a/jbmc/regression/jbmc/assume-inputs-interval/arg_assume_invalid5.desc b/jbmc/regression/jbmc/assume-inputs-interval/arg_assume_invalid5.desc index 11bbef4ed31..0a1d71fa082 100644 --- a/jbmc/regression/jbmc/assume-inputs-interval/arg_assume_invalid5.desc +++ b/jbmc/regression/jbmc/assume-inputs-interval/arg_assume_invalid5.desc @@ -1,6 +1,6 @@ CORE My ---function My.numericalArg --java-assume-inputs-interval [1.5:3] +--function My.numericalArg --java-assume-inputs-interval [1.5:3] -cp target/classes ^EXIT=1$ ^SIGNAL=0$ ^Invalid User Input diff --git a/jbmc/regression/jbmc/assume-inputs-interval/arg_assume_neg.desc b/jbmc/regression/jbmc/assume-inputs-interval/arg_assume_neg.desc index 7528bab4114..9abcafe0abe 100644 --- a/jbmc/regression/jbmc/assume-inputs-interval/arg_assume_neg.desc +++ b/jbmc/regression/jbmc/assume-inputs-interval/arg_assume_neg.desc @@ -1,6 +1,6 @@ CORE My ---function My.numericalArg --java-assume-inputs-interval [-1:3] +--function My.numericalArg --java-assume-inputs-interval [-1:3] -cp target/classes ^EXIT=10$ ^SIGNAL=0$ ^VERIFICATION FAILED$ diff --git a/jbmc/regression/jbmc/assume-inputs-interval/arg_assume_singleton.desc b/jbmc/regression/jbmc/assume-inputs-interval/arg_assume_singleton.desc index cac3205ebdf..5ec0e07c630 100644 --- a/jbmc/regression/jbmc/assume-inputs-interval/arg_assume_singleton.desc +++ b/jbmc/regression/jbmc/assume-inputs-interval/arg_assume_singleton.desc @@ -1,6 +1,6 @@ CORE symex-driven-lazy-loading-expected-failure My ---function My.intervalUnion --java-assume-inputs-interval [3:3] --property 'java::My.intervalUnion:(I)V.assertion.1' --property 'java::My.intervalUnion:(I)V.assertion.2' --property 'java::My.intervalUnion:(I)V.assertion.3' --property 'java::My.intervalUnion:(I)V.assertion.4' --property 'java::My.intervalUnion:(I)V.assertion.6' +--function My.intervalUnion --java-assume-inputs-interval [3:3] --property 'java::My.intervalUnion:(I)V.assertion.1' --property 'java::My.intervalUnion:(I)V.assertion.2' --property 'java::My.intervalUnion:(I)V.assertion.3' --property 'java::My.intervalUnion:(I)V.assertion.4' --property 'java::My.intervalUnion:(I)V.assertion.6' -cp target/classes ^EXIT=0$ ^SIGNAL=0$ ^VERIFICATION SUCCESSFUL$ diff --git a/jbmc/regression/jbmc/assume-inputs-interval/arg_assume_union.desc b/jbmc/regression/jbmc/assume-inputs-interval/arg_assume_union.desc index a1916f7e5bb..d3057b0d697 100644 --- a/jbmc/regression/jbmc/assume-inputs-interval/arg_assume_union.desc +++ b/jbmc/regression/jbmc/assume-inputs-interval/arg_assume_union.desc @@ -1,6 +1,6 @@ CORE My ---function My.intervalUnion --java-assume-inputs-interval [-3:-2],[5:],[1:2] +--function My.intervalUnion --java-assume-inputs-interval [-3:-2],[5:],[1:2] -cp target/classes ^EXIT=10$ ^SIGNAL=0$ ^VERIFICATION FAILED$ diff --git a/jbmc/regression/jbmc/assume-inputs-interval/class_arr_assume.desc b/jbmc/regression/jbmc/assume-inputs-interval/class_arr_assume.desc index c36f416a1ba..0e2f82284c8 100644 --- a/jbmc/regression/jbmc/assume-inputs-interval/class_arr_assume.desc +++ b/jbmc/regression/jbmc/assume-inputs-interval/class_arr_assume.desc @@ -1,6 +1,6 @@ KNOWNBUG My ---function My.classArrArg --java-assume-inputs-interval [1:3] +--function My.classArrArg --java-assume-inputs-interval [1:3] -cp target/classes ^EXIT=10$ ^SIGNAL=0$ ^VERIFICATION FAILED$ diff --git a/jbmc/regression/jbmc/assume-inputs-interval/class_assume.desc b/jbmc/regression/jbmc/assume-inputs-interval/class_assume.desc index abb58e1710e..04b0347b1d6 100644 --- a/jbmc/regression/jbmc/assume-inputs-interval/class_assume.desc +++ b/jbmc/regression/jbmc/assume-inputs-interval/class_assume.desc @@ -1,6 +1,6 @@ CORE My ---function My.classArg --java-assume-inputs-interval [1:3] +--function My.classArg --java-assume-inputs-interval [1:3] -cp target/classes ^EXIT=10$ ^SIGNAL=0$ ^VERIFICATION FAILED$ diff --git a/jbmc/regression/jbmc/assume-inputs-interval/class_assume_lower.desc b/jbmc/regression/jbmc/assume-inputs-interval/class_assume_lower.desc index 0e3c694a653..92267d2bada 100644 --- a/jbmc/regression/jbmc/assume-inputs-interval/class_assume_lower.desc +++ b/jbmc/regression/jbmc/assume-inputs-interval/class_assume_lower.desc @@ -1,6 +1,6 @@ CORE My ---function My.classArg --java-assume-inputs-interval [1:] +--function My.classArg --java-assume-inputs-interval [1:] -cp target/classes ^EXIT=10$ ^SIGNAL=0$ ^VERIFICATION FAILED$ diff --git a/jbmc/regression/jbmc/assume-inputs-interval/class_assume_upper.desc b/jbmc/regression/jbmc/assume-inputs-interval/class_assume_upper.desc index 28c8c382d00..23617a1003f 100644 --- a/jbmc/regression/jbmc/assume-inputs-interval/class_assume_upper.desc +++ b/jbmc/regression/jbmc/assume-inputs-interval/class_assume_upper.desc @@ -1,6 +1,6 @@ CORE My ---function My.classArg --java-assume-inputs-interval [:3] +--function My.classArg --java-assume-inputs-interval [:3] -cp target/classes ^EXIT=10$ ^SIGNAL=0$ ^VERIFICATION FAILED$ diff --git a/jbmc/regression/jbmc/assume-inputs-interval/field_assume.desc b/jbmc/regression/jbmc/assume-inputs-interval/field_assume.desc index 103a5364b33..9664d049594 100644 --- a/jbmc/regression/jbmc/assume-inputs-interval/field_assume.desc +++ b/jbmc/regression/jbmc/assume-inputs-interval/field_assume.desc @@ -1,6 +1,6 @@ CORE My ---function My.field --java-assume-inputs-interval [1:3] +--function My.field --java-assume-inputs-interval [1:3] -cp target/classes ^EXIT=10$ ^SIGNAL=0$ ^VERIFICATION FAILED$ diff --git a/jbmc/regression/jbmc/assume-inputs-interval/field_assume_static.desc b/jbmc/regression/jbmc/assume-inputs-interval/field_assume_static.desc index 9e1bb28a314..3e1d770d7ca 100644 --- a/jbmc/regression/jbmc/assume-inputs-interval/field_assume_static.desc +++ b/jbmc/regression/jbmc/assume-inputs-interval/field_assume_static.desc @@ -1,6 +1,6 @@ CORE symex-driven-lazy-loading-expected-failure My ---function My.fieldStatic --java-assume-inputs-interval [1:3] --nondet-static +--function My.fieldStatic --java-assume-inputs-interval [1:3] --nondet-static -cp target/classes ^EXIT=10$ ^SIGNAL=0$ ^VERIFICATION FAILED$ diff --git a/jbmc/regression/jbmc/assume-inputs-interval/field_assume_static_no_clinit.desc b/jbmc/regression/jbmc/assume-inputs-interval/field_assume_static_no_clinit.desc index a214a8afed8..84d918b5b50 100644 --- a/jbmc/regression/jbmc/assume-inputs-interval/field_assume_static_no_clinit.desc +++ b/jbmc/regression/jbmc/assume-inputs-interval/field_assume_static_no_clinit.desc @@ -1,6 +1,6 @@ KNOWNBUG symex-driven-lazy-loading-expected-failure My ---function My.fieldStaticNoClinit --java-assume-inputs-interval [1:3] --nondet-static +--function My.fieldStaticNoClinit --java-assume-inputs-interval [1:3] --nondet-static -cp target/classes ^EXIT=10$ ^SIGNAL=0$ ^VERIFICATION FAILED$ diff --git a/jbmc/regression/jbmc/assume-inputs-interval/pom.xml b/jbmc/regression/jbmc/assume-inputs-interval/pom.xml new file mode 100644 index 00000000000..c1a0ffc5ab4 --- /dev/null +++ b/jbmc/regression/jbmc/assume-inputs-interval/pom.xml @@ -0,0 +1,30 @@ + + + 4.0.0 + org.cprover.regression + regression.jbmc.assume-inputs-interval + 1.0-SNAPSHOT + + + org.cprover.regression + regression.jbmc + 1.0-SNAPSHOT + + + + + + maven-jar-plugin + + + default-jar + none + + + + + + + diff --git a/jbmc/regression/jbmc/assume-inputs-interval/My.java b/jbmc/regression/jbmc/assume-inputs-interval/src/main/java/My.java similarity index 100% rename from jbmc/regression/jbmc/assume-inputs-interval/My.java rename to jbmc/regression/jbmc/assume-inputs-interval/src/main/java/My.java diff --git a/jbmc/regression/jbmc/assume-inputs-interval/Other.java b/jbmc/regression/jbmc/assume-inputs-interval/src/main/java/Other.java similarity index 100% rename from jbmc/regression/jbmc/assume-inputs-interval/Other.java rename to jbmc/regression/jbmc/assume-inputs-interval/src/main/java/Other.java diff --git a/jbmc/regression/jbmc/assume-inputs-interval/OtherNoClinit.java b/jbmc/regression/jbmc/assume-inputs-interval/src/main/java/OtherNoClinit.java similarity index 100% rename from jbmc/regression/jbmc/assume-inputs-interval/OtherNoClinit.java rename to jbmc/regression/jbmc/assume-inputs-interval/src/main/java/OtherNoClinit.java diff --git a/jbmc/regression/jbmc/pom.xml b/jbmc/regression/jbmc/pom.xml index 1bef6c82283..b39e815f0cd 100644 --- a/jbmc/regression/jbmc/pom.xml +++ b/jbmc/regression/jbmc/pom.xml @@ -53,6 +53,7 @@ assume2 assume3 assume-inputs-integral + assume-inputs-interval classpath-jar-load-whole-jar From 54c440276d0769272b3dd7168c3dbeb178c24353 Mon Sep 17 00:00:00 2001 From: Peter Schrammel Date: Thu, 2 Jan 2025 20:58:46 +0100 Subject: [PATCH 40/47] Compile jbmc/assume-inputs-non-null test sources Add pom.xml for compilation, move sources, remove obsolete pre-compiled class files. --- .../jbmc/assume-inputs-non-null/My.class | Bin 1110 -> 0 bytes .../jbmc/assume-inputs-non-null/Other.class | Bin 291 -> 0 bytes .../jbmc/assume-inputs-non-null/Other2.class | Bin 230 -> 0 bytes .../assume-inputs-non-null/class_assume.desc | 2 +- .../assume-inputs-non-null/field_assume.desc | 2 +- .../jbmc/assume-inputs-non-null/pom.xml | 30 ++++++++++++++++++ .../{ => src/main/java}/My.java | 0 .../{ => src/main/java}/Other.java | 0 .../{ => src/main/java}/Other2.java | 0 .../string_array_assume.desc | 2 +- .../string_array_no_assume.desc | 2 +- .../assume-inputs-non-null/string_assume.desc | 2 +- jbmc/regression/jbmc/pom.xml | 1 + 13 files changed, 36 insertions(+), 5 deletions(-) delete mode 100644 jbmc/regression/jbmc/assume-inputs-non-null/My.class delete mode 100644 jbmc/regression/jbmc/assume-inputs-non-null/Other.class delete mode 100644 jbmc/regression/jbmc/assume-inputs-non-null/Other2.class create mode 100644 jbmc/regression/jbmc/assume-inputs-non-null/pom.xml rename jbmc/regression/jbmc/assume-inputs-non-null/{ => src/main/java}/My.java (100%) rename jbmc/regression/jbmc/assume-inputs-non-null/{ => src/main/java}/Other.java (100%) rename jbmc/regression/jbmc/assume-inputs-non-null/{ => src/main/java}/Other2.java (100%) diff --git a/jbmc/regression/jbmc/assume-inputs-non-null/My.class b/jbmc/regression/jbmc/assume-inputs-non-null/My.class deleted file mode 100644 index ee262398832ad036eb521d18c78e86976c830ea4..0000000000000000000000000000000000000000 GIT binary patch literal 0 HcmV?d00001 literal 1110 zcmbtS-*3`T6#i~06iWHk!35nL+t^^Jpg5mKj0D|-0g1zyIG+ks>_jlPoeBSl5Bmpv z_D5WziN0y#A7wnZv@qjdjA?p%&$;J(_xsM*pT9nT1+a^oDx$a?K?G|G@+tx%SjUD~ zHpNm9XIl!kRTNQDu)`31W|^Y_gWftaUK`bsF&WfSW=kjc#Dt7B>fTnlv%zm=4H; zL*&WYDE$T!y+jj8W`#hCLiCbekjb=Lr7xpzuzU*kjy7a7tsytb2qcXR?L}#az(nbK z`3F+(A)O%i1%W50kiWT6)Q<#=(Vao}+*5To!v4tRscyGcH6(OUFpkclBocl$=~y50dP hJ@N_a2^9G)lKTiMSCLiBrRYxVLOrsWz$dy__TtK7bD;rbFT|`{w=L zWOn!Uemnt;(6o_9%|hKmgW#OgL`VC%R^g7&@Q(h~AB29iAFL!86YMxWsN^?cdCSZ( zb_5T9y!hoq4$O&;bUG#EJKYVTFpGDJ;Cebzi_0lc$=VM>CiW`6BwIDtVq|SUyS@w? z4#5yYsQsU`4327>qKzDX0a67R+yN#m(IQH$#KlWk%iOhCGh+1apqs=MK23pHRArZg F`vKSBIc@*| diff --git a/jbmc/regression/jbmc/assume-inputs-non-null/Other2.class b/jbmc/regression/jbmc/assume-inputs-non-null/Other2.class deleted file mode 100644 index 29d7b35b2b807cb8d24fa67b7277c40f41c339f4..0000000000000000000000000000000000000000 GIT binary patch literal 0 HcmV?d00001 literal 230 zcmYL@I}3tf6o%hpUP|pkd(c=73DQ=y1Wi&y(XRPnpO}Ja|Enoz=m+$pqN4>3=kmS} z=kj_#o&aX(nrOf_&^FK^*q0)gY2>b@NJ2v2i~XzbBz_t>yPC`i`a-6%SP~ke@qwVO zvQQAZo=nB2JO?7*`$58vxy#D@DAuwP*0wl_+?`hYZ0Im}&(|XK{ztY!ERF?+Q1~l= gI8 + + 4.0.0 + org.cprover.regression + regression.jbmc.assume-inputs-non-null + 1.0-SNAPSHOT + + + org.cprover.regression + regression.jbmc + 1.0-SNAPSHOT + + + + + + maven-jar-plugin + + + default-jar + none + + + + + + + diff --git a/jbmc/regression/jbmc/assume-inputs-non-null/My.java b/jbmc/regression/jbmc/assume-inputs-non-null/src/main/java/My.java similarity index 100% rename from jbmc/regression/jbmc/assume-inputs-non-null/My.java rename to jbmc/regression/jbmc/assume-inputs-non-null/src/main/java/My.java diff --git a/jbmc/regression/jbmc/assume-inputs-non-null/Other.java b/jbmc/regression/jbmc/assume-inputs-non-null/src/main/java/Other.java similarity index 100% rename from jbmc/regression/jbmc/assume-inputs-non-null/Other.java rename to jbmc/regression/jbmc/assume-inputs-non-null/src/main/java/Other.java diff --git a/jbmc/regression/jbmc/assume-inputs-non-null/Other2.java b/jbmc/regression/jbmc/assume-inputs-non-null/src/main/java/Other2.java similarity index 100% rename from jbmc/regression/jbmc/assume-inputs-non-null/Other2.java rename to jbmc/regression/jbmc/assume-inputs-non-null/src/main/java/Other2.java diff --git a/jbmc/regression/jbmc/assume-inputs-non-null/string_array_assume.desc b/jbmc/regression/jbmc/assume-inputs-non-null/string_array_assume.desc index a8bae456601..4e3651ee069 100644 --- a/jbmc/regression/jbmc/assume-inputs-non-null/string_array_assume.desc +++ b/jbmc/regression/jbmc/assume-inputs-non-null/string_array_assume.desc @@ -1,6 +1,6 @@ CORE My ---function My.stringArrayArg --java-assume-inputs-non-null +--function My.stringArrayArg --java-assume-inputs-non-null -cp target/classes ^EXIT=10$ ^SIGNAL=0$ ^VERIFICATION FAILED$ diff --git a/jbmc/regression/jbmc/assume-inputs-non-null/string_array_no_assume.desc b/jbmc/regression/jbmc/assume-inputs-non-null/string_array_no_assume.desc index dbad249bce4..5737a812498 100644 --- a/jbmc/regression/jbmc/assume-inputs-non-null/string_array_no_assume.desc +++ b/jbmc/regression/jbmc/assume-inputs-non-null/string_array_no_assume.desc @@ -1,6 +1,6 @@ CORE My ---function My.stringArrayArg +--function My.stringArrayArg -cp target/classes ^EXIT=10$ ^SIGNAL=0$ ^VERIFICATION FAILED$ diff --git a/jbmc/regression/jbmc/assume-inputs-non-null/string_assume.desc b/jbmc/regression/jbmc/assume-inputs-non-null/string_assume.desc index bdfb938fb45..fc37e0b71e5 100644 --- a/jbmc/regression/jbmc/assume-inputs-non-null/string_assume.desc +++ b/jbmc/regression/jbmc/assume-inputs-non-null/string_assume.desc @@ -1,6 +1,6 @@ CORE My ---function My.stringArg --java-assume-inputs-non-null --max-nondet-string-length 10 +--function My.stringArg --java-assume-inputs-non-null --max-nondet-string-length 10 -cp target/classes ^EXIT=10$ ^SIGNAL=0$ ^VERIFICATION FAILED$ diff --git a/jbmc/regression/jbmc/pom.xml b/jbmc/regression/jbmc/pom.xml index b39e815f0cd..345c060840b 100644 --- a/jbmc/regression/jbmc/pom.xml +++ b/jbmc/regression/jbmc/pom.xml @@ -54,6 +54,7 @@ assume3 assume-inputs-integral assume-inputs-interval + assume-inputs-non-null classpath-jar-load-whole-jar From f69d05f782f5f176f490e665775082ecbbd66894 Mon Sep 17 00:00:00 2001 From: Peter Schrammel Date: Thu, 2 Jan 2025 21:09:53 +0100 Subject: [PATCH 41/47] Compile jbmc/astore_aload1 test sources Add pom.xml for compilation, move sources, remove obsolete pre-compiled class files. --- .../jbmc/astore_aload1/astore_aload1.class | Bin 3060 -> 0 bytes jbmc/regression/jbmc/astore_aload1/pom.xml | 30 ++++++++++++++++++ .../{ => src/main/java}/astore_aload1.java | 0 jbmc/regression/jbmc/astore_aload1/test.desc | 2 +- jbmc/regression/jbmc/pom.xml | 1 + 5 files changed, 32 insertions(+), 1 deletion(-) delete mode 100644 jbmc/regression/jbmc/astore_aload1/astore_aload1.class create mode 100644 jbmc/regression/jbmc/astore_aload1/pom.xml rename jbmc/regression/jbmc/astore_aload1/{ => src/main/java}/astore_aload1.java (100%) diff --git a/jbmc/regression/jbmc/astore_aload1/astore_aload1.class b/jbmc/regression/jbmc/astore_aload1/astore_aload1.class deleted file mode 100644 index 730c243fb527ad5263e72eeb6baf65a863e1cbc9..0000000000000000000000000000000000000000 GIT binary patch literal 0 HcmV?d00001 literal 3060 zcmZuzTWnNS6kX@u^SE=T$nCt^>!7^Kt8}IeGgHb?o&^->i?$$86sPR~1EnQ1gCr6^ zOcWDMngGVc{zyy=(GL?fg3%HFi9bsGHu1wm{Pjm-#C;m4V9!0xoU>=GefBwP-#y*; z{y*Q|1(3ro7cEGI5Jy^}(}j(cAVLqTVb~3WHw@7*WW!Jm!)X{Hg-tFp*sPFch_)50 z)l#Kao|&%hEmw=94;c7j3nl&8zJ9SrvR4M!Px@62S0VQF7^x-@X4Ew3{KC))PIM%BQuvO6Q%uSeMF>Kt<6+Qr;1ZE#mP)sAJc?qk!(UMe1_I1=k9KZ z*;lE|ROs;k?Nr#_gdNz);62$gIDW1)QKL)*+@HZ3qf}U9d-T++rx86J(9=OZ?bXwM z%FC00y;GD@O2}lXTCS8P7p_Eks9hq0@_7O)=*hOw!(?8o7D1LxAJPPdWn?`^E2CAk z-vRrA3`P(j=Rt-Lp2u>s$u(33M-!k1J+~)W=l#jLGmxx{0#DXM1(B?~1(~de3o2Px z1t(dTg^=Cl#@*z{7`D5@aaUZNgXCS|j<_2SkEUpLuZ{X#uh)c9q@beU~`9^oii|={m{TffS(NT zQvrUC;TP%fq~S=Q3i5Phj4Q@6%L`C#EPK)AHirf|vA0m7w72MCuk9Uxq)bbxT_ zqyvOYPo{%}OHZYPgiFs!2ML#6C><2tM0{@N7H1>sbDj$*1TJy` zg}`Mlpb)sq1r!2zash?FJ(&wC1n#L^P$6*7$psYx_d>bgLU0V>QQxsMvx}9-e1~Ud z4e11n%&eiEV40aU#1pJCvxa(toy@EuKjAwbMKSejg5sD7&;&&?GoXnO5l{d3(@odX zO_yEAr0&Gjp(Pakh2g-X795959XpKW)PCEr1RJmvn~BMz89j(#Ct}z~UVTVll)C*% z>hu%T>(A4!Ds}oR^{=$7j&{evB?S}W39qwYb&zW5OUUOk2R^{R!65$;L;N8Q3yxv&JVrz}M#V6Wh_g5<-oQ)Z29AkOaa`QP z3Gp+=#2+{*ZM-a#ctvJ$N*=oWgR8?0H@_coKZH;s%0pvJkF^B z%HRrmBCliUF**=dSjiMtDXdm#Q&^+0R$-mOdPNBX{zioTh262}{D|ohou3ml;<30M zEi|4s6Ny$DK8>f*xZW|(PzAIvysPErU&?^yNc=Vub5Q&ixcwEZg%VnLZ`0Qnu$p%1 Lx4Vt>#X`rwtr%_b diff --git a/jbmc/regression/jbmc/astore_aload1/pom.xml b/jbmc/regression/jbmc/astore_aload1/pom.xml new file mode 100644 index 00000000000..dc7ebf16d41 --- /dev/null +++ b/jbmc/regression/jbmc/astore_aload1/pom.xml @@ -0,0 +1,30 @@ + + + 4.0.0 + org.cprover.regression + regression.jbmc.astore_aload1 + 1.0-SNAPSHOT + + + org.cprover.regression + regression.jbmc + 1.0-SNAPSHOT + + + + + + maven-jar-plugin + + + default-jar + none + + + + + + + diff --git a/jbmc/regression/jbmc/astore_aload1/astore_aload1.java b/jbmc/regression/jbmc/astore_aload1/src/main/java/astore_aload1.java similarity index 100% rename from jbmc/regression/jbmc/astore_aload1/astore_aload1.java rename to jbmc/regression/jbmc/astore_aload1/src/main/java/astore_aload1.java diff --git a/jbmc/regression/jbmc/astore_aload1/test.desc b/jbmc/regression/jbmc/astore_aload1/test.desc index c12fa6d0767..7b9d0fc934e 100644 --- a/jbmc/regression/jbmc/astore_aload1/test.desc +++ b/jbmc/regression/jbmc/astore_aload1/test.desc @@ -1,6 +1,6 @@ CORE astore_aload1 - +-cp target/classes ^EXIT=0$ ^SIGNAL=0$ ^VERIFICATION SUCCESSFUL$ diff --git a/jbmc/regression/jbmc/pom.xml b/jbmc/regression/jbmc/pom.xml index 345c060840b..b747f462b23 100644 --- a/jbmc/regression/jbmc/pom.xml +++ b/jbmc/regression/jbmc/pom.xml @@ -55,6 +55,7 @@ assume-inputs-integral assume-inputs-interval assume-inputs-non-null + astore_aload1 classpath-jar-load-whole-jar From 5672a051dba4ffc0e10791cbc8fd8f6334e19db7 Mon Sep 17 00:00:00 2001 From: Peter Schrammel Date: Thu, 2 Jan 2025 21:10:18 +0100 Subject: [PATCH 42/47] Compile jbmc/athrow1 test sources Add pom.xml for compilation, move sources, remove obsolete pre-compiled class files. --- jbmc/regression/jbmc/athrow1/A.class | Bin 185 -> 0 bytes jbmc/regression/jbmc/athrow1/athrow1.class | Bin 635 -> 0 bytes jbmc/regression/jbmc/athrow1/pom.xml | 30 ++++++++++++++++++ .../athrow1/{ => src/main/java}/athrow1.java | 0 jbmc/regression/jbmc/athrow1/test.desc | 2 +- jbmc/regression/jbmc/pom.xml | 1 + 6 files changed, 32 insertions(+), 1 deletion(-) delete mode 100644 jbmc/regression/jbmc/athrow1/A.class delete mode 100644 jbmc/regression/jbmc/athrow1/athrow1.class create mode 100644 jbmc/regression/jbmc/athrow1/pom.xml rename jbmc/regression/jbmc/athrow1/{ => src/main/java}/athrow1.java (100%) diff --git a/jbmc/regression/jbmc/athrow1/A.class b/jbmc/regression/jbmc/athrow1/A.class deleted file mode 100644 index a5f1be16970b092e25b185e5ee4e4a3becce1956..0000000000000000000000000000000000000000 GIT binary patch literal 0 HcmV?d00001 literal 185 zcmX^0Z`VEs1_l!bUM>b^1}=66ZgvJ9Mg}&U%)HDJJ4Oa(4b3n{1{UZ1lvG9rexJ;| zRKL>Pq|~C2#H1Xc2v=}^X;E^jTPBFZlUR~blwWSBmz7wS$iu+Gz{<$L=*Y+*4C3qO zB<7{-yH+Hp7L;V>=P@WSFaa$D0Y)GOss++)K$a|!28pn0ZD(NI2$p6Cl5Ai>kQ4`y I$Hc%10Eh=5bN~PV diff --git a/jbmc/regression/jbmc/athrow1/athrow1.class b/jbmc/regression/jbmc/athrow1/athrow1.class deleted file mode 100644 index 9a5e577142b593fedbda515ef286c35c0e14fcda..0000000000000000000000000000000000000000 GIT binary patch literal 0 HcmV?d00001 literal 635 zcmZvZT~8B16o%i~c028M%U87)ly6kjL}J37#7GdX3S5+sP_Cxi2@aNBGP_lO3xB|C zB!NT{x%Wqb@05?;aIrII&w1ya=bZU>{pT-$WxNg$U_#<~0MG3&N+@DdVk$tv{Z9v& z!K}obKy^W-skWI(;`ED2RlBP@0-_~QSTV85J_+O&-|PzH*OHDF7;czYZ}pDa+U__p z3rEVt0=32c#-aMImbxlFSZZe0#0MYU!Adhz(YH-?+}BIYlZ!|K#g(XgcSX=ldN$G< z#uJE!hjvx6!FGiEx z1$Y1L1;i->vT!ZjCQ-sD#uz(k#D{Z-CobXbT_D$ZceVK&{t3#LC@>+fPN{U)1;|tD zd}{Eyx~DEPTj4s4ae7vnt-`xu(vx^1@f1R$HbmjG2e#!t1TZ>QJV)sSGXD$t+!=hw UdFy}A>HK_n;b+%Py + + 4.0.0 + org.cprover.regression + regression.jbmc.athrow1 + 1.0-SNAPSHOT + + + org.cprover.regression + regression.jbmc + 1.0-SNAPSHOT + + + + + + maven-jar-plugin + + + default-jar + none + + + + + + + diff --git a/jbmc/regression/jbmc/athrow1/athrow1.java b/jbmc/regression/jbmc/athrow1/src/main/java/athrow1.java similarity index 100% rename from jbmc/regression/jbmc/athrow1/athrow1.java rename to jbmc/regression/jbmc/athrow1/src/main/java/athrow1.java diff --git a/jbmc/regression/jbmc/athrow1/test.desc b/jbmc/regression/jbmc/athrow1/test.desc index d5e77f68299..d70f94bc7e5 100644 --- a/jbmc/regression/jbmc/athrow1/test.desc +++ b/jbmc/regression/jbmc/athrow1/test.desc @@ -1,6 +1,6 @@ CORE athrow1 - +-cp target/classes ^EXIT=10$ ^SIGNAL=0$ ^VERIFICATION FAILED$ diff --git a/jbmc/regression/jbmc/pom.xml b/jbmc/regression/jbmc/pom.xml index b747f462b23..74d283d3d30 100644 --- a/jbmc/regression/jbmc/pom.xml +++ b/jbmc/regression/jbmc/pom.xml @@ -56,6 +56,7 @@ assume-inputs-interval assume-inputs-non-null astore_aload1 + athrow1 classpath-jar-load-whole-jar From 173b5b764dcf362593c3cddb118349c2fa1531a6 Mon Sep 17 00:00:00 2001 From: Peter Schrammel Date: Thu, 2 Jan 2025 21:10:49 +0100 Subject: [PATCH 43/47] Compile jbmc/basic1 test sources Add pom.xml for compilation, move sources, remove obsolete pre-compiled class files. --- jbmc/regression/jbmc/basic1/helloworld.class | Bin 923 -> 0 bytes jbmc/regression/jbmc/basic1/pom.xml | 30 ++++++++++++++++++ .../{ => src/main/java}/helloworld.java | 0 jbmc/regression/jbmc/basic1/test.desc | 2 +- jbmc/regression/jbmc/pom.xml | 1 + 5 files changed, 32 insertions(+), 1 deletion(-) delete mode 100644 jbmc/regression/jbmc/basic1/helloworld.class create mode 100644 jbmc/regression/jbmc/basic1/pom.xml rename jbmc/regression/jbmc/basic1/{ => src/main/java}/helloworld.java (100%) diff --git a/jbmc/regression/jbmc/basic1/helloworld.class b/jbmc/regression/jbmc/basic1/helloworld.class deleted file mode 100644 index 244d721feaa31d660036d64436fb91cb44071b28..0000000000000000000000000000000000000000 GIT binary patch literal 0 HcmV?d00001 literal 923 zcmZuvT~8B16g{*3nB8ScOQl$C(SoQ2m7=1eG)99Mn^ZBW0mY|nJHf^6ZnL}f)Q+3f7yd+(ex=iK@8_xn!(t0I<30&U#Vs)v@F|Ym?^%k?pq(Ml4H4hrCR9Q?%ulEn5czTuK6<{>Tvk{DQ%DOWk>a=^u#6Hzc0}@caPm#x z_k0HNOl>dhsQq&sD*`uhOW-z2f{ePuaaZ6T)<|>@!}dy*t<6sj*;eWq%n>`seSrs9 zXGo3cw(9$`5ssy5pMy}g$Re*pg-qW7!hK2VL-IgcEy5Vmok%nAwrX;SI8!{`xrp>h zm8RSsL08;%=M?A@X$FJ5vz`8UXnGZLb|hoNp^4MHnli9`*&LckV+uP|pbfhy(0!Vu z`^8dOWj{p`dTAOUITX#(m(e%2bPRS#0mC${@qQ8pGMJ%QwSIv{5Aga3+5x7H5c!RX zABes=M(h{;rQ==jK}{d4>0>oxtY&m!mcJreJtUqgYS_jE@u*YGL#LHftRqinS%HZ) zs#cMpz9e=?&{^s*5u48CDjZo*=eeP{)t(BHn-*Op4#1 + + 4.0.0 + org.cprover.regression + regression.jbmc.basic1 + 1.0-SNAPSHOT + + + org.cprover.regression + regression.jbmc + 1.0-SNAPSHOT + + + + + + maven-jar-plugin + + + default-jar + none + + + + + + + diff --git a/jbmc/regression/jbmc/basic1/helloworld.java b/jbmc/regression/jbmc/basic1/src/main/java/helloworld.java similarity index 100% rename from jbmc/regression/jbmc/basic1/helloworld.java rename to jbmc/regression/jbmc/basic1/src/main/java/helloworld.java diff --git a/jbmc/regression/jbmc/basic1/test.desc b/jbmc/regression/jbmc/basic1/test.desc index 4c355e7c702..0a54dedeb3c 100644 --- a/jbmc/regression/jbmc/basic1/test.desc +++ b/jbmc/regression/jbmc/basic1/test.desc @@ -1,6 +1,6 @@ CORE helloworld - +-cp target/classes ^EXIT=0$ ^SIGNAL=0$ ^VERIFICATION SUCCESSFUL$ diff --git a/jbmc/regression/jbmc/pom.xml b/jbmc/regression/jbmc/pom.xml index 74d283d3d30..637fc885263 100644 --- a/jbmc/regression/jbmc/pom.xml +++ b/jbmc/regression/jbmc/pom.xml @@ -57,6 +57,7 @@ assume-inputs-non-null astore_aload1 athrow1 + basic1 classpath-jar-load-whole-jar From fb1bed2cca9d1ce3ffb27ada6d7a6676db9771c7 Mon Sep 17 00:00:00 2001 From: Peter Schrammel Date: Thu, 2 Jan 2025 21:11:11 +0100 Subject: [PATCH 44/47] Compile jbmc/basic2 test sources Add pom.xml for compilation, move sources, remove obsolete pre-compiled class files. --- jbmc/regression/jbmc/basic2/basic.class | Bin 434 -> 0 bytes jbmc/regression/jbmc/basic2/basic2.class | Bin 253 -> 0 bytes jbmc/regression/jbmc/basic2/pom.xml | 30 ++++++++++++++++++ .../basic2/{ => src/main/java}/basic.java | 0 jbmc/regression/jbmc/basic2/test.desc | 2 +- jbmc/regression/jbmc/pom.xml | 1 + 6 files changed, 32 insertions(+), 1 deletion(-) delete mode 100644 jbmc/regression/jbmc/basic2/basic.class delete mode 100644 jbmc/regression/jbmc/basic2/basic2.class create mode 100644 jbmc/regression/jbmc/basic2/pom.xml rename jbmc/regression/jbmc/basic2/{ => src/main/java}/basic.java (100%) diff --git a/jbmc/regression/jbmc/basic2/basic.class b/jbmc/regression/jbmc/basic2/basic.class deleted file mode 100644 index cfaa6ef986ec86ba7eb144cf05022a8a504c1dc0..0000000000000000000000000000000000000000 GIT binary patch literal 0 HcmV?d00001 literal 434 zcmZWkO-sW-5Pj36joqd;jhb3Nz++Uf&}+quAQXxoDuQ?@NxQaNngr6+OMjIYD+->) zA0^HPr3YDNcjnE!_jbO%-#!4eaUft}TcCs;3!Z?X3j+-cyB3-RF;5~ncvNyWB2br5 zI#;pEE(nHyd`B=ZlaVCUdMcLJizt-oZ4k~FF{41m1kZoyO@pVPH4EZ#tDmJR9(Odc zk_$&NnD z2L(Pr!&%np^A&}6822lfy;EoTg5sL&!sM|E`{@;`@K~g*m-!WHa#sue^K*H?&6`_4 DV^BsT diff --git a/jbmc/regression/jbmc/basic2/basic2.class b/jbmc/regression/jbmc/basic2/basic2.class deleted file mode 100644 index c75dafa2beee4ca1ad36d93b22a21e8026d9e0af..0000000000000000000000000000000000000000 GIT binary patch literal 0 HcmV?d00001 literal 253 zcmYk0OA5j;5QhJ;)@rPe3kY4R3kBEWMi2zih2mDyHfW>|sMQmAAyTxIT?(hkEa3FYm*DN#-bu>5|HQ=(tcltAhWiBr_Gr~H}ANtuR@c;k- diff --git a/jbmc/regression/jbmc/basic2/pom.xml b/jbmc/regression/jbmc/basic2/pom.xml new file mode 100644 index 00000000000..8a7197539ed --- /dev/null +++ b/jbmc/regression/jbmc/basic2/pom.xml @@ -0,0 +1,30 @@ + + + 4.0.0 + org.cprover.regression + regression.jbmc.basic2 + 1.0-SNAPSHOT + + + org.cprover.regression + regression.jbmc + 1.0-SNAPSHOT + + + + + + maven-jar-plugin + + + default-jar + none + + + + + + + diff --git a/jbmc/regression/jbmc/basic2/basic.java b/jbmc/regression/jbmc/basic2/src/main/java/basic.java similarity index 100% rename from jbmc/regression/jbmc/basic2/basic.java rename to jbmc/regression/jbmc/basic2/src/main/java/basic.java diff --git a/jbmc/regression/jbmc/basic2/test.desc b/jbmc/regression/jbmc/basic2/test.desc index 260f047024f..fe3693b2412 100644 --- a/jbmc/regression/jbmc/basic2/test.desc +++ b/jbmc/regression/jbmc/basic2/test.desc @@ -1,6 +1,6 @@ CORE basic - +-cp target/classes ^EXIT=0$ ^SIGNAL=0$ ^VERIFICATION SUCCESSFUL$ diff --git a/jbmc/regression/jbmc/pom.xml b/jbmc/regression/jbmc/pom.xml index 637fc885263..d9003913a0b 100644 --- a/jbmc/regression/jbmc/pom.xml +++ b/jbmc/regression/jbmc/pom.xml @@ -58,6 +58,7 @@ astore_aload1 athrow1 basic1 + basic2 classpath-jar-load-whole-jar From f73c738ad15c7b3d65e046b67f76c9257dd3151f Mon Sep 17 00:00:00 2001 From: Peter Schrammel Date: Thu, 2 Jan 2025 21:11:42 +0100 Subject: [PATCH 45/47] Compile jbmc/bitwise1 test sources Add pom.xml for compilation, move sources, remove obsolete pre-compiled class files. --- jbmc/regression/jbmc/bitwise1/bitwise1.class | Bin 574 -> 0 bytes jbmc/regression/jbmc/bitwise1/pom.xml | 30 ++++++++++++++++++ .../{ => src/main/java}/bitwise1.java | 0 jbmc/regression/jbmc/bitwise1/test.desc | 2 +- jbmc/regression/jbmc/pom.xml | 1 + 5 files changed, 32 insertions(+), 1 deletion(-) delete mode 100644 jbmc/regression/jbmc/bitwise1/bitwise1.class create mode 100644 jbmc/regression/jbmc/bitwise1/pom.xml rename jbmc/regression/jbmc/bitwise1/{ => src/main/java}/bitwise1.java (100%) diff --git a/jbmc/regression/jbmc/bitwise1/bitwise1.class b/jbmc/regression/jbmc/bitwise1/bitwise1.class deleted file mode 100644 index ae41460ca8a68ba6925403bcd6d36754622bc089..0000000000000000000000000000000000000000 GIT binary patch literal 0 HcmV?d00001 literal 574 zcmYL`OHaZ;5Xb-9mbTQQJbd5-6ypIsNKCj%j0W}O1ynO&DW8H#@g*bF%rCBtvWI@A%fn^IT$Qj5pFqgh6 zLuSJX0`7;R>jj4*a2jpiq)eSbuLw_sdkkuE^O8ZUcAK1G=0te>tk-F9|3Vg1qT>jU zVZL~M(sJ&dQrq!vO101z-p#ITOw>Zhy*+jA{_4$&+x{b4wQkRM`LU3kL_>rRBH%mQ z5@REQX&Z4^Hl|=RWGC>0vEn1&@A?epxYNL@jWrY)l9TH5MvJ>4DW8O@ZCaWnH+dj@ z-u&m0(y&Jf+PIDay`4!9s*oiaKr$IgK#4t822lG*F6&R2dWUv3LhMsAl!%e0-zG^K3=&|{s5mlFgnc7N oi(~d*Mmd@Xq|*8;j6MwQ8JaqTI>C)4Nkj~ay)T8&MbqYg0h=LakpKVy diff --git a/jbmc/regression/jbmc/bitwise1/pom.xml b/jbmc/regression/jbmc/bitwise1/pom.xml new file mode 100644 index 00000000000..94147b570b0 --- /dev/null +++ b/jbmc/regression/jbmc/bitwise1/pom.xml @@ -0,0 +1,30 @@ + + + 4.0.0 + org.cprover.regression + regression.jbmc.bitwise1 + 1.0-SNAPSHOT + + + org.cprover.regression + regression.jbmc + 1.0-SNAPSHOT + + + + + + maven-jar-plugin + + + default-jar + none + + + + + + + diff --git a/jbmc/regression/jbmc/bitwise1/bitwise1.java b/jbmc/regression/jbmc/bitwise1/src/main/java/bitwise1.java similarity index 100% rename from jbmc/regression/jbmc/bitwise1/bitwise1.java rename to jbmc/regression/jbmc/bitwise1/src/main/java/bitwise1.java diff --git a/jbmc/regression/jbmc/bitwise1/test.desc b/jbmc/regression/jbmc/bitwise1/test.desc index c72bb47d6d5..0271dbaab5c 100644 --- a/jbmc/regression/jbmc/bitwise1/test.desc +++ b/jbmc/regression/jbmc/bitwise1/test.desc @@ -1,6 +1,6 @@ CORE bitwise1 - +-cp target/classes ^EXIT=0$ ^SIGNAL=0$ ^VERIFICATION SUCCESSFUL$ diff --git a/jbmc/regression/jbmc/pom.xml b/jbmc/regression/jbmc/pom.xml index d9003913a0b..624d3f3538a 100644 --- a/jbmc/regression/jbmc/pom.xml +++ b/jbmc/regression/jbmc/pom.xml @@ -59,6 +59,7 @@ athrow1 basic1 basic2 + bitwise1 classpath-jar-load-whole-jar From 7ea59f05a66916edab975806e7feb46bde977316 Mon Sep 17 00:00:00 2001 From: Peter Schrammel Date: Thu, 2 Jan 2025 21:11:59 +0100 Subject: [PATCH 46/47] Compile jbmc/boolean1 test sources Add pom.xml for compilation, move sources, remove obsolete pre-compiled class files. --- jbmc/regression/jbmc/boolean1/boolean1.class | Bin 525 -> 0 bytes jbmc/regression/jbmc/boolean1/pom.xml | 30 ++++++++++++++++++ .../{ => src/main/java}/boolean1.java | 0 jbmc/regression/jbmc/boolean1/test.desc | 2 +- jbmc/regression/jbmc/pom.xml | 1 + 5 files changed, 32 insertions(+), 1 deletion(-) delete mode 100644 jbmc/regression/jbmc/boolean1/boolean1.class create mode 100644 jbmc/regression/jbmc/boolean1/pom.xml rename jbmc/regression/jbmc/boolean1/{ => src/main/java}/boolean1.java (100%) diff --git a/jbmc/regression/jbmc/boolean1/boolean1.class b/jbmc/regression/jbmc/boolean1/boolean1.class deleted file mode 100644 index 0683803836873f83c30491e1dc528c6d41f08cbf..0000000000000000000000000000000000000000 GIT binary patch literal 0 HcmV?d00001 literal 525 zcmYL_OH0F05QWdpvrSX`w6@WT3m4UeMd-4KQWXRri;7@(d0ZqlCX%H7n6BKpu7U*x z-TR}&N$g{B?+i0@&V2X&{C<1^=wMTWifR@zR#ntAh^VSq(@;l4g~3qSHlv7#u^af& zu^X9|#~lVXU{JcQ@5ToVVr%DyLFxq#XDFPzKEE72SUkK=hNskJb-Hq0LX-M3uLKz~iRBzc)0WOdT3>Ix@&I)RRKnGyS{v(H!k041nLvcBMWevGaB!y+E=h5pJY7URwkUI-Mf{aJhpr;M6MW3V6XR%^EA)rj8 zLqK5ADQi+>6y@D1*n|?Ir&~#jj07tvP@asQK}f5HAw5Hy7-PC#A&imxgm^oJ^quI1 zR9}Xax+t_fM=lLoS)_^#QIYaQQd$snQd6K*mfxX_p-L~1#5V{_w>izfgP + + 4.0.0 + org.cprover.regression + regression.jbmc.boolean1 + 1.0-SNAPSHOT + + + org.cprover.regression + regression.jbmc + 1.0-SNAPSHOT + + + + + + maven-jar-plugin + + + default-jar + none + + + + + + + diff --git a/jbmc/regression/jbmc/boolean1/boolean1.java b/jbmc/regression/jbmc/boolean1/src/main/java/boolean1.java similarity index 100% rename from jbmc/regression/jbmc/boolean1/boolean1.java rename to jbmc/regression/jbmc/boolean1/src/main/java/boolean1.java diff --git a/jbmc/regression/jbmc/boolean1/test.desc b/jbmc/regression/jbmc/boolean1/test.desc index 808347e008b..bc15c092cef 100644 --- a/jbmc/regression/jbmc/boolean1/test.desc +++ b/jbmc/regression/jbmc/boolean1/test.desc @@ -1,6 +1,6 @@ CORE boolean1 ---function boolean1.doit +--function boolean1.doit -cp target/classes ^EXIT=0$ ^SIGNAL=0$ ^VERIFICATION SUCCESSFUL$ diff --git a/jbmc/regression/jbmc/pom.xml b/jbmc/regression/jbmc/pom.xml index 624d3f3538a..fe5e5e52906 100644 --- a/jbmc/regression/jbmc/pom.xml +++ b/jbmc/regression/jbmc/pom.xml @@ -60,6 +60,7 @@ basic1 basic2 bitwise1 + boolean1 classpath-jar-load-whole-jar From 7e4897cd042ec81e949ca94dcdbeaaab10aff36d Mon Sep 17 00:00:00 2001 From: Peter Schrammel Date: Thu, 2 Jan 2025 21:12:40 +0100 Subject: [PATCH 47/47] Compile jbmc/boolean2 test sources Add pom.xml for compilation, move sources, remove obsolete pre-compiled class files. --- jbmc/regression/jbmc/boolean2/boolean2.class | Bin 638 -> 0 bytes jbmc/regression/jbmc/boolean2/pom.xml | 30 ++++++++++++++++++ .../{ => src/main/java}/boolean2.java | 0 jbmc/regression/jbmc/boolean2/test.desc | 2 +- jbmc/regression/jbmc/pom.xml | 1 + 5 files changed, 32 insertions(+), 1 deletion(-) delete mode 100644 jbmc/regression/jbmc/boolean2/boolean2.class create mode 100644 jbmc/regression/jbmc/boolean2/pom.xml rename jbmc/regression/jbmc/boolean2/{ => src/main/java}/boolean2.java (100%) diff --git a/jbmc/regression/jbmc/boolean2/boolean2.class b/jbmc/regression/jbmc/boolean2/boolean2.class deleted file mode 100644 index 86c6fdf0ffacd4ba788d3c2f36a0d329b42addc3..0000000000000000000000000000000000000000 GIT binary patch literal 0 HcmV?d00001 literal 638 zcmYL_OHbQS5QWe985{=!l-6y4w!i|AC{o1|sv@APJ{DA!nw^teDuc0+?I889u<5d! zZVD1eAhmmb6mYJI6E9|b=kd*%xxKso2Vet>9%=|YICwrr^TI{TgN4AwtcN+wyLc&> zUJCPEWkr-G`EHblomlk*(iS+IQ4$sJ1m^O}H-WX2_LN}aW0a`R{o{_xzUpFut&$@9 z$%5s!u50WUVfW}$cv7Z0i?oBsETOf{Zalzx`)NPxst=KdG&*S-t1x-{<}f@BebnLm zn8p(yWAFrlj;_aH@?(9wlDn5>X+~nz>Ee}-*H{oVN7Y|ChpJmp_9(Oyb7R5Np30+4 z^@cp^F8WMx-8MN6j|WII&k58q8dyH< + + 4.0.0 + org.cprover.regression + regression.jbmc.boolean2 + 1.0-SNAPSHOT + + + org.cprover.regression + regression.jbmc + 1.0-SNAPSHOT + + + + + + maven-jar-plugin + + + default-jar + none + + + + + + + diff --git a/jbmc/regression/jbmc/boolean2/boolean2.java b/jbmc/regression/jbmc/boolean2/src/main/java/boolean2.java similarity index 100% rename from jbmc/regression/jbmc/boolean2/boolean2.java rename to jbmc/regression/jbmc/boolean2/src/main/java/boolean2.java diff --git a/jbmc/regression/jbmc/boolean2/test.desc b/jbmc/regression/jbmc/boolean2/test.desc index e457b40c62b..93e69f9d0dd 100644 --- a/jbmc/regression/jbmc/boolean2/test.desc +++ b/jbmc/regression/jbmc/boolean2/test.desc @@ -1,6 +1,6 @@ CORE boolean2 ---function boolean2.entry +--function boolean2.entry -cp target/classes ^EXIT=0$ ^SIGNAL=0$ ^VERIFICATION SUCCESSFUL$ diff --git a/jbmc/regression/jbmc/pom.xml b/jbmc/regression/jbmc/pom.xml index fe5e5e52906..4c59f214dcc 100644 --- a/jbmc/regression/jbmc/pom.xml +++ b/jbmc/regression/jbmc/pom.xml @@ -61,6 +61,7 @@ basic2 bitwise1 boolean1 + boolean2 classpath-jar-load-whole-jar