From e152c92cf0337c8bd402b0ba2b441630f4abf01d Mon Sep 17 00:00:00 2001 From: Peter Schrammel Date: Sun, 5 Aug 2018 11:03:17 +0100 Subject: [PATCH] JBMC tests should not use --cover Use assertions instead. Tests that make only sense with --cover are moved to jbmc-cover. --- .../covered1/covered1.class | Bin .../covered1/covered1.java | 0 .../{jbmc => jbmc-cover}/covered1/test.desc | 0 .../jbmc-cover/generics/AbstractTest.class | Bin 645 -> 0 bytes jbmc/regression/jbmc-cover/generics/test.desc | 9 -- .../json_trace2/Test.class | Bin .../json_trace2/Test.java | 0 .../json_trace2/test.desc | 0 .../StringBuilderSetCharAt/Test.class | Bin 1528 -> 1621 bytes .../StringBuilderSetCharAt/Test.java | 8 +- .../test_dependency.desc | 4 +- .../StringBuilderSetCharAt/test_det.desc | 6 +- .../StringBuilderSetCharAt/test_nondet.desc | 6 +- .../jbmc-strings/StringToLowerCase/Test.class | Bin 1713 -> 1806 bytes .../jbmc-strings/StringToLowerCase/Test.java | 8 +- .../StringToLowerCase/test_dependency.desc | 4 +- .../StringToLowerCase/test_det.desc | 6 +- .../StringToLowerCase/test_nondet.desc | 6 +- .../jbmc-strings/StringToUpperCase/Test.class | Bin 1737 -> 1830 bytes .../jbmc-strings/StringToUpperCase/Test.java | 8 +- .../StringToUpperCase/test_dependency.desc | 4 +- .../StringToUpperCase/test_det.desc | 6 +- .../StringToUpperCase/test_nondet.desc | 6 +- .../jbmc-strings/StringValueOfInt/Test.class | Bin 1638 -> 1743 bytes .../jbmc-strings/StringValueOfInt/Test.java | 2 + .../StringValueOfInt/test_dependency.desc | 4 +- .../StringValueOfInt/test_det.desc | 6 +- .../StringValueOfInt/test_nondet.desc | 6 +- .../jbmc-strings/char_escape/Test.class | Bin 672 -> 947 bytes .../jbmc-strings/char_escape/Test.java | 9 +- .../jbmc-strings/char_escape/test.desc | 9 +- .../IntegerTests.class | Bin 834 -> 1136 bytes .../IntegerTests.java | 12 +- .../max-length-generic-array/MyGenSet.class | Bin 501 -> 501 bytes .../max-length-generic-array/MySet.class | Bin 446 -> 446 bytes .../max-length-generic-array/test.desc | 20 +-- .../max-length-generic-array/test_gen.desc | 21 +-- jbmc/regression/jbmc/array2/test.class | Bin 315 -> 591 bytes jbmc/regression/jbmc/array2/test.desc | 3 +- jbmc/regression/jbmc/array2/test.java | 4 + .../array_nonconstsize_nonconstaccess/A.class | Bin 244 -> 192 bytes .../FloatMultidim1.class | Bin 508 -> 609 bytes .../FloatMultidim1.java | 8 +- .../FloatMultidim2.class | Bin 510 -> 609 bytes .../FloatMultidim2.java | 8 +- .../RefMultidim1.class | Bin 555 -> 658 bytes .../RefMultidim1.java | 8 +- .../RefMultidim2.class | Bin 555 -> 658 bytes .../RefMultidim2.java | 8 +- .../RefMultidimConstsize.class | Bin 487 -> 626 bytes .../RefMultidimConstsize.java | 1 + .../RefSingledim.class | Bin 544 -> 647 bytes .../RefSingledim.java | 8 +- .../test_float_multidim_1.desc | 9 +- .../test_float_multidim_2.desc | 8 +- .../test_ref_multidim_1.desc | 9 +- .../test_ref_multidim_2.desc | 9 +- .../test_ref_multidim_constsize.desc | 6 +- .../test_ref_singledim.desc | 8 +- .../TestClass.class | Bin 399 -> 576 bytes .../TestClass.java | 3 + .../dynamic-multi-dimensional-array/test.desc | 5 +- .../com/diffblue/regression/Foo$1.class | Bin 730 -> 701 bytes .../com/diffblue/regression/Foo.class | Bin 715 -> 864 bytes .../com/diffblue/regression/Foo.java | 4 + jbmc/regression/jbmc/enum_switch/test.desc | 12 +- .../com/diffblue/regression/EnumIter.class | Bin 574 -> 713 bytes .../com/diffblue/regression/EnumIter.java | 4 +- .../jbmc/enum_values_clone/test.desc | 3 +- .../com/diffblue/regression/EnumIter.class | Bin 699 -> 946 bytes .../com/diffblue/regression/EnumIter.java | 5 +- .../jbmc/enum_values_clone_name/test.desc | 3 +- .../jbmc/generic_class_bound1/Gn.class | Bin 831 -> 891 bytes .../jbmc/generic_class_bound1/Gn.java | 4 +- .../jbmc/generic_class_bound1/test.desc | 10 +- .../generics/AbstractImpl.class | Bin .../generics/AbstractInt.class | Bin .../generics/AbstractTest$ClassA.class | Bin 349 -> 349 bytes .../generics/AbstractTest$ClassB.class | Bin 416 -> 416 bytes .../generics/AbstractTest$Dummy.class | Bin 346 -> 346 bytes .../jbmc/generics/AbstractTest.class | Bin 0 -> 941 bytes .../generics/AbstractTest.java | 7 +- jbmc/regression/jbmc/generics/test.desc | 6 + .../KeyValue.class | Bin 562 -> 473 bytes .../MutuallyRecursiveGenerics.class | Bin 361 -> 571 bytes .../MutuallyRecursiveGenerics.java | 3 +- .../generics_recursive_parameters/test.desc | 2 +- .../GenericFields$SimpleGenericField.class | Bin 715 -> 994 bytes .../generics_type_param/GenericFields.java | 4 +- .../jbmc/generics_type_param/test.desc | 2 +- .../jbmc/integer_without_simplify1/test.desc | 2 +- .../nestedobjects/subpackage/Order.class | Bin 719 -> 964 bytes .../nestedobjects/subpackage/Order.java | 2 + jbmc/regression/jbmc/internal1/test.desc | 4 +- .../regression/jbmc/iterator1/iterator1.class | Bin 581 -> 812 bytes jbmc/regression/jbmc/iterator1/iterator1.java | 2 + jbmc/regression/jbmc/iterator1/test.desc | 8 +- .../regression/jbmc/iterator2/iterator2.class | Bin 681 -> 912 bytes jbmc/regression/jbmc/iterator2/iterator2.java | 1 + jbmc/regression/jbmc/iterator2/test.desc | 8 +- jbmc/regression/jbmc/json_trace1/Test.class | Bin 382 -> 625 bytes jbmc/regression/jbmc/json_trace1/Test.java | 1 + jbmc/regression/jbmc/json_trace1/test.desc | 6 +- jbmc/regression/jbmc/json_trace3/Test.class | Bin 314 -> 573 bytes jbmc/regression/jbmc/json_trace3/Test.java | 3 + jbmc/regression/jbmc/json_trace3/test.desc | 6 +- .../jbmc/nondet-static/My$PInner.class | Bin 422 -> 352 bytes .../jbmc/nondet-static/My$PSInner.class | Bin 1480 -> 1419 bytes .../jbmc/nondet-static/My$PrInner.class | Bin 415 -> 354 bytes .../jbmc/nondet-static/My$PrSInner.class | Bin 1433 -> 1371 bytes jbmc/regression/jbmc/nondet-static/My.class | Bin 3011 -> 3726 bytes jbmc/regression/jbmc/nondet-static/My.java | 122 +++++++++--------- jbmc/regression/jbmc/nondet-static/test.desc | 102 +++++++-------- .../jbmc/reachability-slice/A.class | Bin 318 -> 577 bytes .../regression/jbmc/reachability-slice/A.java | 7 +- .../jbmc/reachability-slice/test.desc | 8 +- .../jbmc/reachability-slice/test2.desc | 6 +- .../jbmc/reachability-slice/test3.desc | 2 +- .../test.desc | 2 +- .../jbmc/removed_virtual_functions/test.desc | 2 +- jbmc/regression/jbmc/stack_var12/test.desc | 6 +- .../string_field_aliasing/Cart$Category.class | Bin 406 -> 332 bytes .../string_field_aliasing/Cart$Product.class | Bin 473 -> 400 bytes .../jbmc/string_field_aliasing/Cart.class | Bin 680 -> 830 bytes .../jbmc/string_field_aliasing/Cart.java | 4 +- .../jbmc/string_field_aliasing/test.desc | 10 +- .../trace_class_identifier/TestGenTest.class | Bin 245 -> 509 bytes .../trace_class_identifier/TestGenTest.java | 1 + .../jbmc/trace_class_identifier/test.desc | 4 +- 129 files changed, 345 insertions(+), 318 deletions(-) rename jbmc/regression/{jbmc => jbmc-cover}/covered1/covered1.class (100%) rename jbmc/regression/{jbmc => jbmc-cover}/covered1/covered1.java (100%) rename jbmc/regression/{jbmc => jbmc-cover}/covered1/test.desc (100%) delete mode 100644 jbmc/regression/jbmc-cover/generics/AbstractTest.class delete mode 100644 jbmc/regression/jbmc-cover/generics/test.desc rename jbmc/regression/{jbmc => jbmc-cover}/json_trace2/Test.class (100%) rename jbmc/regression/{jbmc => jbmc-cover}/json_trace2/Test.java (100%) rename jbmc/regression/{jbmc => jbmc-cover}/json_trace2/test.desc (100%) rename jbmc/regression/{jbmc-cover => jbmc}/generics/AbstractImpl.class (100%) rename jbmc/regression/{jbmc-cover => jbmc}/generics/AbstractInt.class (100%) rename jbmc/regression/{jbmc-cover => jbmc}/generics/AbstractTest$ClassA.class (87%) rename jbmc/regression/{jbmc-cover => jbmc}/generics/AbstractTest$ClassB.class (79%) rename jbmc/regression/{jbmc-cover => jbmc}/generics/AbstractTest$Dummy.class (87%) create mode 100644 jbmc/regression/jbmc/generics/AbstractTest.class rename jbmc/regression/{jbmc-cover => jbmc}/generics/AbstractTest.java (72%) create mode 100644 jbmc/regression/jbmc/generics/test.desc diff --git a/jbmc/regression/jbmc/covered1/covered1.class b/jbmc/regression/jbmc-cover/covered1/covered1.class similarity index 100% rename from jbmc/regression/jbmc/covered1/covered1.class rename to jbmc/regression/jbmc-cover/covered1/covered1.class diff --git a/jbmc/regression/jbmc/covered1/covered1.java b/jbmc/regression/jbmc-cover/covered1/covered1.java similarity index 100% rename from jbmc/regression/jbmc/covered1/covered1.java rename to jbmc/regression/jbmc-cover/covered1/covered1.java diff --git a/jbmc/regression/jbmc/covered1/test.desc b/jbmc/regression/jbmc-cover/covered1/test.desc similarity index 100% rename from jbmc/regression/jbmc/covered1/test.desc rename to jbmc/regression/jbmc-cover/covered1/test.desc diff --git a/jbmc/regression/jbmc-cover/generics/AbstractTest.class b/jbmc/regression/jbmc-cover/generics/AbstractTest.class deleted file mode 100644 index d2fff4e9d81ddbb304a16017659f3ce377b37147..0000000000000000000000000000000000000000 GIT binary patch literal 0 HcmV?d00001 literal 645 zcmZuuO;6iE5Ph52*~D>6NJ7g;QwXIcp(|-oH`xBK zLZ`TdZnigd!^z&MccJuNj}-R=s`py{6|bC;6o3j+B7u6VJ$%@-L%o@F&QqBkG$DD9 z`pJRPqC&gKs6iA&bLSf3iVo+}7E-cETSJ{C`sfFuNnHDh+^1{gkKcZWA@B?4$-8eT vyf>DNuXhcqFz8n~vqoFTGM4!2>CgB*PrYSW#8u?kR-#0|Otgtlh);oA0#u5P diff --git a/jbmc/regression/jbmc-cover/generics/test.desc b/jbmc/regression/jbmc-cover/generics/test.desc deleted file mode 100644 index 0fe333922c8..00000000000 --- a/jbmc/regression/jbmc-cover/generics/test.desc +++ /dev/null @@ -1,9 +0,0 @@ -CORE -AbstractTest.class ---cover location --function AbstractTest.getFromAbstract -^EXIT=0$ -^SIGNAL=0$ -file AbstractTest.java line 18 .* SATISFIED -file AbstractTest.java line 19 .* SATISFIED -file AbstractTest.java line 20 .* SATISFIED -file AbstractTest.java line 21 .* SATISFIED diff --git a/jbmc/regression/jbmc/json_trace2/Test.class b/jbmc/regression/jbmc-cover/json_trace2/Test.class similarity index 100% rename from jbmc/regression/jbmc/json_trace2/Test.class rename to jbmc/regression/jbmc-cover/json_trace2/Test.class diff --git a/jbmc/regression/jbmc/json_trace2/Test.java b/jbmc/regression/jbmc-cover/json_trace2/Test.java similarity index 100% rename from jbmc/regression/jbmc/json_trace2/Test.java rename to jbmc/regression/jbmc-cover/json_trace2/Test.java diff --git a/jbmc/regression/jbmc/json_trace2/test.desc b/jbmc/regression/jbmc-cover/json_trace2/test.desc similarity index 100% rename from jbmc/regression/jbmc/json_trace2/test.desc rename to jbmc/regression/jbmc-cover/json_trace2/test.desc diff --git a/jbmc/regression/jbmc-strings/StringBuilderSetCharAt/Test.class b/jbmc/regression/jbmc-strings/StringBuilderSetCharAt/Test.class index 08c0c54995546515ef6798be91476ac741497396..8b1f79ecc44b6256e1c99b842edc659bb3bd4f59 100644 GIT binary patch delta 700 zcmZ9K%TE(w6vcltbUM@NpcRTx<BLQZbQts*^jA{}odJ_17j-UeP20iR`Ldl|ow4sN z*qODQ!08Nby-jT$Y;Fu$q!_liOq0bK>ZD>ZLRz6|#lCMR*6jRJ;!3HME0&iF`K!fZ zp{P(hyIu|#?uIjk_57WZg2&EeBNn5KiNBC5m377~CYV$RoS@8RR&v?$KdE`GTwKmC zIX{#UXH0!(DoxbLgICUh`Y1Z{0ezeL_#TF_gMT02Vg>Vad{;VD&WfEQ=xo+pzqu*V z4vmB)=STU)j?Ouq^C&daBDMjPIf3>{!?%6Z#aIPT+S6j(jtTlp0)hG?M{jwKx6bca zo+le=%_R^FY5y?@X(tqJxkQ>VWln@vI%y+Dm?4QKXy+Oo+>q=dQ8IL~N;f5Xct9@? zi`jVBHjA?W5K>Bl4f>x-ko=!o&BPIrdB@xe*XdRIA!B7 zVp6ggwb3a@VJr$2o1;`M#*^%$W>Js!6DG%ORMgS1InJcXRCmSie)76+9Ie#-{>YnF zVmqUlWzeLlm}6ceeQsmDuy(D`UfWo`(oyUuqha{%%SFWki$PCw)5gWCopqBFijyn_ zU$ue2(wiyghJV{{-11kiH-e@f+I%A>bnqbfq2Et$Nv3g7;#o4mtJs-2jUjSU8xWx? zXXB!UJLs+2HpYVCT9;}e=1Uysz~97lpOeT~!LspqGqThBb{EJ>p2OxaMe>Z|Qe&7I zj<7_5(^5Up2rWvqMZHOx4rAP%!=YVV{&I zLK-8u6EAKidra0tL9#hL>I;dEB_KPo}mHM#oRgfoZrm-&hOmK;ESf!FTX!-0XgOa944!B zB7lpmMt^_-2A$22#z~Ew#wm?qCvn7%n8ReCNwUp zTnaGBluBM9(p56ea?Pr&RL#kXxwbkN4Hm7^{fC9pW-=TD3~`fr2t&FvG0<-PJib$E-qI zakrAJu2{)(bxB0Yrxj~CIU(ATf@i*LS}HdTZc==ocjpxUD{0d$zAW0$J)_-)cNptL zGIfI5YxGYv-TpxH=gfvETqI@f!Eb-_B&NpDS-_xEayrTm3o2bI-6$eS$$Cr*+wze| z-cQokY7P1JfL}h+4;f~WM(GZ6ik>QVtsd?I&CBdyuj&fIMO_4dx1aTYs4tMt3>7~zp z>y1bMZJ^a@AZBk%1L9aZ8;;kJT*sbeyRgwl`sIO>f6!6g_VSn8z@*Fdb+uR1qj`9Vpl$wN~5GQnXfEv?l7p1<O29g=#%7mRu zlV(I74YJ!PPbk~J(@6NdO1Kb(oeGqivV%|IV+&lN3bMMQcBY*qz?++gV?@agk$Dz)KuU9G3;W!m;ed7*;q|6%nJJMU>HeOZM$Z*>dl5-s@wbRit1@J8>L!{A?19R4d;~{-2W1ELTpJ^PPsZYii}xP{yAHsw6?Hp!|)vsrOoxR(7LLJToF zPeXBjxF*sJ2_%U-L);sxl<9t8cA*7~*YN26j;RlIF?>ik;B2`k+QBY7chgisr~Wr^ z57<8F!Y7`RdQTPLCp-)<0?-gd2s#bdpj-$uG}}3hVo{76r%ldazWC3 zBrk=jzQ{H@)Ye6*N9GB%|CH)N=}6}o(*5_4g-rT{D3Y`tJ;3-|7>6)3dZ-JkjUOXS zg`=N(w9%&z;2Y4He>PHN09c5Vn*=#YlG;g9IZgUa6p*H!&Eg?)J>44Ie#!R>IR(>U haLhO-p0iWN5q0Pf#Y1+)E`&)pnOvpi;#@Cn{sECmcb@n!3Ml^s6&1u5L`gg}p#sKilXlgMNxy&x z&7Q=IdNA>Znv_Hny_x7I(8Len2N2^kEsEhV@6J5)&b+^U-uV)E6)b=K{r)3>A*}e& zjy@e}A6)2@==Wg&gKBX?Vn{7cN(@V!k~po@kvgSy7bth&O>{#AfV^ZwFro9o%F?UM9vy?B{I+hG9 zcP7~a;ZpC@#886SjMPLh|WCcO_0{#!Ezqx~kPswd&xNw9qjygsUB)l-8 z5nHE5qp6R=hY9$3xq&Wb`5|_(tfO0{2=w3>V~iW$c$tUadkGe52)~48Hf|?OQ&te# z;v(#%z0qJ(1=>oIDU4>5v+8XtFVy%_2l!I^eB*2(&`27S6d^Prj21*#wi&&g4YJ=O zXd`Dk8`(j}qqu=XxP`+gF-vg=;5PibSp7%di{n-DIIz8kemn6Q#sT~aB8tA*`RR?8 z>0=^gwp6vFe~ql-himfFeSiPsulXA%Lk}8gSSzVJkR*2+!*qF`vo$_+#c9ABaQT0s ppZ-SJg9QJfX7CW4M_QyO@P=8nzG>V6hdSql%b4Vg;I(Qy^#^S_g@ynC delta 715 zcmZXSO>YuG7{~v!!0rIMlx~3{imrv0R-jfy6l+UcwbmDGD`55D0WDgh0Rx+OG2t7S zG;^{C4<1ZBi8jHcP4s4>@gw*J^fMUsnZBe4FFXJFKQHr}XZDTntI_%PXX_JyEN**n z7-Uf`JGn3l4@G2_M|%yP_W zxah&4Y<$Us%b3@2g<&9GZMSPJyWU*yRMvlGd`8KxK6qTLJ}p=8KdFfbn{;Sc5Eb^^ zyP)GLVmhwjy7^%VZeo!^FRe9Ow$-*<^~NIxR@JeDW${;uC2nDvAza#t zSdFG_)f%gmWIe0fYZm1lL6iz+#djrYILo!Rt)Zl&jLK%oF~{6Zx}`$1DTr6jX`@Su z;W&MdLKDmtU15l0m^_QTca-U%^#=j(lg$n ztBp{V6N>I7!URV5IJ?xAbV&VgTx>H`~hSK zcI}t&?%U}D;1NOvh6p=G$Z^6NCY(_MO(KUBiWtW#{Us7mhs#jBzcHa(q1xD(WOs7OQ{s7m; zM0UDy>mw;fg6>`TBm4!rG%@PAcYtDmgf#ii%$ak}{mysJ?bkn_J_8uQH4Vp+_98er zuAvLv;%P#_q<|>_83EJYzdyFV2>2{us|Jne5gEM-&S^M?w1PejA*2QLt2i(0fQkzu zXi&kBhGAS(Fv1XNGfE|HJ7&=;Wz3SXP~dq6HqQ_kH7(N_WAG+B?=bkLih0fu%$gRT zDL-1^_M8Z2P;<*Xx02xwLp0f$eQ2y1y#>Qs>Ya6L(^|U3P&exsxs_YSs?1P8u3DKi zQ?z7WL-NLfi4hrf*L0RMe3e^yZsnd3ljOW0q>kna+YGhYV%g5|tES*nGsjC#kD#IB zBu>$BI!4j1BaRa~E`vI1s*;@8>3-U_i#9`J^^?ngvTPRe+}3dg<0MRrjtL|fJbnE- zCNV{H#CZxbI;L@zAyh4Jd*LC^kt};$ZcPSd%_x-l?M0Hgz^x@`S;~BaUX4}JDMNR1 zzm)q$+GaM=9K9JExi4Yf#-_Z;dlNLOwYL0X3puA?3^6gh_o<`KmMG++@i6sVR>*^f!Y zrzGHWlCYJkt6;zJT)`Qt+lKaSg?_?I9KcqjLfN?Q0X3eD`&|=ojp7>BHNLzX;+lYK z6xXQIY$8M*)~727ha&_PM6-K*amwHCJup)8IAW|Md&F4h=oB0&$x-Y2g#g>Z?$}9% z|HhuKj(t(?c?%6aLBnmOA)cXOwb4^MI?+KRKZ_wGF-C9Gv;zi^(_VSshu0vo{~o5c__F}yo|X1e3=pt|l|TBYIB_;E3$%b~tRT(VB5 z!wnV0*3r7NtY<|Yb>&qFQW?)GM&xDaRtlJFENXKIa*K{t;8T<(&%jXKumbtko z$PC`p8c%J^aEqZj(veu#xAdNjo?Y!(uuLPnI?hlg8FRU;B-KRjpUbL}tS5%GHp4f0 zHqEoC7j$hTDQ+)cu=Lc%Lw!?Ts$i7vok(SlGE^6G1vAC(8X_OxBF|ghA`J~!agDed z#?Z`A`+sWjf{{scQ^PnWsOCluw?J?OVFpKEzlPhm!%$Z`Hgzo3tZC*r z;tYWjbAEZ9r$~`gE?W);WlPT#`1}eftZ#}!8M-28Wjm|UQMx3k*UBA7Q}dQ?T6rNG zL(O?{sFnUwV$&JwH$y1R^M=XOCl!&tR)Jnnvy*6|v8khJWPv)N20gjKgqVc&^sk;Q z6W-`9*n2_5bwZDHQU}n0MtT<1A7lmfRnYMX&Idu4M7KnbL`9-kqEDhKu}tDcZ_l2! zBVTYf`tBslBo!wL^3YF%f*`z9tdA;C(SkBW$=i!^+K>uNz>hcrxQ9y25pxk$NYV~1 zp$01yCxcp;box2T^pb?~k#x;=*SdTPmXzeOaos|IBXX?N z&Sg2N4b;p=YFZODrhTteC~i2kNwI(td1=Q#azsoH diff --git a/jbmc/regression/jbmc-strings/StringValueOfInt/Test.java b/jbmc/regression/jbmc-strings/StringValueOfInt/Test.java index 1af7317bca5..323958250a5 100644 --- a/jbmc/regression/jbmc-strings/StringValueOfInt/Test.java +++ b/jbmc/regression/jbmc-strings/StringValueOfInt/Test.java @@ -23,6 +23,7 @@ public static String checkDet() tmp = String.valueOf(-1000003); tmp = String.valueOf(1000004); tmp = String.valueOf(1000005); + assert tmp.length() < 5; return tmp; } @@ -51,6 +52,7 @@ public static String checkNonDet(int i) tmp += String.valueOf(-i + 1); tmp += " "; tmp += String.valueOf(-i - 2); + assert tmp.length() < 5; return tmp; } diff --git a/jbmc/regression/jbmc-strings/StringValueOfInt/test_dependency.desc b/jbmc/regression/jbmc-strings/StringValueOfInt/test_dependency.desc index 18c4b3b0f9a..23646edbe11 100644 --- a/jbmc/regression/jbmc-strings/StringValueOfInt/test_dependency.desc +++ b/jbmc/regression/jbmc-strings/StringValueOfInt/test_dependency.desc @@ -3,8 +3,8 @@ Test.class --function Test.checkWithDependency --depth 10000 ^EXIT=10$ ^SIGNAL=0$ -assertion at file Test.java line 61 .*: SUCCESS -assertion at file Test.java line 64 .*: FAILURE +assertion at file Test.java line 63 .*: SUCCESS +assertion at file Test.java line 66 .*: FAILURE -- -- Check that when a dependency is present, the correct constraints are added diff --git a/jbmc/regression/jbmc-strings/StringValueOfInt/test_det.desc b/jbmc/regression/jbmc-strings/StringValueOfInt/test_det.desc index 8fc14e7e524..fe9947fcaa7 100644 --- a/jbmc/regression/jbmc-strings/StringValueOfInt/test_det.desc +++ b/jbmc/regression/jbmc-strings/StringValueOfInt/test_det.desc @@ -1,9 +1,9 @@ CORE Test.class ---function Test.checkDet --verbosity 10 --cover location -^EXIT=0$ +--function Test.checkDet --verbosity 10 +^EXIT=10$ ^SIGNAL=0$ -coverage.* file Test.java line 25 .*: SATISFIED +assertion at file Test.java line 26 .*: FAILURE -- adding lemma .*nondet_infinite_array -- diff --git a/jbmc/regression/jbmc-strings/StringValueOfInt/test_nondet.desc b/jbmc/regression/jbmc-strings/StringValueOfInt/test_nondet.desc index 7342d08a711..5d31175c3b9 100644 --- a/jbmc/regression/jbmc-strings/StringValueOfInt/test_nondet.desc +++ b/jbmc/regression/jbmc-strings/StringValueOfInt/test_nondet.desc @@ -1,9 +1,9 @@ CORE Test.class ---function Test.checkNonDet --verbosity 10 --cover location -^EXIT=0$ +--function Test.checkNonDet --verbosity 10 +^EXIT=10$ ^SIGNAL=0$ -coverage.* file Test.java line 53 .*: SATISFIED +assertion at file Test.java line 55 .*: FAILURE -- adding lemma .*nondet_infinite_array -- diff --git a/jbmc/regression/jbmc-strings/char_escape/Test.class b/jbmc/regression/jbmc-strings/char_escape/Test.class index 5ffa97543e07f6203d0805cd7d65dc7b0f94a79c..f866609afb5700c667c08632dbe9883865e64e0e 100644 GIT binary patch delta 568 zcmZ9IPfrt36vcn9)ADA9SD>w8K`Zh{fhtrHT^XZMS-9z_uhB!x%Zs&4su8O<@Z0IzXF@w^_k$3rs8th zC&Qc#S8SMfS@2n8$-{6}bIr%M$Yq}uRy9>cX(>pOFixXxCwUwtL9-pU6l%M_QLk1M z?!BFM)QQsj3cu0q#XI3v)D9KivoJ~5Uj=UhLxE!dV6I-^y5R3Y7&FD$>% z+%()`!!XH|qHLFH?Vz(;dw9b9B#yhWB5RLoZW}Rmr~mWAo?`Mp`cYeyDyCau62)Qb zbh(iRX-@{u%IY@rVst`&MNO40om39WDwJ4~S4FatoU0zAK3X8>B#w=mVvF-kOKqXQ z(2g{qzyCuuo|Zo04H*A||NNNoZ`s2ccgR>#4{-;a89Ik&!Ez=uV%nmxU(c-dnj)_y z!d{ECJ>h#R%W)?^!Fg3*G) z(q}TpyE`{IbMMUg&V4s8@#)Xs*Ah76(BarHv@Mwk diff --git a/jbmc/regression/jbmc-strings/char_escape/Test.java b/jbmc/regression/jbmc-strings/char_escape/Test.java index 791563bbbc0..467e0f838e6 100644 --- a/jbmc/regression/jbmc-strings/char_escape/Test.java +++ b/jbmc/regression/jbmc-strings/char_escape/Test.java @@ -10,10 +10,15 @@ public static boolean test(char c1, char c2, char c3, char c4, char c5, char c6, sb.append(c6); sb.append(c7); sb.append(c8); - if (sb.toString().equals("\b\t\n\f\r\"\'\\")) + if (sb.toString().equals("\b\t\n\f\r\"\'\\")) { + assert false; return true; - if (!sb.toString().equals("\b\t\n\f\r\"\'\\")) + } + if (!sb.toString().equals("\b\t\n\f\r\"\'\\")) { + assert false; return false; + } + assert false; return true; } } diff --git a/jbmc/regression/jbmc-strings/char_escape/test.desc b/jbmc/regression/jbmc-strings/char_escape/test.desc index 46c23067a93..d25b7391444 100644 --- a/jbmc/regression/jbmc-strings/char_escape/test.desc +++ b/jbmc/regression/jbmc-strings/char_escape/test.desc @@ -1,6 +1,9 @@ CORE Test.class ---function Test.test --cover location --trace --json-ui -^EXIT=0$ +--function Test.test --trace --json-ui +^EXIT=10$ ^SIGNAL=0$ -20 of 22 covered \(90.9%\)|30 of 44 covered \(68.2%\) +"reason": "assertion at file Test.java line 14 +"reason": "assertion at file Test.java line 18 +-- +"reason": "assertion at file Test.java line 21 diff --git a/jbmc/regression/jbmc-strings/max-length-generic-array/IntegerTests.class b/jbmc/regression/jbmc-strings/max-length-generic-array/IntegerTests.class index 6120bff5bb6f256912ddb4120be2d604bb633a6e..0b37d96013b83bdd30c99afc78adae91703a877e 100644 GIT binary patch literal 1136 zcmbW0T~8B16o%hvcRTHNfqqd@L8TV$hf+lpwTOI(1OswWVq(2o+L0{QU9-C->3=Zs zTK<5y_z@tIsCOp*CSyEPx^%tuW_Eh!%zK{m&gri|U%vsE#)5_vavYa6gpiBTlINJv za0ORoq!2>_MUIk&7;+lQxW;i^gD!J*Ov+t_8e1*V zWMFlM$gF9Z-W)@?P<+OqEZI%LFtlb`;%WQ!mT)#@GK203*IVzb2&*PMhC*R&$JjM0 zEyLQbtXiJf7EZMoh%MT7OBhy_VW8$2jaTc&o30Wy#Sl9YBPHTyh|V@zJqoR6x1EM~ zY|5I+p717>b|+;$9mB}d1s_Bwvu-nFUIZ%pG#qzy%;2t$d$_M7jSRy`A9}$zWZ7|S zhodT!XBpJ>4sl8033>AYwI0OanA7nP^9+f;*2dP3Xpk$a;W$Qz><;pr9Fh^q{)L_* z1K%}TZL#r^AzN4t`sa5+%{FYyGfc~67!JDL(=E~?29$fgOTBtfum2v|pom{aston{ zmRd9~q|p?v>4@g3SM-!#n+|AL>KLafOwqiu#E5j4b_$3QSz6D~uQB>E`l_Wvu#Ykk zBeX`kK^g*_#W~u`)OQHeTmw%^KcTYyV}za`BD_}q0_6wPa6%j*QY)7Zz~3YL3DG^o zj}fCB?YnY>`2N44undt}s9P_GDD4%ht74GWQE=obHbn$8h+~=lE$1mC4khv%WsXs0 zfR4sa;okP(R(v>}3J*xQ!2sFN|B@w$DM@50@*_>AW>6s$r^%N^;_s6cI4%%b6cr- zf(D6>Kj8xqV$MQD106$e!;D5mD1 zj)ugd16w`YSW>7du`IE2)r-86fE|VXs6FU}5es7>8u=-B0#arzZBm-1wMZIhbxJTV6ya;2Sz=WhvQ=Yl#k$_Ov{GYOLtO=OTGEw+L7ZZ@K`|30NV>8x zOO_vGexNRqBh3E{J^vmW_%ATT@DcXu2+nbEhY8&a$1ppAe-HN>|Md3$2)dL~+oe(9 SW=-z)D_E77qyIwUasCS(IX2w@ diff --git a/jbmc/regression/jbmc-strings/max-length-generic-array/IntegerTests.java b/jbmc/regression/jbmc-strings/max-length-generic-array/IntegerTests.java index c57b3e19be8..ad81b8ac686 100644 --- a/jbmc/regression/jbmc-strings/max-length-generic-array/IntegerTests.java +++ b/jbmc/regression/jbmc-strings/max-length-generic-array/IntegerTests.java @@ -4,7 +4,11 @@ public static Boolean testMyGenSet(Integer key) { if (key == null) return null; MyGenSet ms = new MyGenSet<>(); ms.array[0] = 101; - if (ms.contains(key)) return true; + if (ms.contains(key)) { + assert false; + return true; + } + assert false; return false; } @@ -12,7 +16,11 @@ public static Boolean testMySet(Integer key) { if (key == null) return null; MySet ms = new MySet(); ms.array[0] = 101; - if (ms.contains(key)) return true; + if (ms.contains(key)) { + assert false; + return true; + } + assert false; return false; } diff --git a/jbmc/regression/jbmc-strings/max-length-generic-array/MyGenSet.class b/jbmc/regression/jbmc-strings/max-length-generic-array/MyGenSet.class index e92e43fee856008bdc97ae12d7bab364c7cd6c44..d7dc326cc8ac29d3783936c895086df59088b22e 100644 GIT binary patch delta 35 pcmey${FQk_7bB+v0}F#913!b(& C{RMsi delta 50 zcmdnTypMT9G9#x70}F#H0}q4Rz CEd@>h diff --git a/jbmc/regression/jbmc-strings/max-length-generic-array/test.desc b/jbmc/regression/jbmc-strings/max-length-generic-array/test.desc index e712029ce44..56373bd9be5 100644 --- a/jbmc/regression/jbmc-strings/max-length-generic-array/test.desc +++ b/jbmc/regression/jbmc-strings/max-length-generic-array/test.desc @@ -1,19 +1,7 @@ CORE IntegerTests.class ---max-nondet-string-length 100 --function IntegerTests.testMySet --cover location -^EXIT=0$ +--max-nondet-string-length 100 --function IntegerTests.testMySet +^EXIT=10$ ^SIGNAL=0$ -coverage.* line 12 function java::IntegerTests.testMySet.* bytecode-index 1 .* SATISFIED -coverage.* line 12 function java::IntegerTests.testMySet.* bytecode-index 3 .* SATISFIED -coverage.* line 13 function java::IntegerTests.testMySet.* bytecode-index 4 .* SATISFIED -coverage.* line 13 function java::IntegerTests.testMySet.* bytecode-index 6 .* SATISFIED -coverage.* line 13 function java::IntegerTests.testMySet.* bytecode-index 7 .* SATISFIED -coverage.* line 14 function java::IntegerTests.testMySet.* bytecode-index 12 .* SATISFIED -coverage.* line 14 function java::IntegerTests.testMySet.* bytecode-index 13 .* SATISFIED -coverage.* line 15 function java::IntegerTests.testMySet.* bytecode-index 16 .* SATISFIED -coverage.* line 15 function java::IntegerTests.testMySet.* bytecode-index 17 .* SATISFIED -coverage.* line 16 function java::IntegerTests.testMySet.* bytecode-index 21 .* SATISFIED -coverage.* line 15 function java::IntegerTests.testMySet.* bytecode-index 19 .* SATISFIED -coverage.* line 15 function java::IntegerTests.testMySet.* bytecode-index 20 .* SATISFIED -coverage.* line 16 function java::IntegerTests.testMySet.* bytecode-index 22 .* SATISFIED -coverage.* line 16 function java::IntegerTests.testMySet.* bytecode-index 23 .* SATISFIED +assertion at file IntegerTests.java line 20 .*: FAILURE +assertion at file IntegerTests.java line 23 .*: FAILURE diff --git a/jbmc/regression/jbmc-strings/max-length-generic-array/test_gen.desc b/jbmc/regression/jbmc-strings/max-length-generic-array/test_gen.desc index ca374b5183c..1e86880a323 100644 --- a/jbmc/regression/jbmc-strings/max-length-generic-array/test_gen.desc +++ b/jbmc/regression/jbmc-strings/max-length-generic-array/test_gen.desc @@ -1,20 +1,7 @@ CORE IntegerTests.class ---max-nondet-string-length 100 --function IntegerTests.testMyGenSet --cover location -^EXIT=0$ +--max-nondet-string-length 100 --function IntegerTests.testMyGenSet +^EXIT=10$ ^SIGNAL=0$ -coverage.* line 4 function java::IntegerTests.testMyGenSet.* bytecode-index 1 .* SATISFIED -coverage.* line 4 function java::IntegerTests.testMyGenSet.* bytecode-index 3 .* SATISFIED -coverage.* line 5 function java::IntegerTests.testMyGenSet.* bytecode-index 4 .* SATISFIED -coverage.* line 5 function java::IntegerTests.testMyGenSet.* bytecode-index 6 .* SATISFIED -coverage.* line 5 function java::IntegerTests.testMyGenSet.* bytecode-index 7 .* SATISFIED -coverage.* line 6 function java::IntegerTests.testMyGenSet.* bytecode-index 10 .* SATISFIED -coverage.* line 6 function java::IntegerTests.testMyGenSet.* bytecode-index 13 .* SATISFIED -coverage.* line 6 function java::IntegerTests.testMyGenSet.* bytecode-index 14 .* SATISFIED -coverage.* line 7 function java::IntegerTests.testMyGenSet.* bytecode-index 17 .* SATISFIED -coverage.* line 7 function java::IntegerTests.testMyGenSet.* bytecode-index 18 .* SATISFIED -coverage.* line 8 function java::IntegerTests.testMyGenSet.* bytecode-index 22 .* SATISFIED -coverage.* line 7 function java::IntegerTests.testMyGenSet.* bytecode-index 20 .* SATISFIED -coverage.* line 7 function java::IntegerTests.testMyGenSet.* bytecode-index 21 .* SATISFIED -coverage.* line 8 function java::IntegerTests.testMyGenSet.* bytecode-index 23 .* SATISFIED -coverage.* line 8 function java::IntegerTests.testMyGenSet.* bytecode-index 24 .* SATISFIED +assertion at file IntegerTests.java line 8 .*: FAILURE +assertion at file IntegerTests.java line 11 .*: FAILURE diff --git a/jbmc/regression/jbmc/array2/test.class b/jbmc/regression/jbmc/array2/test.class index 507d6622e5c18acd6a36bd9c7efed1556f2351ec..10fc89c0a6861638963c32b5bb866eee630529d8 100644 GIT binary patch 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 delta 197 zcmX@lvYSct)W2Q(7#J8#7=*YOm>Kxk8Ti>51SUGVstGbOa0Ta=7A2>;W#*(ZGH{lp z7MJK{C6*=fFt9MNGBU7$1SZ~>@MTbBU;^p|0VW2ZI0Gw?WCQYKfixqKX4Trxz_<~} zU}Rtil5Ai>kQ4_4Cy)dw4FMVeGD2c> 0) arr[0]=1; + if(unknown > 0) + assert arr[0] == 1; + else + assert arr.length == 0; } } diff --git a/jbmc/regression/jbmc/array_nonconstsize_nonconstaccess/A.class b/jbmc/regression/jbmc/array_nonconstsize_nonconstaccess/A.class index e31a62ef61b4c664bcd57cbc53f87bef3a770201..14f1d91ebe75e467d02a40f1a87fcb2b7db21a55 100644 GIT binary patch delta 73 zcmeyucz{v#)W2Q(7#J8#82Gsum>GE38F<+l_$G=PP0S3`kY!*5LIws_t?dkq8-WZ) S22LQ!1{MTKaRGTu4BP+_013SS delta 124 zcmX@W_=QpQ)W2Q(7#J8#7=*YOm>Kxl83foF1Sg6bDG2%GCnx5FB^G5SCgr4tfCxqg zmXeIjVnzmLA4ltnuEAFN42(d?z`&}toq=&9kio>j2_)ITf{YAYKsFCV0RuOX#QrSW0H@~@xc~qF diff --git a/jbmc/regression/jbmc/array_nonconstsize_nonconstaccess/FloatMultidim1.class b/jbmc/regression/jbmc/array_nonconstsize_nonconstaccess/FloatMultidim1.class index f894ebdb1e03d34c2b5dedb798fb8f3847506794..ba36f3ebae809d73a9451f7d3c3772823678e10c 100644 GIT binary patch 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 literal 508 zcmY*VO-lk%6g_ulY|PBBGAk>{T4+dOxGUTQf}lkdZCX8Ts^9RP|h4Pe9ARa&HB(TE*)szuxzJ_uOq4cLj1m>1;K3 zc2;50VpIi&D$-{R-3w-qebv0KtDA{h=(yYOHJys9{pS8lZnxB(3L}6iLF9jn{<>N4 zROhmA*l0OTAL}r=r~V9xW-;5W3Ot2pVCxO?I%)@*bsLOn=J0p`A2wLT51k7@Nb;k-HGo)PB`E98$cAUAoMz9l%ve? 0 && y < 5) { - float[][] a1 = new float[y][2]; + a1 = new float[y][2]; int j; if (y > 1) { j = 1; @@ -9,9 +10,8 @@ public float[][] f(int y) { j = 0; } a1[j][1] = 1.0f; - return a1; - } else { - return null; } + assert a1 == null; + return a1; } } diff --git a/jbmc/regression/jbmc/array_nonconstsize_nonconstaccess/FloatMultidim2.class b/jbmc/regression/jbmc/array_nonconstsize_nonconstaccess/FloatMultidim2.class index 4d40ffc37417eb12b337bd1e8bc679df2cb0c195..a2ca10913d17524e6b348795d1049d3ca8f19b05 100644 GIT binary patch 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-OSQY6r8==croV7`0c4+w1`FwN;)Nt5D*eYlr&bG%c&PHiNuTGpRo|ZPP7s% z>}>o;LJ(&!*SPTB?wj{!W_Q1TKRyAJv5Gsc5(B}+{<>N6 zRrj)V+-$o}fK`}$r(OnxW-(i=O56qa*ycOLTiA{>>oyqU%*oLJ5|{|FBvM2)`6Uu9 z+7DQ>x-Fj&mz8J4%*vMBT~3~Cy-KNDucVpK7Wpunw2;WsaE6kLtd?k# zr|CM 0 && y < 5) { - float[][] a1 = new float[2][y]; + a1 = new float[2][y]; int j; if (y > 1) { j = 1; @@ -9,9 +10,8 @@ public float[][] f(int y) { j = 0; } a1[1][j] = 1.0f; - return a1; - } else { - return new float[1][1]; } + assert a1 == null; + return a1; } } diff --git a/jbmc/regression/jbmc/array_nonconstsize_nonconstaccess/RefMultidim1.class b/jbmc/regression/jbmc/array_nonconstsize_nonconstaccess/RefMultidim1.class index 4102562d05f53b2876a84b9e00ae79c0eae02778..38ea3340b0c22e4a80f2026fe5ff8db7f3c77a97 100644 GIT binary patch literal 658 zcmYjOT~8B16g_u$wzJ(XwB^f6t%#xmR#8HHku)|a5kobx#zc79b_X-Kv}Skfk0Hhf zW5TN+Q4&ei7k%(28DhLs3z*H^xwGfYnR8}-{rU10z!ENd$e|>0T4K_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(kl8IdVamT2e69SI2=qn7sm_vj!(8~aoAx0Z#l;thF z?S)&&b?f{Gl+`td-9Ck?6`a0S~e zEY9Su|1kgD!YXS&@7};(?8qaG4s%WDe%~ob`!Uu_uzQkXQ;gDl%}_y(-B;LI>sf`3 uNpeRpN}IqpjA5MLN)vs@sHm@2dr9&H6U-cj*+t5M(S^thAz_N1$kZE{<5Ua) diff --git a/jbmc/regression/jbmc/array_nonconstsize_nonconstaccess/RefMultidim1.java b/jbmc/regression/jbmc/array_nonconstsize_nonconstaccess/RefMultidim1.java index 58ed13eaaa4..2c00d0f5cb4 100644 --- a/jbmc/regression/jbmc/array_nonconstsize_nonconstaccess/RefMultidim1.java +++ b/jbmc/regression/jbmc/array_nonconstsize_nonconstaccess/RefMultidim1.java @@ -1,7 +1,8 @@ public class RefMultidim1 { public A[][] f(int y) { + A[][] a1 = null; if (y > 0 && y < 5) { - A[][] a1 = new A[y][2]; + a1 = new A[y][2]; int j; if (y > 1) { j = 1; @@ -10,9 +11,8 @@ public A[][] f(int y) { } a1[j][1] = new A(); a1[j][1].a = 1.0f; - return a1; - } else { - return null; } + assert a1 == null; + return a1; } } diff --git a/jbmc/regression/jbmc/array_nonconstsize_nonconstaccess/RefMultidim2.class b/jbmc/regression/jbmc/array_nonconstsize_nonconstaccess/RefMultidim2.class index fa85a072b9f289ec63d816343f866116cb8762ec..f55c4cdf72643c89883501ec1d8e4551803e9bfb 100644 GIT binary patch literal 658 zcmYjOU279T6g_u8GMmk`N&01MjI~;|t+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>$xo7=#spStzyy*1J*H7o_UJ(0@M}wEgi1)$S8nu8%sZ-%{g1$8*pMPlIzovVQ0v zHzxfs=mvxG8-W}PqJ>)V=%`-RVUMRKFw~B~{tsRX63tL`J~h(j5ryjX?5}sSlqy#cZISS{fsT!`vt>jc-9w0t;#iQ zv$AQG^Y<`6-oa{WzwCa6y?G-)Vcam+gzmRNLE4Y8UYgz4C^pL|$JYWC?6CW5cGh}! wVdDw8OIW5&V;w74<+pM~A22GKtJU5bd4k8xOu?KY>%f>o 0 && y < 5) { - A[][] a1 = new A[2][y]; + a1 = new A[2][y]; int j; if (y > 1) { j = 1; @@ -10,9 +11,8 @@ public A[][] f(int y) { } a1[1][j] = new A(); a1[1][j].a = 1.0f; - return a1; - } else { - return null; } + assert a1 == null; + return a1; } } diff --git a/jbmc/regression/jbmc/array_nonconstsize_nonconstaccess/RefMultidimConstsize.class b/jbmc/regression/jbmc/array_nonconstsize_nonconstaccess/RefMultidimConstsize.class index c474465f50d05b7d9dcdf10cc5cfef773c1f0e77..1287e3d6ba63003c18ebeea2a174cbec7271d4bb 100644 GIT binary patch literal 626 zcmZutT}vB56g_u8GTF`AB*u?ujrFs&MJj~&q)0iR^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_PYzvFHJ46T9| zK0q(hz6Y?*XwdiZoqO)N=fLIrcE1YU&-up;IH6O)qv;WNY*#4IEDLr#S{}RUc^uUS z57)_Lm^_Y?tI5qp4u(6u8$TK0ATtZPXNKKM-0vR@MPKy#hLao{#nEWc%jfs$>!H6w zS+wWVCQ9dxtZl7J_9$tC{5Tl02rKH2R86%QzhiHU@v5-25Dj14UmB>grp{PrLzsu3 uadn}S%`B?^r$dU_kJV4}bi8!@rR8Oln)3P%wg|LNnUK1)g49q6hsH0lX(U1b diff --git a/jbmc/regression/jbmc/array_nonconstsize_nonconstaccess/RefMultidimConstsize.java b/jbmc/regression/jbmc/array_nonconstsize_nonconstaccess/RefMultidimConstsize.java index 90692e0392a..fc8fe3bcc2a 100644 --- a/jbmc/regression/jbmc/array_nonconstsize_nonconstaccess/RefMultidimConstsize.java +++ b/jbmc/regression/jbmc/array_nonconstsize_nonconstaccess/RefMultidimConstsize.java @@ -4,5 +4,6 @@ public void f(int y) { int j = 1; a1[j][1] = new A(); a1[j][1].a = 1.0f; + assert a1[1][j] == null; } } diff --git a/jbmc/regression/jbmc/array_nonconstsize_nonconstaccess/RefSingledim.class b/jbmc/regression/jbmc/array_nonconstsize_nonconstaccess/RefSingledim.class index 741443d1e2d27d55e857a922be25eed2a6bea976..e3a1a32b8188d0b379091b9c0eb840bae11b5417 100644 GIT binary patch literal 647 zcmYjNO-~b16g_u7`liD`ryy86R7Lr0sw9S;q|%@yCR7q@OvKf+eUOJ`N@k}15qB(H z7!$UBL`WdY&V@h85aWG=fSKgJdH0-q?m6$*pW`0@mN4hSMM>a>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{%?-} literal 544 zcmYjN%Syvg5IvKmO^s2j^-+!W0phb-6n9EN1VN|@Rs?Z%+om-1O2Y^*fIEZ4{#)tz0!yOEsjZqsZL3BL`gJxD>&dwbQ ztj&7K7xd(U(BHj0EBK8ARj9Gkm#Y_5?NBuWUALQ7^CY+sbm#W{ay|$vHNO;`tqG(o zuxGdDj&mEjs`6|L47E&ycJErym2axz>5e*Yso6*foP7PVQS`S0ZQ1)@b*ZYZlnWa% zify+^DmIc)@O$? z+G+|qd3XN+%w4RwEP5C<`56{pig-6jd$C*0c<(TFJnIfID|?TKnN6qOU>v=`%%@W; z?h~x^gFKL8LfcHYWK2ejvQZ>BS(4QVji+e1K+8qi=`mKh!2o%2^fGp19DT$a#3tH3 ez0Kc{`qodJkOA_|ZzOFDenaGoG{F$t29m$8G*TY` diff --git a/jbmc/regression/jbmc/array_nonconstsize_nonconstaccess/RefSingledim.java b/jbmc/regression/jbmc/array_nonconstsize_nonconstaccess/RefSingledim.java index 1237623d6f5..4e3a081738f 100644 --- a/jbmc/regression/jbmc/array_nonconstsize_nonconstaccess/RefSingledim.java +++ b/jbmc/regression/jbmc/array_nonconstsize_nonconstaccess/RefSingledim.java @@ -1,7 +1,8 @@ public class RefSingledim { public A[] f(int y) { + A[] a1 = null; if (y > 0 && y < 5) { - A[] a1 = new A[y]; + a1 = new A[y]; int j; if (y > 1) { j = 1; @@ -10,9 +11,8 @@ public A[] f(int y) { } a1[j] = new A(); a1[j].a = 1.0f; - return a1; - } else { - return null; } + assert a1 == null; + return a1; } } 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 98169774c6f..f1cd44420c8 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,9 +1,6 @@ CORE FloatMultidim1.class ---function FloatMultidim1.f --cover location --unwind 3 -\d+ of \d+ covered -^EXIT=0$ +--function FloatMultidim1.f --unwind 3 +^EXIT=10$ ^SIGNAL=0$ -y=1$ -y=[2-4]$ -y=([05-9]|[1-9][0-9]+|-[1-9][0-9]*)$ +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 9f1c5d4581b..09f87e5d867 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,8 +1,6 @@ CORE FloatMultidim2.class ---function FloatMultidim2.f --cover location --unwind 3 -^EXIT=0$ +--function FloatMultidim2.f --unwind 3 +^EXIT=10$ ^SIGNAL=0$ -y=1$ -y=[2-4]$ -y=([05-9]|[1-9][0-9]+|-[1-9][0-9]*)$ +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 c4a07a7c56b..0ff8489c7d4 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,9 +1,6 @@ CORE RefMultidim1.class ---function RefMultidim1.f --cover location --unwind 3 -\d+ of \d+ covered -^EXIT=0$ +--function RefMultidim1.f --unwind 3 +^EXIT=10$ ^SIGNAL=0$ -y=1$ -y=[2-4]$ -y=([05-9]|[1-9][0-9]+|-[1-9][0-9]*)$ +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 1f46e69a206..ee16addfad0 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,9 +1,6 @@ CORE RefMultidim2.class ---function RefMultidim2.f --cover location --unwind 3 -\d+ of \d+ covered -^EXIT=0$ +--function RefMultidim2.f --unwind 3 +^EXIT=10$ ^SIGNAL=0$ -y=1$ -y=[2-4]$ -y=([05-9]|[1-9][0-9]+|-[1-9][0-9]*)$ +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 eeb64c3e6b1..c054f7ad4ef 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.class ---function RefMultidimConstsize.f --cover location --unwind 3 -^EXIT=0$ +--function RefMultidimConstsize.f --unwind 3 +^EXIT=10$ ^SIGNAL=0$ -y=-*[0-9]+$ +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 84db685c705..6276db8f31e 100644 --- a/jbmc/regression/jbmc/array_nonconstsize_nonconstaccess/test_ref_singledim.desc +++ b/jbmc/regression/jbmc/array_nonconstsize_nonconstaccess/test_ref_singledim.desc @@ -1,8 +1,6 @@ CORE RefSingledim.class ---function RefSingledim.f --cover location --unwind 3 -^EXIT=0$ +--function RefSingledim.f --unwind 3 +^EXIT=10$ ^SIGNAL=0$ -y=1$ -y=[2-4]$ -y=([05-9]|[1-9][0-9]+|-[1-9][0-9]*)$ +assertion at file RefSingledim.java line 15 .*: FAILURE diff --git a/jbmc/regression/jbmc/dynamic-multi-dimensional-array/TestClass.class b/jbmc/regression/jbmc/dynamic-multi-dimensional-array/TestClass.class index 66e0d0732425724aad3f598846515a0603e8f0c3..0db5253f48997459ee1b10bae07ae80fb698962d 100644 GIT binary patch literal 576 zcmYLFO)mpc6g_XgUOSyuTU1qjB@#uVB9;h>MB*btB-+)qePkFNnVI@0HWC{fYa}Ej ztZe)z;=W1M=H2_wJ@=gR-q+9TJAeg@n}{RFF`%uPpq3-gF=#@UV8O%?iX6iXy%Tm2 z2tRbZRByDTp$Ni?OU|=r_LXhHLXv!HwM`2q5)63>mtDJc zT3-E&x8eJq&k*nKa*S9Q#TY~SpT1W=6OE8^{zH)wL#`V#_5OR z^m8noml3E_!DKEvQ*;}q%BbqoFJKRnh#oqP2&7aREb1KD2w#hp^<@384SWXa)@D;tg%cJ}+{;}gIswmej@?!dRMJix(*gH3^bo{rPa{(@nI=EdR8iRqiS|3W_N lf|ndxmoI2iT8r+^6VV{iU+bX-pRz86SIG1$R~a#|_6z5sIxGMH diff --git a/jbmc/regression/jbmc/dynamic-multi-dimensional-array/TestClass.java b/jbmc/regression/jbmc/dynamic-multi-dimensional-array/TestClass.java index 16d680bd804..66051d5fc3b 100644 --- a/jbmc/regression/jbmc/dynamic-multi-dimensional-array/TestClass.java +++ b/jbmc/regression/jbmc/dynamic-multi-dimensional-array/TestClass.java @@ -1,7 +1,10 @@ public class TestClass { public static void f(int y) { + if(y < 1) + return; float[][] a1 = new float[y][3]; int j = 0; a1[j][0] = 34.5f; + assert a1[0][j] > 0; } } diff --git a/jbmc/regression/jbmc/dynamic-multi-dimensional-array/test.desc b/jbmc/regression/jbmc/dynamic-multi-dimensional-array/test.desc index a4220527596..73caffc0a7d 100644 --- a/jbmc/regression/jbmc/dynamic-multi-dimensional-array/test.desc +++ b/jbmc/regression/jbmc/dynamic-multi-dimensional-array/test.desc @@ -1,5 +1,8 @@ CORE TestClass.class ---function TestClass.f --cover location --unwind 2 +--function TestClass.f --unwind 2 ^EXIT=0$ ^SIGNAL=0$ +-- +-- +Tests that there is no crash. diff --git a/jbmc/regression/jbmc/enum_switch/com/diffblue/regression/Foo$1.class b/jbmc/regression/jbmc/enum_switch/com/diffblue/regression/Foo$1.class index 56f0ef4b05aa42166704353dff4f4d8b10d096fe..b9f700ea97dec8b8a6d3c85e6d00801ed04a3578 100644 GIT binary patch delta 199 zcmcb`x|h}P)W2Q(7#J8#7__+<#2Cam88{duIDsrl5Lb$wK^nx70THt7407xY3KI=u z1$l!@5|gui6AMBTlX6mliY9K+kx*o3P~u@wW>Dc_;9}tBVNhjI<6%%|(3to`o_E~NPB1Vt2mvLS7=#%_fHVt( SD3Fu~VlJRI4j|1SzySdHg%`m9 delta 261 zcmdnXdW+TY)W2Q(7#J8#7<9N8#2F+w88{duIe{!G5LcR=K?cN;1rc)W4D##@iW3cE z)r5TVlM{2o5{ohulX6l+Km;QLZ*WOsa<*?`0hkZeIdQ&@lM*|FG7p0agDMXL7XvpB zgBpW64}%7SCL@DXR$^JAeokUuy1rk2aA|UeTV`rbifd6(ei09Y7D$;kgE}LF>|}pN z>B$<5pBURFOEX0UFf;H2oy*3+2qp!9Bohz|f-ze-JA)8|FPvatW)KD|5MdAn(ku*O RKvDsSxq#X^fHZ>u2LQz+DQ5rx diff --git a/jbmc/regression/jbmc/enum_switch/com/diffblue/regression/Foo.class b/jbmc/regression/jbmc/enum_switch/com/diffblue/regression/Foo.class index c7dfc05289a441e993bc6fcfff4dd5432d7c8953..5373625244fd5f7f119dae146ed0cc66d2b6c8e6 100644 GIT binary patch literal 864 zcmaJicYwW7|fCiz6Xc470SZVbkQnWs8b|>xD&92OD6#q*9 zfFOObVhalTDEOnqJKLs_LS>kbJ9FmDIrq-*Ki_@;SVGG}9+f;ST(K~N**pwfHBhyn zp<-ap!aS}Ss2RA3~)s2V3aa+;!i%HZGuKV*!qV8#Zp@mJJ(4hKf9G zhiy zexfZrr7md{>NC`v)bAZY-9zC!v{y&af2wrj-&i{n>t|wfpEz=vnkIc*l1Qp_)M4Td zS-Oh?I%Meynb{;eFA3QvwHFClKwhsES=I=C>D28~CK8yKG!9|z!B9U!RlY!#&X3<3 aIhQ;da`r>26sEJ|%R~&4!ZJB1n|}c?gR?vU delta 406 zcmXX=O-sX25S&f&lC-8;Tdi&SVd_a*sS4ioCJ2I_6mK44DOfCxGzE{IdagnI6OxM_ z6g+qp)F0t55htk+cJ}S=?9Bd{UuygF_w60P4%V_zC}m(`C5tjD7F-Ke3pIgrI2`sy z`vX4=dtr3msuzxeu0J^QM}7Zd&^t{)V2m&Op`ad3E5<<(>_(H06861l>g5Hwld<2u zI`*$qdi3oUZDbtO(Xg=Uz(Z3|jqb`icklP);TBC8JSlk^1Y{GltTvg2S+!mvPw9A$ zXr@ga4*$-KfE?yo2^NqiCd(6wY0O*g4=6o;hSq+8-g#t;HzZs@XSg?n8lz#vDmG&~ zP6vsRODnn)O|0{-7KJxx*`ZltUYZ&Fo6`!5C{Vb_nFVDwMTC?kmKv7X0tF-$Mc)1c Dk5n{i diff --git a/jbmc/regression/jbmc/enum_switch/com/diffblue/regression/Foo.java b/jbmc/regression/jbmc/enum_switch/com/diffblue/regression/Foo.java index af6f1bfdcf0..b3c590686a6 100644 --- a/jbmc/regression/jbmc/enum_switch/com/diffblue/regression/Foo.java +++ b/jbmc/regression/jbmc/enum_switch/com/diffblue/regression/Foo.java @@ -5,12 +5,16 @@ public int foo(MyEnum e) { if (e == null) return 0; switch (e) { case A: + assert false; return 1; case B: + assert false; return 2; case C: + assert false; return 3; } + assert false; return 5; } } diff --git a/jbmc/regression/jbmc/enum_switch/test.desc b/jbmc/regression/jbmc/enum_switch/test.desc index f525e3e15d4..6001b0456fb 100644 --- a/jbmc/regression/jbmc/enum_switch/test.desc +++ b/jbmc/regression/jbmc/enum_switch/test.desc @@ -1,10 +1,10 @@ CORE symex-driven-lazy-loading-expected-failure com/diffblue/regression/Foo.class ---trace --cover location --depth 1024 --java-max-vla-length 16 --refine-strings --max-nondet-string-length 20 --string-printable --unwind 10 --function "com.diffblue.regression.Foo.foo" --java-unwind-enum-static -line 8.*SATISFIED -line 10.*SATISFIED -line 12.*SATISFIED -line 14.*SATISFIED -^EXIT=0$ +--trace --depth 1024 --java-max-vla-length 16 --refine-strings --max-nondet-string-length 20 --string-printable --unwind 10 --function "com.diffblue.regression.Foo.foo" --java-unwind-enum-static +assertion at file com/diffblue/regression/Foo.java line 8 .*: FAILURE +assertion at file com/diffblue/regression/Foo.java line 11 .*: FAILURE +assertion at file com/diffblue/regression/Foo.java line 14 .*: FAILURE +assertion at file com/diffblue/regression/Foo.java line 17 .*: FAILURE +^EXIT=10$ ^SIGNAL=0$ -- diff --git a/jbmc/regression/jbmc/enum_values_clone/com/diffblue/regression/EnumIter.class b/jbmc/regression/jbmc/enum_values_clone/com/diffblue/regression/EnumIter.class index e977adcf00c9274a706a504a980af2dbb92f6807..6e778a9c7ac39e86c23965797106686b24b1821e 100644 GIT binary patch literal 713 zcma)3!EVz)5PcKd*~E2dnnDQBmZoh=LM1Gr-Y5uEic~3uLo1|~3y!_1+&VT|+m-m0 zUN~|Fq!xh$cm4^)tVNO&2(2_bJNx#{+c!Ucefb7p6FnPMG;Lf*ONSd(2;3C7Wy3;K zV8O;BmIQ7S=GVM5l`0F9IDHzX-XM|zfsP2}tuPL=M+BqWdr2_2lRy$?`(Z4f=c9pC z2O7-SA)&UPdH(61_ok=`EE6hQe)NaH-cNGn%V(j6*LLE3w3|tF@5DRv95|>6v>mKq z)xjD%4s6U2TKd+Fy!hCCG8VX_RH6vWell`{a5x-9xpb90Rx(XlzdL3YSa)y-T|#}z z@?vlz{fy9l)&JZ3y|Gva+gh<%G!?De?l{m zX{cl{`70Zm<$S^BAEC|TtMXu}-qP-HW`MMF9IxST2es&gv8B zAwM;^vi=#R{)Tn`0>(yJ$JY-(!aPTPq4EwhUtt|yqWoQRl?tu~OwLVS78=alVM%jb wse*o@BhcW9V}8HN*uf=Md(5n8qiVQ^v76&0?YCJl21>S~R@&8v($S?f?J) delta 330 zcmXX=yH3ME5S+EoHaNx!#^D+41R6*RBt!@FShz$8L4!dcA|)X4sQCuV;xA}u08yle z??B=&5OWuHb+dc3JEQ${Mk@XK{TKn*Lh8do)5k34G|YQg@UU3!catc;IWGo>#cjVh z8(bV{5UBgB{+(bYFMrzcwm>cg_S$;Jt`Kxi@+y<0#({nPFeI6kPie!2=V2*83(El# zgyr{YRhMS9Cr6LyK=A?{76e=+PVl$EDy&ZT4f0~flSJ2$7JT->cmXwbI;Iek(c)v+ zOdx)TmG_*@SJ*vQ8 BCTIWv diff --git a/jbmc/regression/jbmc/enum_values_clone/com/diffblue/regression/EnumIter.java b/jbmc/regression/jbmc/enum_values_clone/com/diffblue/regression/EnumIter.java index bc5d1f617b6..341ad8a6ee8 100644 --- a/jbmc/regression/jbmc/enum_values_clone/com/diffblue/regression/EnumIter.java +++ b/jbmc/regression/jbmc/enum_values_clone/com/diffblue/regression/EnumIter.java @@ -1,8 +1,8 @@ package com.diffblue.regression; public class EnumIter { - int f() { + void f() { MyEnum[] a = MyEnum.values(); int num = a[2].ordinal() + a[3].ordinal(); - return num ; + assert num == 5; } } diff --git a/jbmc/regression/jbmc/enum_values_clone/test.desc b/jbmc/regression/jbmc/enum_values_clone/test.desc index 7009afb0ed1..3d6fc869747 100644 --- a/jbmc/regression/jbmc/enum_values_clone/test.desc +++ b/jbmc/regression/jbmc/enum_values_clone/test.desc @@ -1,7 +1,6 @@ CORE symex-driven-lazy-loading-expected-failure com/diffblue/regression/EnumIter.class ---trace --cover location --depth 1024 --java-max-vla-length 16 --refine-strings --max-nondet-string-length 20 --string-printable --unwind 2 --function "com.diffblue.regression.EnumIter.f" --java-unwind-enum-static -\d+ of \d+ covered \(100\.0%\) +--java-max-vla-length 16 --max-nondet-string-length 20 --string-printable --unwind 2 --function "com.diffblue.regression.EnumIter.f" --java-unwind-enum-static --cp `../../../../scripts/format_classpath.sh . ../../../src/java_bytecode/library/core-models.jar` ^EXIT=0$ ^SIGNAL=0$ -- diff --git a/jbmc/regression/jbmc/enum_values_clone_name/com/diffblue/regression/EnumIter.class b/jbmc/regression/jbmc/enum_values_clone_name/com/diffblue/regression/EnumIter.class index 3c7ca188bc99aa4392d2c79d5c4b9a1cf147c53e..f0733f1749d5846974e40c5c988976dcad066693 100644 GIT binary patch literal 946 zcma)4U2hUW6g>mW4qXwPgg$$zXT5-%W z1ojUom5%!;GNh)^y>U^8j?-}%mg}8%pR#vEQMo7#{=v##HTFJ zYsaGQF=Sqs|Aw!;lMH{thPoM+{tcoQpBN;^Wmw7P{v(BA8*OS|GMg(;H4c-J0M+Pr zg-xHgkv;!>9x-Yw0mEKrtXLIqeZwL_^S^Tp+pwFXp@>Zr?^`rE3=0k6nvQ5pI!>eD z`Sd_zbA${HV2p;9#Z&Ub$O?kV52rmzw=|uM&d}N^*asPidD_*1GeFkDB-AEokUTq| z5h$M_`05l&KD5M~dSj!nicay*!A`qwx)i& zW_QP)2(LvHh<@l_Ng$~4UGPX~bdzIpv<`s=$&AVhiR6J=d&cE>5_$evAidVS#=VD^?S>iEZqdXu(bnsaYW8rPB??=+?dH4}C9AUZ|Ipl#?4y z&GXykQ9!bb(PZWFB%WIP1N4?&Ta0t*Qo#~)Gc#Zrc~-y*Y~ILlkH4(&tUu?R&MOlI cGHj$v6)Lo}pqQEd3sh85z$#Y|*3wMz4>M7h6lv=Z3W{1J%O10aaBNVHrx$?RLkkPW;pb10gX_tTqioaWCnrlhmPk4+fHD% z`?e(@_5>0&$92LwSxU=q$g<^GJeg@auKjX2Xxsj-Y-XYBc~sF#Qbu;BTcO!`|H3>N zHR!S;)gqdK>9_*<(!1uq`N6FAO}AHVg}&qVqI$B{>5p_5YP;*}&1S9Ae6~^Fs8962 zYVX^fknZ)CH}pI9jw6j|4R=Ly8pvVRfPu7uEM^3XW2L8O!#?+Y&)0C@zzV7y*0Q>R z)z$F8z$zXJC=FM`BZIL&7RZhXPNgqEtxrK{515lT38=)rlYS+ zwkXr!yGo1+alOQ^dG3OHynF)jg)g+iH4%Yw&7(jv*}B7B(iSVfkt|ofK{-O~5K}*( zzCA(wmprXRr*jkmji}HgI|W)P5>cU~(j!BcS-FC%RFK@8JSlAyj*!S{$4LHfgc6r6QjJ9eG4BqV%8Y57PKXoQ4>)JBm2iChdta?}f_P2vQ%i5)o(qCX2H zK;poW13wBeYa5zK9K8E>=6Pn`?yuk9e*k!j0~;ppSTL|-;VyQI*t2mD_f0%7@lc@P ze|#dKyS?y8!197gD3fLE3z&pD%`Q=+6NEw1Wp88uguO4L5&11Q2>mz9*}#wcaxf)Q zaigJ}p2#>*=N#0N_rXG-zRsP`|MHfy>GzM6kv@(hhA|r|jj}3vi5#B2mh)W9R*VXj z=9tMKq;lh(dn!N3_Ed(GwwJ^~ILUY!Pv~6z4=u3M=^q}tZl~qGpmlde;dpTB4-=-b zy=WN^{a1mS&FqB-%Ef_$l7k{F6AcIZX!3qWqw!)iHqmnM2#*D{9&>G9gvun>An$yU z_%mK4l~PKHBISJYpewSH#(o$;G+YAACq#oS!vir zfi(xSrIp+nca6K<`iWw* z^#z*J)KkqewLuM?Q7i^g+V!kE*XDnDSmkoTDVL1fq+6Xehp_UAu2AeMu8~jyo>5TE lV|_-UqJPDP^4C&-JM}8jp}aDeh3mMH_GA}y6SvaS?LWPFkmvva diff --git a/jbmc/regression/jbmc/generic_class_bound1/Gn.java b/jbmc/regression/jbmc/generic_class_bound1/Gn.java index 5dfbf4da153..8b48f7742cf 100644 --- a/jbmc/regression/jbmc/generic_class_bound1/Gn.java +++ b/jbmc/regression/jbmc/generic_class_bound1/Gn.java @@ -7,9 +7,11 @@ public class Gn>{ Gn ex1; public void foo1(Gn ex1){ if(ex1 != null) - this.ex1 = ex1; + this.ex1 = ex1; + assert false; } public static void main(String[] args) { System.out.println("ddfsdf"); + assert false; } } diff --git a/jbmc/regression/jbmc/generic_class_bound1/test.desc b/jbmc/regression/jbmc/generic_class_bound1/test.desc index 6f623851472..e7de31a26cd 100644 --- a/jbmc/regression/jbmc/generic_class_bound1/test.desc +++ b/jbmc/regression/jbmc/generic_class_bound1/test.desc @@ -1,12 +1,10 @@ CORE symex-driven-lazy-loading-expected-failure Gn.class ---cover location --no-lazy-methods --no-refine-strings -^EXIT=0$ +--no-lazy-methods --no-refine-strings +^EXIT=10$ ^SIGNAL=0$ -.*file Gn.java line 6 function java::Gn.\:\(\)V bytecode-index 1 block .: FAILED -.*file Gn.java line 9 function java::Gn.foo1:\(LGn;\)V bytecode-index 1 block .: FAILED -.*file Gn.java line 10 function java::Gn.foo1:\(LGn;\)V bytecode-index 4 block .: FAILED -.*file Gn.java line 13 function java::Gn.main:\(\[Ljava/lang/String;\)V bytecode-index 2 block .: SATISFIED +.*file Gn.java line 11 function java::Gn.foo1:\(LGn;\)V.*SUCCESS +.*file Gn.java line 15 function java::Gn.main:\(\[Ljava/lang/String;\)V.*FAILURE -- -- This fails under symex-driven lazy loading because the FAILED blocks occur in functions that are unreachable diff --git a/jbmc/regression/jbmc-cover/generics/AbstractImpl.class b/jbmc/regression/jbmc/generics/AbstractImpl.class similarity index 100% rename from jbmc/regression/jbmc-cover/generics/AbstractImpl.class rename to jbmc/regression/jbmc/generics/AbstractImpl.class diff --git a/jbmc/regression/jbmc-cover/generics/AbstractInt.class b/jbmc/regression/jbmc/generics/AbstractInt.class similarity index 100% rename from jbmc/regression/jbmc-cover/generics/AbstractInt.class rename to jbmc/regression/jbmc/generics/AbstractInt.class diff --git a/jbmc/regression/jbmc-cover/generics/AbstractTest$ClassA.class b/jbmc/regression/jbmc/generics/AbstractTest$ClassA.class similarity index 87% rename from jbmc/regression/jbmc-cover/generics/AbstractTest$ClassA.class rename to jbmc/regression/jbmc/generics/AbstractTest$ClassA.class index b22a6b21506144982d0966e1a876aafac73a7b35..f98494fed705ee51ca0bac5a79285f1e88910db3 100644 GIT binary patch delta 35 ncmcc1beCy^6QeX20}}%;0|SucV-Nw-Tnvm1%nX7I!VC-mVLbyp delta 35 ncmcc1beCy^6QeXY0}}%;0|SucV-Nw-Tnvm1%nX7I!VC-mVORq_ diff --git a/jbmc/regression/jbmc-cover/generics/AbstractTest$ClassB.class b/jbmc/regression/jbmc/generics/AbstractTest$ClassB.class similarity index 79% rename from jbmc/regression/jbmc-cover/generics/AbstractTest$ClassB.class rename to jbmc/regression/jbmc/generics/AbstractTest$ClassB.class index bd168a7012123dd6898bff0d1ba784259ce2d253..b060b10df5a0c1220527c609c7183ef3b7af014b 100644 GIT binary patch delta 41 tcmZ3$ynuN_6eA<|a^x7yyR_1Q!4R delta 41 tcmZ3$ynuN_6eAa^x7yySs1Q`GT diff --git a/jbmc/regression/jbmc-cover/generics/AbstractTest$Dummy.class b/jbmc/regression/jbmc/generics/AbstractTest$Dummy.class similarity index 87% rename from jbmc/regression/jbmc-cover/generics/AbstractTest$Dummy.class rename to jbmc/regression/jbmc/generics/AbstractTest$Dummy.class index 76f7bb6167908438120d4013d98093af1a0ea6e6..020090a3d4842ca3e9a67beab1386ae23ed150cb 100644 GIT binary patch delta 13 Ucmcb`bc<<&JtHIMWCunm03b61p#T5? delta 13 Ucmcb`bc<<&JtHI6WCunm03bL6q5uE@ diff --git a/jbmc/regression/jbmc/generics/AbstractTest.class b/jbmc/regression/jbmc/generics/AbstractTest.class new file mode 100644 index 0000000000000000000000000000000000000000..313c1e6edf732c4475ea558036fa8795fd30e26f GIT binary patch literal 941 zcmZuwTTc@~6#k~W+i91@-e|1|Dp0YdmU;m+X(hHGNt1#PB_{H=Z70oQyCu6@6aRoe zg2ZQEcu^BbBvIc?{7q^+v$91DFXzmh^PTV9W`6ws`~|=Y9_cW!z>(7t!h#gHITm$j zxD$nrJV!xCL?V`S6mgfM#1P)-o32}DFdDWk9RDUg87&y$N$)iKAeaJ`)0N3C*+ zv0hpCGeoML{#nI(YdCT`V#|{CC4yQc&+@+c+BA?xh6WTkWRV8$;XaKcu$?EZ8+d?+ z22z+}$jbO~-?V$>S}?a~jx%)rp_8E;D+X4v#t=V`c;4O@az2+NsWBukq&{1ZLc?X4 z$`_jd(^P1OniX>%9;R+R&p`xZq&QPv-LakEf z>x7C!3I9TxV}@h)C$bDTe4d;1CvJ_~Sn=y6&ZK^fi9>MpJyhirxNPZf(x4?tsv%@N cW#pLi-SbodD7!)q9g}p9k&cs2kWK=B0B!rkaR2}S literal 0 HcmV?d00001 diff --git a/jbmc/regression/jbmc-cover/generics/AbstractTest.java b/jbmc/regression/jbmc/generics/AbstractTest.java similarity index 72% rename from jbmc/regression/jbmc-cover/generics/AbstractTest.java rename to jbmc/regression/jbmc/generics/AbstractTest.java index 5b6049a211c..84e9bbcec34 100644 --- a/jbmc/regression/jbmc-cover/generics/AbstractTest.java +++ b/jbmc/regression/jbmc/generics/AbstractTest.java @@ -13,10 +13,15 @@ class ClassB { int getId() { return id; } } - public int getFromAbstract(AbstractInt arg) { + public int getFromAbstract(AbstractImpl arg) { + if (arg == null) + return -1; AbstractImpl dummy = new AbstractImpl<>(); ClassB b = arg.get(); + if (b == null) + return -1; int i = b.getId(); + assert(i > 0); return i; } } diff --git a/jbmc/regression/jbmc/generics/test.desc b/jbmc/regression/jbmc/generics/test.desc new file mode 100644 index 00000000000..6b2de09b2e4 --- /dev/null +++ b/jbmc/regression/jbmc/generics/test.desc @@ -0,0 +1,6 @@ +CORE +AbstractTest.class +--function AbstractTest.getFromAbstract +^EXIT=10$ +^SIGNAL=0$ +assertion at file AbstractTest.java line 24 .*: FAILURE diff --git a/jbmc/regression/jbmc/generics_recursive_parameters/KeyValue.class b/jbmc/regression/jbmc/generics_recursive_parameters/KeyValue.class index a7920d988fcaf3c390cb899fbff5698729e872f0..87c97a68d9ec91de02c9079e988282f06552aaf7 100644 GIT binary patch delta 81 zcmdnQa+6u~)W2Q(7#J8#7$mtEm>I;_8N}HcBqoZko%sE^fh+?f5Hc{ZYHep=+z4ba YG6(@lHn1Qg0~3(N03?MOM8LEt0JAR(p#T5? delta 164 zcmcb~yop8h)W2Q(7#J8#7-YB@m>DG58Kl@5q$i55)f4i`PfpAUODxJvOv*_O0TGN0 zEF~G4#f%JMsB)DBsS|g<3vpy%1VRP|R;}#}j2nRrW(FZ3$p#i=WDo|jc_0cHL>O3s VJW&)8b|8-ls2W6yF^Gd{2>^(J918#d diff --git a/jbmc/regression/jbmc/generics_recursive_parameters/MutuallyRecursiveGenerics.class b/jbmc/regression/jbmc/generics_recursive_parameters/MutuallyRecursiveGenerics.class index 58e7cc0256ac79b80d38be9adf6e069a22a2efd4..06d26000d4ec9c43b77ed85ac3d918d431b17610 100644 GIT binary patch literal 571 zcmZ`$%SyvQ6g@XhJ8g_wU$xdZxbOjX<5EQNh4=y$L3h)1l+l>VBq{hS{(x&06cltR z_)Q|-1Z`I?X6A72opa9I`TTx)1F(Qe2L+S_1|3)^6(CR+7;=zJ$clquj0lVp`le(U zDii5O5U%M^)_heb&?zCer~@4>5i-*=#{_$|QCEcS9UZ8>_^PJNQPRx4XN1nfNP3sM z@;c?%m5^Wb{9gg*un`+iZRn(ZY&VW#>H9Ya%8N~?n`%=9%4jc~zmQGo!bK&m*uK7ByHH-l4{1}YKF@$qs;f{N zRc{&aqoSA#Jb+V7@CXY$S}K;4NQ^SPI4lTVj7Iq+KC`pWpnC>v!Fw(x1*2lCb&J2m zVrKXi*2yz6I}fmL(LMKpj#p%v$-O56Rw~ey`V^37*9!aga3v4=LPemLQC~}TA+-W} fdc_m+w-ELn?93zVw%A{qL?jE#T~0Fhr(Od;0mW{2 literal 361 zcmZ`!%Sr=55Ufr%SzV)v-a#%c@{P?z59tCycu=yA$xUJP9810r@Dg zCk7ED4b$CKQ&rH*ug?X5bL=N*VlPHFMvu_GG=-_J2+gD82_d>Jr%dQ(rr>-3nzI|L z+zNA$m0H<}awgz48PzYQA`G%SUwdWk+aqi5Dl_L>F4!4eT@dJrkc>+2G~bvIb+}P| zHdAxeL4+2ezfnc#1zl=Y@ti*7GuAbRXvkHe8uBCna+++ZOp@6;`2fAIzGLa_6&Yho f_Rfz0+eicfJHO^rK_Tv+G5KSpwUHz!$alX1Rn$gz diff --git a/jbmc/regression/jbmc/generics_recursive_parameters/MutuallyRecursiveGenerics.java b/jbmc/regression/jbmc/generics_recursive_parameters/MutuallyRecursiveGenerics.java index 1fbdeb644d2..d9492106c67 100644 --- a/jbmc/regression/jbmc/generics_recursive_parameters/MutuallyRecursiveGenerics.java +++ b/jbmc/regression/jbmc/generics_recursive_parameters/MutuallyRecursiveGenerics.java @@ -6,6 +6,7 @@ class KeyValue { } class MutuallyRecursiveGenerics { void f() { - KeyValue example1; + KeyValue example1 = new KeyValue<>(); + assert example1 != null; } } diff --git a/jbmc/regression/jbmc/generics_recursive_parameters/test.desc b/jbmc/regression/jbmc/generics_recursive_parameters/test.desc index 859670558b4..08f1ae52143 100644 --- a/jbmc/regression/jbmc/generics_recursive_parameters/test.desc +++ b/jbmc/regression/jbmc/generics_recursive_parameters/test.desc @@ -1,6 +1,6 @@ CORE MutuallyRecursiveGenerics.class ---cover location --function MutuallyRecursiveGenerics.f +--function MutuallyRecursiveGenerics.f ^EXIT=0$ ^SIGNAL=0$ -- diff --git a/jbmc/regression/jbmc/generics_type_param/GenericFields$SimpleGenericField.class b/jbmc/regression/jbmc/generics_type_param/GenericFields$SimpleGenericField.class index daf2c6ff9b4723df28d0a53bbaa39326b018e644..351f249110be8141a73ef58a1272a8eb330198fb 100644 GIT binary patch delta 557 zcmYLETT2^37(J6sGRbCR5=~=nwVK3M+r}sezLa9I7bseU2tn~>O@^}VHVM0FU;Pal z@WDUes~1pEsEk+Ky2-~2dQ|yXE(pD+1(9I zGjLyQMkBA9uG4mUulo&ASs%rig*0*k@w)S^>#Bxlce~27kVHx#`^ElY*Ic{(x%OuG z%sbEPc=UfzZRI)5_l|N~zQmk`8s_^4Vp}C1ZmqbiCy;3=-|CXiUyW_-RB3ig+k<$uMj-y#|GB`Zg z(!_Zb7_My}x$DT{6^zXb1V5c3bcjUt2C*xI$;j*KG4%j+!pNXt1`(n>A1k5*0`UiV ziO2stPmpfe$FdKlvt;biDwO&j#c%FbDuiK?Wg^ z43H-Y#2`_|jbH{snFx?C%pd}^0;Egz*v-Hkxt)P!1Da|vr~^cS>coI@Obp@- SazL63XgDi_Gy}6N0|Njdlpoaq diff --git a/jbmc/regression/jbmc/generics_type_param/GenericFields.java b/jbmc/regression/jbmc/generics_type_param/GenericFields.java index 3b903ebaa56..59f1ccf8919 100644 --- a/jbmc/regression/jbmc/generics_type_param/GenericFields.java +++ b/jbmc/regression/jbmc/generics_type_param/GenericFields.java @@ -19,7 +19,9 @@ class SimpleGenericField { public void foo() { } SimpleWrapper f(SimpleWrapper s, SimpleWrapper a) { - return new SimpleWrapper<>(); + SimpleWrapper r = new SimpleWrapper<>(); + assert r != null; + return r; } } } diff --git a/jbmc/regression/jbmc/generics_type_param/test.desc b/jbmc/regression/jbmc/generics_type_param/test.desc index 4b4bcca0974..ef3971e4559 100644 --- a/jbmc/regression/jbmc/generics_type_param/test.desc +++ b/jbmc/regression/jbmc/generics_type_param/test.desc @@ -1,6 +1,6 @@ CORE GenericFields$SimpleGenericField.class ---cover location --function GenericFields\$SimpleGenericField.foo --verbosity 10 +--function GenericFields\$SimpleGenericField.foo --verbosity 10 ^EXIT=0$ ^SIGNAL=0$ Reading class AWrapper diff --git a/jbmc/regression/jbmc/integer_without_simplify1/test.desc b/jbmc/regression/jbmc/integer_without_simplify1/test.desc index 284277c7b4a..b6f6e0dc0de 100644 --- a/jbmc/regression/jbmc/integer_without_simplify1/test.desc +++ b/jbmc/regression/jbmc/integer_without_simplify1/test.desc @@ -1,6 +1,6 @@ CORE test.class ---no-simplify --function test.f --cover location +--no-simplify --function test.f ^EXIT=0$ ^SIGNAL=0$ -- diff --git a/jbmc/regression/jbmc/internal1/com/diffblue/javatest/nestedobjects/subpackage/Order.class b/jbmc/regression/jbmc/internal1/com/diffblue/javatest/nestedobjects/subpackage/Order.class index 9c810453dec2363c6c121eec0729834933080b60..af8d3a3d7c4b26d31571813974fdb8ac2cecd5f5 100644 GIT binary patch literal 964 zcmb7COK;Oa5dPMWxN+PzO(6sbP16=gf`l&tAyE*hPzfo}Ls2ETZR~Bk#fdAg1N@f$ z0WQ7pY9)~11`@vsA!Z%Z9604NyED7~>1JpYp>T-%%nRpWkUs%aJ*6 zYlq^kR4K`vSr4Mzth*hLl0a-qZOzT(+|T6I&85yK z7(Zc~$JQ~WCN#txtsriP*o(wGfhy%t7qYvoNEkI-%rW1PWZl^8oWQ)-x$zms2Utg_ zXpSE!eTDtv6ov2g2~&kUfn?bv%q6G>foZnoF;LD%kl7>{-K*mgDKelHkk#L4&=0`n mv#E45TfjoaIl;^k9P1q{^CPVPC!`^47~TUtiaI3*uKWeDK*pH> delta 353 zcmYL^y-EW?6ot>7bu#YmB*vc@qZ^FvrdR~Q%EHE0u(Vqx1cF$JZF~Tmu&4o_!~KSnN# z2T7W%2t68b9&2b9OF5nj+LQb~&u;SDadv(+8C~DufN@KvaM8>vV8tvoVwaUSfKA^Z zPdqS)sSO^h)l+?0TQt#PC;A*!!)M&p7pKoKpT)w&Qw_Hm1PzX;kgt8!WfMoFHkqQ8|j3M8QSE|;L4;A;EJ&0 z1>Cq%6G=4Dl^fr}*D%p|?j+F7Irp6Wzs~(x`A{4D`uFuau*;55z*4|fmIJPF-IW`L z6%UV_hOUoc$*}6P#x29TFuxjQS#0xUJj$LXS@bH6hl0F3UVkAQ$8YaX>JRqQWR&C& z1%EI;vitG#B#nicB#&*Bk8OYZb@V0*nW1U89kR(C!$!zmwnDb)2`vZcrP1i1H^^-= zItU4A2%YKv@p*`6){d>gE~p(E*v&S}T?gI>$Vv0(z*u>JU38zok3*MD3K| z8)ol}`VU7f71VYCGCI{&-J`4ief7Sihz8}qcw)Hxhs6f%g0!H(&PAZz!Wm}gyf65t dn96%9<HJ;X^?DTR;R4U2`?mH$QTSO@?B delta 249 zcmW-bJx&5q6otP#z&vK=smPz84# list) int i = 0; for(String s : list) i++; + + assert false; } } diff --git a/jbmc/regression/jbmc/iterator1/test.desc b/jbmc/regression/jbmc/iterator1/test.desc index 3e8c6068f6a..550f9ad5e95 100644 --- a/jbmc/regression/jbmc/iterator1/test.desc +++ b/jbmc/regression/jbmc/iterator1/test.desc @@ -1,8 +1,10 @@ CORE iterator1.class ---cover location --unwind 3 --function iterator1.f -^EXIT=0$ +--unwind 3 --function iterator1.f +^EXIT=10$ ^SIGNAL=0$ -^.*SATISFIED$ +^.*FAILURE -- ^warning: ignoring +-- +Tests that end of function is reachable. diff --git a/jbmc/regression/jbmc/iterator2/iterator2.class b/jbmc/regression/jbmc/iterator2/iterator2.class index 45d6532dfff7da483fe0cc226eb20c6900204a97..d5dddf70c78aa6f523449558b564cbd32154c233 100644 GIT binary patch delta 467 zcmYL_OG_J36vuyeOnN7iYfXH_)EG4yAC0Z?k)?=YUD$0!sk^C}mXVOa%vflbegZ>w zeu2_uTd1I-dq0p+!N*C&x;f|k&*lF(_h0p!BOgT(5qj|09E4pFm1(DyVhwuE*{Z#X+3borTZN*ALZXUi**vor0zwSpX z&8xA29#V!`-e^jOx6B#J%s20g6+<^K71@3Ft6Q$Q^)KbMC*_SGXatIcA9;ZrHG)OW zf?<)lR#|=DRP;P^)@zbSk*Rv2A9&UO5+5QrItVGqAx5rMschR$rY?j}N@}`wsWOFL z*}V|-_|iu|7HL7}(rxLVTi0qQ_Zxjo@(laq35m;JvbSh6$FWu3!>0C3AsdH?_b delta 239 zcmW-Zy-osA5QV>c5k__|KZ2~n%EHP@VM&M&VP|5L*22Qdgi!GWR77&0f`-JF!Uy1u zAdxW36lczvIp_Syy7;&|ZvTKW!+=YokRmrBx3qKU2(fS{bcJN~_IlCN!)o*F3npom z2^@V=q35_~;K+FJPbPDQ^4IKh`Z4>Sj{MThBT_`$^ReicKr!?$HcFk|N~)lsSfQ$p zP}N#@o|yQBeXsl~v*g|c@dw)-)s)ASjyPk4`ag+qrDRWhz?y)@Invb9>oaSe0B)%r AxBvhE diff --git a/jbmc/regression/jbmc/iterator2/iterator2.java b/jbmc/regression/jbmc/iterator2/iterator2.java index 16b40e48dd3..7b8369b4806 100644 --- a/jbmc/regression/jbmc/iterator2/iterator2.java +++ b/jbmc/regression/jbmc/iterator2/iterator2.java @@ -11,5 +11,6 @@ public void f(List> list) i++; } for(j=0;jx~w6iBMp_Ia%NpvbEMJN3 zsFJ`y?i6+EYLppeWxfY?A1@+HF_jEsVFWp<`32>BMW^avgU T{rwvN#lIAAeIv#$CbIDh7mr08 delta 215 zcmey!@{dXM)W2Q(7#J8#7zDT&m>GE48Ti;4_$NAg)^i2tmlh?bx@G31GBR+6q!yRx zWhIs+@-VP4ure~RfCLyB1VBRiIf;4c`u<5-smUb_iVRFZb3lNJ0jP|D6-crHd9py7 z5lFLYZD(NI2xKraumedpupmf+gMkys1}U8l)XKsFWH?W*WOU?XS_5PuPXDNP_F diff --git a/jbmc/regression/jbmc/json_trace1/Test.java b/jbmc/regression/jbmc/json_trace1/Test.java index 79cb55bfdf9..956ed099a7a 100644 --- a/jbmc/regression/jbmc/json_trace1/Test.java +++ b/jbmc/regression/jbmc/json_trace1/Test.java @@ -16,6 +16,7 @@ byte main(byte[] a) { } } + assert a[0] == 0; return -1; } } diff --git a/jbmc/regression/jbmc/json_trace1/test.desc b/jbmc/regression/jbmc/json_trace1/test.desc index d0f9b27b618..52971e9fbd3 100644 --- a/jbmc/regression/jbmc/json_trace1/test.desc +++ b/jbmc/regression/jbmc/json_trace1/test.desc @@ -1,7 +1,9 @@ CORE Test.class ---cover location --trace --json-ui --function Test.main -^EXIT=0$ +--trace --json-ui --function Test.main +^EXIT=10$ ^SIGNAL=0$ -- ^warning: ignoring +-- +Tests that it doesn't crash. \ No newline at end of file diff --git a/jbmc/regression/jbmc/json_trace3/Test.class b/jbmc/regression/jbmc/json_trace3/Test.class index 86426242aaaa8cdeff7edab3792771ba00554c50..49de108337401bbbf7b1299e6f64e579b7899ecd 100644 GIT binary patch literal 573 zcmYLGO)mpc6g_u7bvh_jN_|8kQnSzvR*euJ3-Of@30BkgMTT}NGgE5|{()7OHr6E} zA*rRr&#@H2eNAaz^6q>0o_p>&@4bINHv!CH+=7XL7<8me3|dezU}DHZ8p9?=2+1io z3`G!mRX<$yLbp&BB?280jJ)T2(IP?3&KwZ5m1;>4dN(~^Y}YCU5$sDa7b>pj6ZGuy zhQxL6MQ-tI%RO(GyYj_yo5Q!D8>kh4sxe(DvA+n>!eo7Y>O~h5}_A}(mxlAi)vh8Pe+*KS26jO zD3O-a`J{rR7~XBZjd3K7y7L5TNFcg-H(E({fFAVnSwb(NLE*UIyg_R?P2-k>n$I}R zTl6@Y%=PXS(cRC-J(N0Yyazwo)1LZGi-e}qwosogUwIqq8^J9JX;XT&@y9ahmM*oisW|WoXy}Z3cqC zjJm66z37hTX%g?zf?|$23Y5VnI_#QcA=~XcY hDi?=&l10?)ZTPHeGn)7+4sD*%?IH86+l3rA#~^ry07B1 z;F*_~TExh}24nDm1)Osdi;Gi>C%%ifRbpTQLIwsdE$yugj9S|nm^K1=j12rhk_|{R cFvtVt1%NaYgCK)Akmdr4GBb!Uh%qn%0HjhFjsO4v delta 190 zcmaFBw2WEm)W2Q(7#J8#800t^m>I;m7+4r2*cqhQ8KfslrAP_+TQge4YbCMM;i zhJXl029}bH%;Je_qxQsC2)TjsObntx9urVr7%a*N LbfqMN5CbCs)eRrN diff --git a/jbmc/regression/jbmc/nondet-static/My$PSInner.class b/jbmc/regression/jbmc/nondet-static/My$PSInner.class index f3432fcb033aa8d0b33ca6c71708db361d65b5bd..681100b4995ccd13ec658fdac3065c5938b47560 100644 GIT binary patch delta 277 zcmX@X-OXKp>ff$?3=9k=3=y0RA`G@5!VW~(g9rx@;Rqs}K!h`haN%MQWpD+t+(3jo z7lQ|bCy3?6&fv|(z{lVN;`o9HKM>&$A_CYM0@)ct7#Wxf3>g_1JwXg35HYcS)8tad z`)r{+3}Fn0lcShq8N(-6Fey*=Wt5yeo9PapECWzI(1EO4+Zi}FPCm#i%xnNuxRzO+ z*$7Bq2hzqsnvq4F*#t;y18GwRv&o@A+8oHQ2htWmdL@hcWDOS4$xm5C8LcM&X4xig X4K$RA!G<9iNOJ+L5CQrlh=CIT^X@Ml delta 395 zcmXYtO-lk%6o%hBGc`F5QK1-ZGX^4J0gjJWGC8Eh)9=y%tsHkdechrOs11OI{%RGn)7+4sD*%?IH86+l3rA#~|rzOeGAjQbQI;m7+4r2*cqhQ8KfslrAP_+TQge4YbCMM;i zhJXl029}bH%;Je_rFnULd@EG~iahi3Qj4r7)+h+durtUqGH@Y8CmxIUH(_7`LIwsd zE$yugj9S|nm^K1=Obq-$l8u28NIEhI07)J&n~On^K?E!>3MR!Egn={{P>z{Fl0k@p F2>=@kAc_D0 diff --git a/jbmc/regression/jbmc/nondet-static/My$PrSInner.class b/jbmc/regression/jbmc/nondet-static/My$PrSInner.class index 2c9413cd7c34cebf2114120d3869bae6e47ad5b3..844bce96d46720e52d4934f2f6dc901a2f8938ec 100644 GIT binary patch delta 285 zcmbQqeVeQP)W2Q(7#J8#7{WOjL>O#9ge{1$0}=Kh!U04$f(R!r22loQ5X%KbxNS1Tq*I^noNBSkPU7 zgTVl(Z3VMBvk{QK1f-3D^dBH?0;JVg)EP}DUtkuQoWvr^Yz`EuVo_(d0MbiL@FgcFEx1`#eG!WBfgfe3dl22lnN5X%!pcyTd! zGx&g5zU&NsTnxMn{vb{OhzJA`K_DU+M1-(2gt9Y)F)}a}7&0<2dV&~6AYx+uCMhAG z{N%)(u*9Ow#H5_m5D>x0z*3TtSv=W~NrsQt$G1`?peWcgFE6#oda^#_6}E65h6o0; z$(&5GjFFSonKUP7G2JoHX8@WE^a`uib_R}(Kn4?oK9FPs3%WBH0NFec1q_Bj|1wPG zVUd_z!z{{ZK3RZ8Wb!f~%L2^00AyK$S-+S?nXMSCCkwHtGunVf{8&U8ZNaPxAj@uY ZAImmzd$3&&48}m33uuD~Fj$NjxBvi;JUsva diff --git a/jbmc/regression/jbmc/nondet-static/My.class b/jbmc/regression/jbmc/nondet-static/My.class index df0cb67c70161275baec59bf5c94bb3bf894336d..c4830d093cfbe90c18946b7c2ab7a33464be745a 100644 GIT binary patch literal 3726 zcma)9X>b%p6#ja8Hj~|KNJz-B350+V69mZx0zp7gG)hb~ih?L^k^vSrn{{?K5D-!D z0>leM6Ym31M1-UYqExBng`ie>miJYKir0V3qR{t-WVgG*5A)-D{rY?T&3oN%XF5ku zzWN$~TJ%|1VIgdx-9p4dhYzz6O~*}Mc;GO^EW~~AA<9mIp_5@H!zv$UqKjcQyK5M3 zW?0K`3&T2wTN!R+SkJJ5;dX{Qypa4D$;y(IB`Zs;Vjw-qdJ=1W1a~sr#c(&nMutrc zn;Gt5*y4p?J;8c{^#tn)))TBJSWmE?z`YFjG2GAa0K7@Ed++J!sbpkTFgw|xv>4?PQ!AN|5Fr2U@9hz_{QlS8nAtW6cbtst7 zop;=M=hQqsz>GSq#fEq`6u^cea?3b>Cmy2bTo{T4Tf%l5rMi&RI)h=t@(N1ZoYT=} z3uMg;MeNHH?Jc%*6-NrB%?L$8@tG7+USBbv@@TURs$qb^S!W#LiUwHdA9fjH8m zFkf>=!fCbVhFHUD=sJgYKp>-`t1Pv_KGz%ALDw1FS1&VzTiej(M+=rwsx9H5A9HcB zAB%9kKw)ZI&mXMuBFE`){J4aJ>KQI&xD50BcnpvG@dTdqqlxFPV7QWrW*%L|a5ckx zhHIEuz@vo>*RlH)7W?ru!!r!eGCYSJe(dDYE{5mXeSt^28D3=A!|)OldwKLS7F*co z$A0wsaRU|$3{TZD&>mcHt3Y;&Xlz+-x5l-p=C~7zET!$Gb4=KcO9b-ij85BYY4%Nt zU^pg_SFZ42JD#8|q6S`wG4x`X zO+Ut5c)8(dKqal5&eI?lD! zbgreob1k(V*&RmzXkFoWk}sbD{gdIK}eaT?I9Eh5~h*m z+ypn*sW@v9`SjB9M8+RPT8`Dwi}Y^f^}^eOtm1BD9D;AbL1et%3%~g!@?9dkn1%|I z=}9p(RG49DDTam$la=0&>;o9ylhm{{K8J(~+@}pM&eoUalAEOTRU@oH)nq`rCY#rt zTI$u9e5xtA$fr>SYAzWXRjB6T*Qh|U!lZ1b7Eq+hW@%KhDx0lQBZrnaTniYbl$fV6 zC2EQJ8Z}zYr9h)f)m#cSYRu3Q16sgXRkm28&QN7XYE;?K5=SWk{Ww!8u|#9WsU?oq zsI$~uN;Rrn&1H;6RSYe0tQIg{l`Ye#vsKwMHEP1p62~b4y_l$!SfMfJs3nfqs7Y!r zXKPfYn#%-@sv272L@l6Nm7SzfHL7f-M%4~2u}TT($7H3%YK@tqmRO@v=c>8XYSdIU zm&qD6ZD@&8w1DZV>{N}aQ)Q=V)M-v}x)LxU$J&v4r_?FTe)m00?_{wZHjP_hlC`iD znOKI=2w@zSV;WY_Hz-Wsi*~w%Lu8c}RP9NUnfyGAEnCRXAtting=!ZEDD@3jm5pe?DhD481fJcoIJZ4nmabp&qFq-j9FXVXpu7V8@>;wi!+2G8;gH;dx8zp5 zEqCD^xfk!sH*r`V!F%#M9FfOxRQ`?kO%FaW1Ng`+#m8nXJ~8X?so99n%tiRzjN%Kk z6JMH}@Rj)hzBYH@8*>l7HQ&H@=3#tqeuE#(DD^l-XA(#2*3wOS!1S3*~Y3TnBD7={|+XCem|5IYxnbhXH* zJ8%(Qe2eMwFw)%+4-Efo`k#jSlkXABDHs?_y(>uce7e~fWakh{vKNxLN%kU${{TD* BF_!=U literal 3011 zcma)8X;f5Y7=GSwfXfVn;wXx!xl*{~f*XoknHC9(Vw#%T03!~J0}ca9D(>Z4X{orE zil(^aaMGKeqd(FX^+#Eqv_(57+m805e)-FK-^+5ppdTIadB1nL&->l`KJ(ps?a_rx z0EXa=0r5Y0_6e~0!svz3RJp~fmZ~UiMw22g+P_SN`X}Z zs|D5wtQA-%uwLL*Cmh1;5N3xkJA~PRN&)6`2%iI0E{4|xHVAAK*d(x7V2i+3f!CcN z;UnQA;UnQA;UnQA;UnQAydm(Wz&3&H0&fYtEwIDI``c+?m)u^pf!&1IoKS9NFz5>r z+?E|5@RpVN$_PeIs3BqGG?v8VG=x;?AOd9)RB4*PV1Xe5LkVrOio6xx0ReBYa6o1- z>?`zzG6;^+1$<5X_>y2**c%Mb@CM3#4xSTPDQ4jUreS0rM`?(Q8LfE8iihgs+#sqn zBwS)RFNO=ma7FY2zb{b0*H(A~jH$hOlTqVK3VejtS^l7Ja`~b>Uue2FFTjzQQU0Jm zJccV$Gkeb%kmnYx8*cW z!6})>L1b6DF%Lz2t9b#h8?*3?8{-8g2uu`sR^T~gy0I7g+}Mu;Ze&YrvcMEcvH& zJ!eMm**pwye!j1)tk=MS18rxJ?xg9?VBHxaPGahRcWxves$VfocZTauy6%h+C$3>< zycylI_STfMHrM1?yKC}zd+5$T`O*9{YYV67f>%zFhGkhDmSurhmNmk*Bc5lUFp1X+ zS?se|tT^k%vMd?4E>VqTSvZzu?O2xOV_8-Z+hn}JzRi~`qO#(wE6cL9*pi5st%G;S z;$Z(JD@%;LlbDl?gt?3{Y-MjGTB)y#`iXr$PSo{2=Mm#Evio%U0I?A`cf;8yAz-at zQ3q`&E?RTkF`5$}YogUTwBBPEC+Nj(^kR?EqPVTrvYp;CQD%}AV;ud$=&tudy>h3Iy+#!OeJy^i&0z|AEXQW7z;;xjnj;6Xicj&? zd`z!F1Z!~_>u?nta04506Ps|GtM6h99$+i}!VWydPCUXcibgfX@u!4`Uv){?OI@*# zQm~)WaDdWrh{obDO~4V#LJdvBQJRlqM?w-Qt*Z9i<>G9U#fI`r6%BOH3{FSsko(P; zrmXpm!=S%;WDWy`WbpLhcDp_N7x#ZHVtL+0^#>lmUFGWum>X3GS9BfXOpL69`yw)C z#h%BgI>d7@!3wsKpkW0)T-}ZniB_V$UEP6$Nmj6BS%L;{BbGfU zzZv4ug;zb%8vR+2X=sOGNW>_#=Z}tLeuH%4kBZKG`^9{%V)>0_+k-jyI}Ky_4WihN PV|1{6iW#HWJ`MT@VySEe diff --git a/jbmc/regression/jbmc/nondet-static/My.java b/jbmc/regression/jbmc/nondet-static/My.java index 6e8d6d86eef..04ffa03b5ee 100644 --- a/jbmc/regression/jbmc/nondet-static/My.java +++ b/jbmc/regression/jbmc/nondet-static/My.java @@ -96,143 +96,143 @@ private static class PrSInner { private static final Integer prf4 = new Integer(4); } - public int field; public My(int i) { + String s = "bla"; - field = i; + if (p1 != 0) - field = 108; // this line can only be covered with nondet-static + assert i == 0; // this line can only be covered with nondet-static if (p2 != 1) - field = 108; // this line can only be covered with nondet-static + assert i == 1; // this line can only be covered with nondet-static if (p3 != 2) - field = 108; // this line can only be covered with nondet-static + assert i == 2; // this line can only be covered with nondet-static if (p4 != 3) - field = 108; // this line can only be covered with nondet-static + assert i == 3; // this line can only be covered with nondet-static if (!p5.equals(5)) - field = 108; // this line can only be covered with nondet-static + assert i == 4; // this line can only be covered with nondet-static if (pf1 != 1) - field = 108; // this line cannot be covered even with nondet-static + assert i == 5; // this line cannot be covered even with nondet-static if (pf2 != 2) - field = 108; // this line cannot be covered even with nondet-static + assert i == 6; // this line cannot be covered even with nondet-static if (pf3 != 3) - field = 108; // this line cannot be covered even with nondet-static + assert i == 7; // this line cannot be covered even with nondet-static if (!pf4.equals(4)) - field = 108; // this line cannot be covered even with nondet-static + assert i == 8; // this line cannot be covered even with nondet-static if (pr1 != 0) - field = 108; // this line can only be covered with nondet-static + assert i == 9; // this line can only be covered with nondet-static if (pr2 != 1) - field = 108; // this line can only be covered with nondet-static + assert i == 10; // this line can only be covered with nondet-static if (pr3 != 2) - field = 108; // this line can only be covered with nondet-static + assert i == 11; // this line can only be covered with nondet-static if (pr4 != 3) - field = 108; // this line can only be covered with nondet-static + assert i == 12; // this line can only be covered with nondet-static if (!pr5.equals(5)) - field = 108; // this line can only be covered with nondet-static + assert i == 13; // this line can only be covered with nondet-static if (prf1 != 1) - field = 108; // this line cannot be covered even with nondet-static + assert i == 14; // this line cannot be covered even with nondet-static if (prf2 != 2) - field = 108; // this line cannot be covered even with nondet-static + assert i == 15; // this line cannot be covered even with nondet-static if (prf3 != 3) - field = 108; // this line cannot be covered even with nondet-static + assert i == 16; // this line cannot be covered even with nondet-static if (!prf4.equals(4)) - field = 108; // this line cannot be covered even with nondet-static + assert i == 17; // this line cannot be covered even with nondet-static if (PInner.pf1 != 1) - field = 108; // this line cannot be covered even with nondet-static + assert i == 19; // this line cannot be covered even with nondet-static if (PInner.prf1 != 1) - field = 108; // this line cannot be covered even with nondet-static + assert i == 20; // this line cannot be covered even with nondet-static if (PSInner.p1 != 0) - field = 108; // this line can only be covered with nondet-static + assert i == 21; // this line can only be covered with nondet-static if (PSInner.p2 != 1) - field = 108; // this line can only be covered with nondet-static + assert i == 22; // this line can only be covered with nondet-static if (PSInner.p3 != 2) - field = 108; // this line can only be covered with nondet-static + assert i == 23; // this line can only be covered with nondet-static if (PSInner.p4 != 3) - field = 108; // this line can only be covered with nondet-static + assert i == 24; // this line can only be covered with nondet-static if (!PSInner.p5.equals(5)) - field = 108; // this line can only be covered with nondet-static + assert i == 25; // this line can only be covered with nondet-static if (PSInner.pf1 != 1) - field = 108; // this line cannot be covered even with nondet-static + assert i == 26; // this line cannot be covered even with nondet-static if (PSInner.pf2 != 2) - field = 108; // this line cannot be covered even with nondet-static + assert i == 27; // this line cannot be covered even with nondet-static if (PSInner.pf3 != 3) - field = 108; // this line cannot be covered even with nondet-static + assert i == 28; // this line cannot be covered even with nondet-static if (!PSInner.pf4.equals(4)) - field = 108; // this line cannot be covered even with nondet-static + assert i == 29; // this line cannot be covered even with nondet-static if (PSInner.pr1 != 0) - field = 108; // this line can only be covered with nondet-static + assert i == 30; // this line can only be covered with nondet-static if (PSInner.pr2 != 1) - field = 108; // this line can only be covered with nondet-static + assert i == 31; // this line can only be covered with nondet-static if (PSInner.pr3 != 2) - field = 108; // this line can only be covered with nondet-static + assert i == 32; // this line can only be covered with nondet-static if (PSInner.pr4 != 3) - field = 108; // this line can only be covered with nondet-static + assert i == 33; // this line can only be covered with nondet-static if (!PSInner.pr5.equals(5)) - field = 108; // this line can only be covered with nondet-static + assert i == 34; // this line can only be covered with nondet-static if (PSInner.prf1 != 1) - field = 108; // this line cannot be covered even with nondet-static + assert i == 35; // this line cannot be covered even with nondet-static if (PSInner.prf2 != 2) - field = 108; // this line cannot be covered even with nondet-static + assert i == 36; // this line cannot be covered even with nondet-static if (PSInner.prf3 != 3) - field = 108; // this line cannot be covered even with nondet-static + assert i == 37; // this line cannot be covered even with nondet-static if (!PSInner.prf4.equals(4)) - field = 108; // this line cannot be covered even with nondet-static + assert i == 38; // this line cannot be covered even with nondet-static if (PrInner.pf1 != 1) - field = 108; // this line cannot be covered even with nondet-static + assert i == 39; // this line cannot be covered even with nondet-static if (PrInner.prf1 != 1) - field = 108; // this line cannot be covered even with nondet-static + assert i == 40; // this line cannot be covered even with nondet-static if (PrSInner.p1 != 0) - field = 108; // this line can only be covered with nondet-static + assert i == 41; // this line can only be covered with nondet-static if (PrSInner.p2 != 1) - field = 108; // this line can only be covered with nondet-static + assert i == 42; // this line can only be covered with nondet-static if (PrSInner.p3 != 2) - field = 108; // this line can only be covered with nondet-static + assert i == 43; // this line can only be covered with nondet-static if (PrSInner.p4 != 3) - field = 108; // this line can only be covered with nondet-static + assert i == 44; // this line can only be covered with nondet-static if (!PrSInner.p5.equals(5)) - field = 108; // this line can only be covered with nondet-static + assert i == 45; // this line can only be covered with nondet-static if (PrSInner.pf1 != 1) - field = 108; // this line cannot be covered even with nondet-static + assert i == 46; // this line cannot be covered even with nondet-static if (PrSInner.pf2 != 2) - field = 108; // this line cannot be covered even with nondet-static + assert i == 47; // this line cannot be covered even with nondet-static if (PrSInner.pf3 != 3) - field = 108; // this line cannot be covered even with nondet-static + assert i == 48; // this line cannot be covered even with nondet-static if (!PrSInner.pf4.equals(4)) - field = 108; // this line cannot be covered even with nondet-static + assert i == 49; // this line cannot be covered even with nondet-static if (PrSInner.pr1 != 0) - field = 108; // this line can only be covered with nondet-static + assert i == 50; // this line can only be covered with nondet-static if (PrSInner.pr2 != 1) - field = 108; // this line can only be covered with nondet-static + assert i == 51; // this line can only be covered with nondet-static if (PrSInner.pr3 != 2) - field = 108; // this line can only be covered with nondet-static + assert i == 52; // this line can only be covered with nondet-static if (PrSInner.pr4 != 3) - field = 108; // this line can only be covered with nondet-static + assert i == 53; // this line can only be covered with nondet-static if (!PrSInner.pr5.equals(5)) - field = 108; // this line can only be covered with nondet-static + assert i == 54; // this line can only be covered with nondet-static if (PrSInner.prf1 != 1) - field = 108; // this line cannot be covered even with nondet-static + assert i == 55; // this line cannot be covered even with nondet-static if (PrSInner.prf2 != 2) - field = 108; // this line cannot be covered even with nondet-static + assert i == 56; // this line cannot be covered even with nondet-static if (PrSInner.prf3 != 3) - field = 108; // this line cannot be covered even with nondet-static + assert i == 57; // this line cannot be covered even with nondet-static if (!PSInner.prf4.equals(4)) - field = 108; // this line cannot be covered even with nondet-static + assert i == 58; // this line cannot be covered even with nondet-static if (s != "bla") - field = 108; // this line cannot be covered even with nondet-static + assert i == 59; // this line cannot be covered even with nondet-static } } diff --git a/jbmc/regression/jbmc/nondet-static/test.desc b/jbmc/regression/jbmc/nondet-static/test.desc index 36b8fd59718..f401d5bfe06 100644 --- a/jbmc/regression/jbmc/nondet-static/test.desc +++ b/jbmc/regression/jbmc/nondet-static/test.desc @@ -1,57 +1,57 @@ CORE symex-driven-lazy-loading-expected-failure My.class ---function "My." --cover location --nondet-static --cp `../../../../scripts/format_classpath.sh . ../../../src/java_bytecode/library/core-models.jar` -^EXIT=0$ +--function "My." --nondet-static --cp `../../../../scripts/format_classpath.sh . ../../../src/java_bytecode/library/core-models.jar` +^EXIT=10$ ^SIGNAL=0$ -file My\.java line 104 function java::My\.\:\(I\)V.*SATISFIED$ -file My\.java line 106 function java::My\.\:\(I\)V.*SATISFIED$ -file My\.java line 108 function java::My\.\:\(I\)V.*SATISFIED$ -file My\.java line 110 function java::My\.\:\(I\)V.*SATISFIED$ -file My\.java line 112 function java::My\.\:\(I\)V.*SATISFIED$ -file My\.java line 117 function java::My\.\:\(I\)V.*FAILED$ -file My\.java line 119 function java::My\.\:\(I\)V.*FAILED$ -file My\.java line 121 function java::My\.\:\(I\)V.*FAILED$ -file My\.java line 124 function java::My\.\:\(I\)V.*SATISFIED$ -file My\.java line 126 function java::My\.\:\(I\)V.*SATISFIED$ -file My\.java line 128 function java::My\.\:\(I\)V.*SATISFIED$ -file My\.java line 130 function java::My\.\:\(I\)V.*SATISFIED$ -file My\.java line 132 function java::My\.\:\(I\)V.*SATISFIED$ -file My\.java line 137 function java::My\.\:\(I\)V.*FAILED$ -file My\.java line 139 function java::My\.\:\(I\)V.*FAILED$ -file My\.java line 141 function java::My\.\:\(I\)V.*FAILED$ -file My\.java line 150 function java::My\.\:\(I\)V.*SATISFIED$ -file My\.java line 152 function java::My\.\:\(I\)V.*SATISFIED$ -file My\.java line 154 function java::My\.\:\(I\)V.*SATISFIED$ -file My\.java line 156 function java::My\.\:\(I\)V.*SATISFIED$ -file My\.java line 158 function java::My\.\:\(I\)V.*SATISFIED$ -file My\.java line 163 function java::My\.\:\(I\)V.*FAILED$ -file My\.java line 165 function java::My\.\:\(I\)V.*FAILED$ -file My\.java line 167 function java::My\.\:\(I\)V.*FAILED$ -file My\.java line 170 function java::My\.\:\(I\)V.*SATISFIED$ -file My\.java line 172 function java::My\.\:\(I\)V.*SATISFIED$ -file My\.java line 174 function java::My\.\:\(I\)V.*SATISFIED$ -file My\.java line 176 function java::My\.\:\(I\)V.*SATISFIED$ -file My\.java line 178 function java::My\.\:\(I\)V.*SATISFIED$ -file My\.java line 183 function java::My\.\:\(I\)V.*FAILED$ -file My\.java line 185 function java::My\.\:\(I\)V.*FAILED$ -file My\.java line 187 function java::My\.\:\(I\)V.*FAILED$ -file My\.java line 196 function java::My\.\:\(I\)V.*SATISFIED$ -file My\.java line 198 function java::My\.\:\(I\)V.*SATISFIED$ -file My\.java line 200 function java::My\.\:\(I\)V.*SATISFIED$ -file My\.java line 202 function java::My\.\:\(I\)V.*SATISFIED$ -file My\.java line 204 function java::My\.\:\(I\)V.*SATISFIED$ -file My\.java line 209 function java::My\.\:\(I\)V.*FAILED$ -file My\.java line 211 function java::My\.\:\(I\)V.*FAILED$ -file My\.java line 213 function java::My\.\:\(I\)V.*FAILED$ -file My\.java line 216 function java::My\.\:\(I\)V.*SATISFIED$ -file My\.java line 218 function java::My\.\:\(I\)V.*SATISFIED$ -file My\.java line 220 function java::My\.\:\(I\)V.*SATISFIED$ -file My\.java line 222 function java::My\.\:\(I\)V.*SATISFIED$ -file My\.java line 224 function java::My\.\:\(I\)V.*SATISFIED$ -file My\.java line 229 function java::My\.\:\(I\)V.*FAILED$ -file My\.java line 231 function java::My\.\:\(I\)V.*FAILED$ -file My\.java line 233 function java::My\.\:\(I\)V.*FAILED$ -file My\.java line 236 function java::My\.\:\(I\)V.*FAILED$ +file My\.java line 104 function java::My\.\:\(I\)V.*FAILURE$ +file My\.java line 106 function java::My\.\:\(I\)V.*FAILURE$ +file My\.java line 108 function java::My\.\:\(I\)V.*FAILURE$ +file My\.java line 110 function java::My\.\:\(I\)V.*FAILURE$ +file My\.java line 112 function java::My\.\:\(I\)V.*FAILURE$ +file My\.java line 117 function java::My\.\:\(I\)V.*SUCCESS$ +file My\.java line 119 function java::My\.\:\(I\)V.*SUCCESS$ +file My\.java line 121 function java::My\.\:\(I\)V.*SUCCESS$ +file My\.java line 124 function java::My\.\:\(I\)V.*FAILURE$ +file My\.java line 126 function java::My\.\:\(I\)V.*FAILURE$ +file My\.java line 128 function java::My\.\:\(I\)V.*FAILURE$ +file My\.java line 130 function java::My\.\:\(I\)V.*FAILURE$ +file My\.java line 132 function java::My\.\:\(I\)V.*FAILURE$ +file My\.java line 137 function java::My\.\:\(I\)V.*SUCCESS$ +file My\.java line 139 function java::My\.\:\(I\)V.*SUCCESS$ +file My\.java line 141 function java::My\.\:\(I\)V.*SUCCESS$ +file My\.java line 150 function java::My\.\:\(I\)V.*FAILURE$ +file My\.java line 152 function java::My\.\:\(I\)V.*FAILURE$ +file My\.java line 154 function java::My\.\:\(I\)V.*FAILURE$ +file My\.java line 156 function java::My\.\:\(I\)V.*FAILURE$ +file My\.java line 158 function java::My\.\:\(I\)V.*FAILURE$ +file My\.java line 163 function java::My\.\:\(I\)V.*SUCCESS$ +file My\.java line 165 function java::My\.\:\(I\)V.*SUCCESS$ +file My\.java line 167 function java::My\.\:\(I\)V.*SUCCESS$ +file My\.java line 170 function java::My\.\:\(I\)V.*FAILURE$ +file My\.java line 172 function java::My\.\:\(I\)V.*FAILURE$ +file My\.java line 174 function java::My\.\:\(I\)V.*FAILURE$ +file My\.java line 176 function java::My\.\:\(I\)V.*FAILURE$ +file My\.java line 178 function java::My\.\:\(I\)V.*FAILURE$ +file My\.java line 183 function java::My\.\:\(I\)V.*SUCCESS$ +file My\.java line 185 function java::My\.\:\(I\)V.*SUCCESS$ +file My\.java line 187 function java::My\.\:\(I\)V.*SUCCESS$ +file My\.java line 196 function java::My\.\:\(I\)V.*FAILURE$ +file My\.java line 198 function java::My\.\:\(I\)V.*FAILURE$ +file My\.java line 200 function java::My\.\:\(I\)V.*FAILURE$ +file My\.java line 202 function java::My\.\:\(I\)V.*FAILURE$ +file My\.java line 204 function java::My\.\:\(I\)V.*FAILURE$ +file My\.java line 209 function java::My\.\:\(I\)V.*SUCCESS$ +file My\.java line 211 function java::My\.\:\(I\)V.*SUCCESS$ +file My\.java line 213 function java::My\.\:\(I\)V.*SUCCESS$ +file My\.java line 216 function java::My\.\:\(I\)V.*FAILURE$ +file My\.java line 218 function java::My\.\:\(I\)V.*FAILURE$ +file My\.java line 220 function java::My\.\:\(I\)V.*FAILURE$ +file My\.java line 222 function java::My\.\:\(I\)V.*FAILURE$ +file My\.java line 224 function java::My\.\:\(I\)V.*FAILURE$ +file My\.java line 229 function java::My\.\:\(I\)V.*SUCCESS$ +file My\.java line 231 function java::My\.\:\(I\)V.*SUCCESS$ +file My\.java line 233 function java::My\.\:\(I\)V.*SUCCESS$ +file My\.java line 236 function java::My\.\:\(I\)V.*SUCCESS$ -- file My\.java line 115 function java::My\.\:\(I\)V file My\.java line 135 function java::My\.\:\(I\)V diff --git a/jbmc/regression/jbmc/reachability-slice/A.class b/jbmc/regression/jbmc/reachability-slice/A.class index 7f527e5fa9a3b3375f571dd2761cf5a82c2dea18..11dea8278127f4f7ae4e16742baba84cbca2d2f4 100644 GIT binary patch literal 577 zcmYLFT`vPc6g{)k-O;tQTUDh<8bW#C#bb%aS0p|jh=eEGcF0zBWq0dW_ytXP^^Ams zgm?eM*FO+(XQTRZXXe~T2)e;%I!%wg1oKspW`{Q?;i9BF|86Il!j3^DYLJ3%1* z(DfR@vKu(%x~wv=0|uk$Hr#N5ffuIs7-CCaRWc+t+=kq0o|dJ*tH{(o@;qu6))lK~ zCv++&o6gx^v#VIC|E)21yry4~tF9U{N;5U*+_7My+d>!O3|R%t)}6-jY^iN&#rHj* z?34s@7KSmxknGU5%QaaE$x{bfs#6?>OjQQ1FRTBH$X3{-24y)wo_<5n@33T6Nz;vk zDJN7ddX3P@=+vhlz-|-~JyeYdRIOels4D6OG#UohZ2p!zoX=e$Z}WG$+5Cg*EwmOU zhc7Yq1it@(*o)0S+jxTT?hgJ%xDwMMv5Cl+PND`m6G)QN3}FS5ogu~|Sy&}BNfQFv rHwtWkDE5DdxyUVGr}TRmEr{4PV*CzTN247`?a-lFiz-_xve5Snyy0cy delta 238 zcmXYry$%6E9K>gL?*r$!laR;-QBY{E(JE9b@d}QJL_{T8&v4Oe)hdZXqV*=e-ay3c z#umT-{AXt;d$lgIeEXg+0J;crQ1D$8Tolv(Al+5A7Hk307YG)~CW)8HY95a!i`jII zCM4tfNC+@UI^1fUg46DtAdVCQF6kIkUuBRbb#(f#Xou<^jeF4^rBFSnLiHpM7-mED nGW(miu16}z+Rp@Vd=3)K^0&*U3 diff --git a/jbmc/regression/jbmc/reachability-slice/A.java b/jbmc/regression/jbmc/reachability-slice/A.java index 7680ebd172f..f0fe5bb037b 100644 --- a/jbmc/regression/jbmc/reachability-slice/A.java +++ b/jbmc/regression/jbmc/reachability-slice/A.java @@ -4,11 +4,14 @@ public void foo(int i ) { // We use integer constants that we grep for later in a goto program. int x = 1001 + i; if (i > 0) { - x = 1002 + i; // property "java::A.foo:(I)V.coverage.3", see https://github.com/diffblue/cbmc/pull/1943#discussion_r175367063 for a discusison. + x = 1002 + i; x = 1003 + i; + assert false; } - else + else { x = 1004 + i; + assert false; + } x = 1005 + i; } } diff --git a/jbmc/regression/jbmc/reachability-slice/test.desc b/jbmc/regression/jbmc/reachability-slice/test.desc index c997bae2a05..0ddbc9d0505 100644 --- a/jbmc/regression/jbmc/reachability-slice/test.desc +++ b/jbmc/regression/jbmc/reachability-slice/test.desc @@ -1,13 +1,11 @@ CORE symex-driven-lazy-loading-expected-failure A.class ---reachability-slice --show-goto-functions --property 'java::A.foo:(I)V.coverage.3' --cover location +--reachability-slice --function A.foo --show-goto-functions --property 'java::A.foo:(I)V.assertion.1' = \(int\)\(short\)1001 --- += \(int\)\(short\)1002 = \(int\)\(short\)1003 +-- = \(int\)\(short\)1004 = \(int\)\(short\)1005 -- -Note: 1002 might and might not be removed, based on where the assertion for coverage resides. -At the time of writing of this test, 1002 is removed. - Doesn't work with symex-driven lazy loading because the reachability slicer is a whole-program pass. diff --git a/jbmc/regression/jbmc/reachability-slice/test2.desc b/jbmc/regression/jbmc/reachability-slice/test2.desc index 93b579d1b63..11c64768983 100644 --- a/jbmc/regression/jbmc/reachability-slice/test2.desc +++ b/jbmc/regression/jbmc/reachability-slice/test2.desc @@ -1,11 +1,11 @@ CORE symex-driven-lazy-loading-expected-failure A.class ---reachability-slice-fb --show-goto-functions --property 'java::A.foo:(I)V.coverage.4' --cover location +--reachability-slice --function A.foo --show-goto-functions --property 'java::A.foo:(I)V.assertion.2' = \(int\)\(short\)1001 += \(int\)\(short\)1004 +-- = \(int\)\(short\)1002 = \(int\)\(short\)1003 = \(int\)\(short\)1005 -- -= \(int\)\(short\)1004 --- Doesn't work with symex-driven lazy loading because the reachability slicer is a whole-program pass. diff --git a/jbmc/regression/jbmc/reachability-slice/test3.desc b/jbmc/regression/jbmc/reachability-slice/test3.desc index 7b10cf97e1a..4c7e8091dc8 100644 --- a/jbmc/regression/jbmc/reachability-slice/test3.desc +++ b/jbmc/regression/jbmc/reachability-slice/test3.desc @@ -1,6 +1,6 @@ CORE symex-driven-lazy-loading-expected-failure A.class ---reachability-slice --show-goto-functions --cover location +--reachability-slice --function A.foo --show-goto-functions = \(int\)\(short\)1001 = \(int\)\(short\)1002 = \(int\)\(short\)1003 diff --git a/jbmc/regression/jbmc/remove_virtual_function_typecast/test.desc b/jbmc/regression/jbmc/remove_virtual_function_typecast/test.desc index 8bbea6300ec..defa750d6ab 100644 --- a/jbmc/regression/jbmc/remove_virtual_function_typecast/test.desc +++ b/jbmc/regression/jbmc/remove_virtual_function_typecast/test.desc @@ -1,6 +1,6 @@ CORE symex-driven-lazy-loading-expected-failure VirtualFunctions.class ---lazy-methods --java-max-vla-length 48 --unwind 8 --java-unwind-enum-static --trace --cover location --function VirtualFunctions.check --show-goto-functions +--lazy-methods --java-max-vla-length 48 --unwind 8 --java-unwind-enum-static --trace --function VirtualFunctions.check --show-goto-functions \(struct VirtualFunctions\$B \*\)a \. VirtualFunctions\$B\.f:\(\)V\(\);$ a \. VirtualFunctions\$A\.f:\(\)V\(\);$ b \. VirtualFunctions\$B\.f:\(\)V\(\);$ diff --git a/jbmc/regression/jbmc/removed_virtual_functions/test.desc b/jbmc/regression/jbmc/removed_virtual_functions/test.desc index cf36ec36380..632fb272be9 100644 --- a/jbmc/regression/jbmc/removed_virtual_functions/test.desc +++ b/jbmc/regression/jbmc/removed_virtual_functions/test.desc @@ -1,6 +1,6 @@ CORE symex-driven-lazy-loading-expected-failure ArrayListEquals.class ---lazy-methods --java-max-vla-length 48 --unwind 8 --java-unwind-enum-static --trace --cover location --function ArrayListEquals.check2 --show-goto-functions +--lazy-methods --java-max-vla-length 48 --unwind 8 --java-unwind-enum-static --trace --function ArrayListEquals.check2 --show-goto-functions e2 . ArrayList\$Itr.hasNext:\(\)Z\(\); ^EXIT=0$ ^SIGNAL=0$ diff --git a/jbmc/regression/jbmc/stack_var12/test.desc b/jbmc/regression/jbmc/stack_var12/test.desc index 27eaa97285e..158fcd8e452 100644 --- a/jbmc/regression/jbmc/stack_var12/test.desc +++ b/jbmc/regression/jbmc/stack_var12/test.desc @@ -1,9 +1,9 @@ CORE stack_typecast.class ---cover location --function stack_typecast.f -^EXIT=0$ +--function stack_typecast.f +^EXIT=10$ ^SIGNAL=0$ -covered \(100.0%\) +^VERIFICATION FAILED$ -- -- This tests that there is no invariant violation when modifying the values on the diff --git a/jbmc/regression/jbmc/string_field_aliasing/Cart$Category.class b/jbmc/regression/jbmc/string_field_aliasing/Cart$Category.class index e3dcef537a3d4923196d50e02f9143300518a055..d69b188bf014557989fa328581e3b273f3e998bf 100644 GIT binary patch delta 149 zcmbQne1=Kt)W2Q(7#J8#7$i6um>KxF7+4qt*cpV_8AK;a#Z5e*peM%8AkN6Z>zr6r zqT-xblA4}hRLRJ|fnf4@=H;apIp-u67pE3a{Nib=#J~iE3=CXa+FKbIwYD=bZ3OZd j8F+vs8<1vT-~h_=0%;}&J_ZpW%>@)?W)Nf$W?%pSx*ruv6)W2Q(7#J8#7^FEFm>ER47+4rY*%`#y86+l3#YqYITQge4YbCMM;i zhJXl029}bH%;Je_WCZwqoD+*mRGbq_Qq%K`Dy=7$DTzq3Ge|Kq@S;deJm$%0H(7vD z)R~Ea2WS}^10#^+VBiIkVhl_`l8b?lK@doTSnNOER47+4rY*%`#y86+o4sW3`Sw9lLPL_tiNok50? zfyX(qs6-{8C_kk%xrC8{eX;;!hN}_-6A&^maA|38Wnk3W&cL)0$YW#>1d?n(ngM7m e6N3AR delta 210 zcmbQhe3Mz~)W2Q(7#J8#7!)`em>DFv7+4r2*%_qS8Du6(sW8e;w9hjY^2tw5%n3^@ z%1lhkNeuxJj0`L#8JWe54D10#`6;EzC5#MwKF*0nB`Q$9^~BXmJaX&|@{9~TVDX8M zGZO6>n1GOhflEt!D+8m}b_S-6Kpqo=AdqBZU<8uP3_?Is45Erbm_ZcC1FC1>Vc-SI eGXZ5l>cxQ~3_z7k3>*wn44gnVGmsWxU;qFSUh!Vq6??#j2a+LLa#+6uJecIzb~r(1!v_nyf&Lqc-R?hUo9me<#|dg6p+ z!>SmBz*)?a6WO)}ZlEGi#Z7@*sBqjCxPzKN4l@k%W5GwGx*luoX;T2vIPMDE!+nPA zIP*n&SD9Xh#KjXkwNMwB&RIv8IslJ-LM-|X+*ljn fM%D}>j)-{3=-^U#oF_U+BSJrfMQR`=3)8@VFXgCh literal 680 zcmZWmT~8BH5IwhDy504*#T8KN7f98XB7Nbl#+N20CXJfVV8Yw&a?@TcyJmN5fZxOm z325R2KY$-aJa=0Z!#>R1nK^Uj%p33wnPL2iS$0*WCZ=%vvr!L+IxL=ZZe;Q^2rFSMW*?WOvv$ZSW^x}OjQ0tpW zf0`Z+buv)H2{S=I4%K8=CC0|{q?3(JN{)U{C0SR%3&%SAHc&^~0_)8@+n7)4_7Bt# z)tRVh)Y-`r6OFp9Jqr1LBc%F2TtJXHxZ5S*@5Iw2)E|u1<=N3&mRq8V8uw7cP@;*t zL<<`dZPZv!#T&oPn1rXExx27OZp1%2Xg?0rvLx| diff --git a/jbmc/regression/jbmc/string_field_aliasing/Cart.java b/jbmc/regression/jbmc/string_field_aliasing/Cart.java index d14d35baafc..a499e1cd142 100644 --- a/jbmc/regression/jbmc/string_field_aliasing/Cart.java +++ b/jbmc/regression/jbmc/string_field_aliasing/Cart.java @@ -11,6 +11,8 @@ class Category { public boolean checkTax4(Product product, String s) { product.size="abc"; - return s.startsWith(product.cat.name); + boolean result = s.startsWith(product.cat.name); + assert !result; + return result; } } diff --git a/jbmc/regression/jbmc/string_field_aliasing/test.desc b/jbmc/regression/jbmc/string_field_aliasing/test.desc index 0666460000c..f3e41c0662f 100644 --- a/jbmc/regression/jbmc/string_field_aliasing/test.desc +++ b/jbmc/regression/jbmc/string_field_aliasing/test.desc @@ -1,13 +1,11 @@ CORE Cart.class ---cp `../../../../scripts/format_classpath.sh . ../../../src/java_bytecode/library/core-models.jar` --trace --cover location --java-max-vla-length 96 --refine-strings --java-unwind-enum-static --max-nondet-string-length 200 --unwind 4 Cart.class --function Cart.checkTax4 --string-printable -^EXIT=0$ +--cp `../../../../scripts/format_classpath.sh . ../../../src/java_bytecode/library/core-models.jar` --trace --java-max-vla-length 96 --refine-strings --java-unwind-enum-static --max-nondet-string-length 200 --unwind 4 Cart.class --function Cart.checkTax4 --string-printable +^EXIT=10$ ^SIGNAL=0$ -checkTax4:.*: SATISFIED +^VERIFICATION FAILED$ -- -checkTax4:.*bytecode-index 8.*: FAILED dec_solve: current index set is empty, this should not happen -- This checks that assigning to a field of an object (which generates a WITH expression in this case) doesn't result -in conflating the String-typed and non-String-typed fields of the Cart class. When they are conflated we get -warnings from the string solver and missing coverage. +in conflating the String-typed and non-String-typed fields of the Cart class. When they are conflated we get warnings from the string solver. diff --git a/jbmc/regression/jbmc/trace_class_identifier/TestGenTest.class b/jbmc/regression/jbmc/trace_class_identifier/TestGenTest.class index 4238fc097d67b30d995df670ca8fa4d5af465a15..d81426ff313407801dcc483c2a7f421811806e14 100644 GIT binary patch literal 509 zcmYk2OHaZ;6ot>w(t%Q-fFeFvn7B|EvSEovgO81m1;j*lr5#PNwx%uq82*53HIYOU z-TRx2@lNGon#}FoIp@1)=IiI}13(jX9UPS`(pcbF)S;llQPr`88pkq2Wy6Xh5yo!d zM~7}?^*!M*upWcfa(y@6V^B7?E*aEz;0T7|sq2gL;ay*ZT`4B*HAB7=TlVdlbwBB4 zTDCWF>z!a2+Tz%iTC*#n_(b@!>WIh7^)Obh-bgdrN>0vlM6f`4ldr&UXu@~AMA?jl7WP~xp;q(;cSL%AA5{gk#;Vk;1xShUk%(%j-7 p>Ki7b>E;a8Oz?y%r(dCsz|}{n$_r9+)HH!a5YX6{VM@uQ@-O8wTTB1| delta 180 zcmey%{FPDk)W2Q(7#J8#82Gptm>Ia)8F<(kcqcmQP3%&rXJKGvWZ(`-EiQ3S%>z-4 z3<6n+Wr_MZiFxVz{z+M>$t4Vm3`{_cAi%`H$N