From c7bf5287331cafd70e8e09edef87ecd475767e95 Mon Sep 17 00:00:00 2001 From: Adrian Palacios <73246657+adpaco-aws@users.noreply.github.com> Date: Wed, 16 Aug 2023 17:44:10 -0400 Subject: [PATCH 1/2] Update docs before `0.0.6` release (#128) --- README.md | 4 ++-- docs/user-guide.md | 24 +++++++++++++++++++++++- resources/screenshots/coverage-info.png | Bin 0 -> 32387 bytes 3 files changed, 25 insertions(+), 3 deletions(-) create mode 100644 resources/screenshots/coverage-info.png diff --git a/README.md b/README.md index b542f0f..55b2f85 100644 --- a/README.md +++ b/README.md @@ -1,6 +1,6 @@ # Kani Visual Studio Code Extension -A [Visual Studio Code](https://code.visualstudio.com/) extension that allows users to run and debug their [Kani Rust Verifier](https://github.com/model-checking/kani) harnesses in vscode. +A [Visual Studio Code](https://code.visualstudio.com/) extension that allows users to run and debug their [Kani Rust Verifier](https://github.com/model-checking/kani) harnesses in VS Code. ## Usage @@ -22,7 +22,7 @@ Check [user guide](docs/user-guide.md) for more detailed information. ## Requirements - [Visual Studio Code](https://code.visualstudio.com/) 1.50 or newer -- [Kani](https://github.com/model-checking/kani) 0.29 or newer +- [Kani](https://github.com/model-checking/kani) 0.34 or newer NOTE: The extension only works on Cargo packages. For standalone Rust files, Kani is only available on the command line. diff --git a/docs/user-guide.md b/docs/user-guide.md index 87201f5..659c737 100644 --- a/docs/user-guide.md +++ b/docs/user-guide.md @@ -16,6 +16,8 @@ This guide provides the various workflows that you can use to verify and debug y - [View trace report in window](#view-trace-report-in-window) - [Kani output logging](#kani-output-logging) - [View full Kani output](#view-full-kani-output) +- [Coverage information](#coverage-information) + - [View coverage information](#view-coverage-information) ### Verify Kani harnesses @@ -81,7 +83,7 @@ By clicking the `Generate report for (your harness)` option in the error banner, You can click on the `Preview in Editor` button to view the HTML trace within VSCode. It should look like this: -![Generate Report](../resources/screenshots/view-report.png) +![View Report](../resources/screenshots/view-report.png) ### Kani output logging @@ -91,3 +93,23 @@ It should look like this: For every test run, you can view the full output from Kani logged into the output channel as a text file. To view the log, open the output channel, and click on the channel drop down list to view a channel called `Output (Kani): ...` ![Generate Report](../resources/screenshots/view-output.png) + +### Coverage information + +Line-based coverage information can be displayed for any harness as in: + +![Coverage information](../resources/screenshots/coverage-info.png) + +To enable the coverage feature in the extension, toggle on the `Codelens-kani: Highlight Coverage` setting in `Settings > Extensions > Kani`. + +#### View coverage information + +Once the coverage feature is enabled, the `Get coverage info` action should be visible on top of each Kani harness in the project. +Running the `Get coverage info` highlights all lines for which coverage information was obtained. + +Coverage information (as described in the [RFC for line coverage](https://model-checking.github.io/kani/rfc/rfcs/0008-line-coverage.html#postprocessing-coverage-checks)) is represented with three colors: + - **Green:** Indicates `FULL` coverage. + - **Yellow:** Indicates `PARTIAL` coverage. + - **Red:** Indicates `NONE` coverage. + +**NOTE**: Line-based coverage information is an unstable feature. diff --git a/resources/screenshots/coverage-info.png b/resources/screenshots/coverage-info.png new file mode 100644 index 0000000000000000000000000000000000000000..f539092a42b97499bcd1caa0421e1a5cc43eb21b GIT binary patch literal 32387 zcmZU41ymf((l+kyu0eylYjB4E!QI{60t9!L#T|kNcV}^T2=4Cw?|bk4R=b3elSrraTysEQZx_^U05anb7g57!?G@_Z%^c1%X54#s9o zo_3D^uz(48@`0*$X0AqLo_4nOE_|MX6#t^&1J(a&W~Lzf7m2HlAjJ;_WioLGXEQP` zCKe_Z3LykCGBN>YQ*%DmZ<7CE2b~F0Sh~78@-Z`ecz7^*uroP0TQIZo^71mXuraf- zF@h)du>ooJU z`X5d9F8{eL&E-)8<- zE6C152m;LiJ!V1(cLUtjU|=F(GT%hMdxD<F>mxtkgsCLDX26lG*A9;z+I{&E_i-%RR+2SoG+ly6HTC6%nD7jJ(yUVpSx-$0Q2# zaf=FnYHnRv6^A7%rwl`kG9OSx|{9Ge0T31c~n z4zH?@IcA$9LAw_6WXx-%TXI75?ZU6ih*rkhj|e6;iCSUy8)P3i`RB*$<$jLO1s!JA z!m-U>b?c+FsFTrj3r)7;PuG)qnI`)U?a1V2n&)qw$K28LwPfHxHq?<4YUfE!Trv@2D(>75)v=$>j7T;rTmar2%d=mQjm zCH~U=b`!<$qc#s%W3Ym2JDnGl?YR?C@Bi+d!RumfW>7u;MyY;@SF7)PJt+2id`9Z* z?7Vm0y!9aGeRET|SIHZ}=KrH<-Sb1Sb-ON^ZA>SLVqkc9%KOl0hNCtC4Nm=`>rpWh404jO+W$3S) z?zj^~$ZctvKMToHCosYLb2oXIoaD?SifNn%0yMn*i*hPm4#NZtenpc2w?(bC-eQby zkeYhy1^WCMEUiHGtfgEZ7?RM&M$c%=PS^V>4VDTD$3l|oXT0Y)s zcjy>=`a>E>Zi!Y1GL8nKDoMHbQoWhn`+6DsywZu)`^$Z?B7o0%2;bsp1@QUt*j-#P zfBtD#B=fv?o#DKu76Vn#)jfj9+>r-6bQcuww7D`ALpZh@C(M+l>l{&~*WM)7j8NT( zI9>%Z_Sd40pMsb1Y|C*J*x1;|T(iH6mJRIdypqHg93rr2{ic%~QfOT%-2(n(Cev_U z7CEiojM3DeKTc7GS}i}b&`Vi@ZTdCa&Sfm=`zSmud?}AGL%}u}c^VC~I5~0+)BsBU zZJbk_3-R4(a}zSfF(#2|-HH4PVLtr#aYl-Cfm$0H8k&!U_)Seouz13%L=ix*sM=*U zNBw)Wlxgnzo0Qa;*CBuglSVNaWaN<`SQ1*{&o`Hz(-q7=utCxb{3lcg^vqpP1!-h# zd7Y1&KKDq|Ai0c6!tagLqKd9d4iPC-Uw4b8h6OU*Cz)DzkKYUR`0l2~J41+~)0p(= z$EjK7bZhhlw*e9+`U@CmUYc%N5BK+6w##{(`>$<8DQ@pP3tN;D5-IG{ztQMwDy8kL zKl@D|E4HZU`6N|eiRqo(2xW&>CF=bjY*f>A3PuON7fqzIQ!!I2aJ}!z39J!0r(WbO z`QIDU5wS8_xm}GWu2;wH6+5KaA$BD<4@sw<=8Yj0)^|T&EuJzm2bWpz@M>6hThd$oSlJWzZtN2Og@j)6o{^s~ zFTYf;*vmMP#hu1JC7=dtBCgOGnVh%cih%4b0c{+o6|E-pyodSxdf5#SUH!FTcM`bx zF{dPq4THSg%0KuUzLZ4pcAUKpQY?7VM*|?uJN3|q$UJZN)edpC)5pVsu>TswT62o> z3g-sVK*3T(q8dRkn(VGE-yXyi2VIf_vNER-2p6N~cfrcoug}G8@Dk3XJMr&~$1BSF(xx<@!|m zRlxhH!B2ds8<5Zw4+YZie+|s$`C)z^Y_Lm+>rD1s_rj9SPo=uQP6>Zy8WF8(4~&VZ#UM%O&%`D?0W)UT;l|1=#LR}6yG)AhVxDb+hl^)VIyVJ9atunF5=2(nFDa}2qYQx|FS}+4S^En7vGf>N9A=Ii{EVJv$WARY{0(lSYdm& z1&WzG4qz%B#imIjZ3~!&Ob#gk$>obUi-;&T^^rN`^>&`cu*f6e=C-&uT$6MI-tS-1 z11!Vp8r%`?V}l@rQJWp@=gU<1(!D{ehmQ@9Eh}VpC=|kPE|(WJX@}`B*%k*_FvRw% z7Xp{-7L3qh7W%2mG)HB=9ZkmB6hxNR(wpS{%7q#V?>kc`u340ee@g_3ZFlZ~iT$)z&P1f#&j zS>9}DA4Mhy4;GjoZ2uy(zna;68cP!e2S5=|PUnlel}ZTQGQG%|^m&$!2R^JhbaVDD z7)Sle@{SE;9(YN)RR^vK4DRGG_p_9KzK$k)MPfj|i1U4Yykt&C za}B9i#U3LhG->Yi*o ziLcgNTCAMQ&CZs-pp3HU!h&arb9&K!x%eg3KMg!oN9?#;fnXDHQw>Y@jt1@$buaa? zRG`lg+(;uM^o*8^Z2m54(!GCAL3s2P>BEpnx(xD8NipA`z)v*WMqli_dz;z7_c}Bh zk5z0cn^i6HAjkh#5IFmMLShoit>-#$Bs%tcs?c-t1ch$_ERQmCf1+m162bo4xL*C; zgig_vmy)z>96CKXvgorxA7l4KJaK@xWP|0%C}u;F2BlJJ3aMAg6=X8d!O_VmNLjLo zc1yfudNYfqJK{UpfS}7Qf}i)qp_1IA+C_56uN)PhJdWNz@(oFTOE@;{v5;puo05lP z261$HZf3BbO;|B#$dHtld{Pg{=!HRKNcoUv2obl~DSmq97tlu5C@~y;V^Jlcbn*o3 zjiasvaFB_h4W~LcP`GgUS= zhi)M$Lc(Oq(P{a~wS|-;re!-o7A;z-mX2%~k0XEdX5YGxLkwMSbK+ggq3(rZS8t_+ z#0!mzdBB87;3D6WEk-QS@T+8sx5Z`1h*S(JgA2gvm4IW^6HJHXmdXV zv1T}$6WsIP9Iu;O2-JM!bTToTO`l7_?O`Os16kUimL~WNdXBx&ZRZla7#FWUR{&N~ zmW1nlE*zQ8kG#^w8R%^%6_u_VMT(hjWF4dj#H{y08FPkibn}M_ekHmcJ`7}1mH{;# zH?kWCLCBZsgmKC*4#{+TN+gm;W6HEw?Ci1!x;#3`*l@vg>{-z_!|TEP%$pMaW_p-J z@&R%ry2G?)o`--C!R(K$UM%5N7nt8jWJldr7I?}tm+Xci7NK9mh?5yjP)AY|f}M-Z z<{%bQBLp7(-yIv^>HI*UStk+K9o(ZPAT*%^oli_a67N+Gj>j}yGFB2!%mVawlDhA?Aj>7CGsZQ8 zd;^ZTi`?(R=Pwmk3=}e>DN&XJhX5QiM{uSHM)xBlaN?^Enz%kFG>{^rfx@yLIx8e6 zdk_1tfQ|{j+y~OEWo^3oH8Paq**dF?{5U3zvKn zwOp%LJX$D9{rm&X9MAo74@-)2k7NKoJi8^l>w7`xOKlOKL{LEpR_v>U1^*5+`VY1! z8z>43a}5^C-lCsceCD=K`A(d{^hwmqi&{!R3jax8+BCIY1#LK%U>KOplune82PD>D z2sJMG_@kr@&K+W>q?`H|F)XWeaf(J!S}kST(BN{qsBXr639ErgUv`cuSIw?IR&-AIwK_Azu8JYYF+e8>wCh4jaj8&Y# zO}IVY#*%s7Ph_K_0W?M!VapCOgJq5SMQ|}V{BP@O^9gNT{G=BE6qKN|X?UadI1Oer zIt%aASOnYjCeEk!+iIC%B&3-y8OIJI(dA0(VM$o6mxz7D((?RbSvxqZBouKBD0x!%*yfX}(JzXVp$TUH| z!{IyIc^7=m2o4p_L3|@3nzp|Hr1^|WNy}^Mjc!y18`d}4(DYu%sN<}DP$(j4#J;OB zhY7iIJk1_GH9+M^-2~k3bzsh#4fGJTK9IH-xvcrN-t>;#PJ>49kV44?)6+yW5-CHS zIZ1eC^?;1oqVXj#UML0xwjZEub=achs$!lK0U{zhJOe5R}+!tk#em(07njhVhgjUhIWh+*QHXV(o}zy!{l-WL7m=?V@W|XJuMS!J`pt@Za*f!oaJA^ScL_2rVE4#2XKi(@q_gg2sv8 z_xG8j+k#4RUri#*domP}H_GcDqiZ80mU3)W>-z^A7h{)kV@I5v{^ zwY(x@FsEOP8S5B?XS@HFP(qhbr@&eA#Z@S|-?eK9GV=9hpV$0k-cx0pWTwX`C-5L! zagJ`8U+fz?@ZfH9HyRh%W#!q*?N2nP#bRkp&N#P*ga+qQbAd|rDLs6=`lk|=Zdecx zfVJO#zo_%xR!}L8Uz^Xt&gV*&zqnFgZN+CAFwj%PskS{In(O~E3S|>Vvl;AsmhJ{_ z|NG0TqPVPl(~vmIH-vgaEZ76zyx*UNyI4X zy6>fS*3Af~H+HeD*Cr#;ojtnDh)tM!0=Lph&`6UI7CZCIIM21To}c)q@{my(7)H2k zaKgF0?<|P{-hXpqija#@S%SqWGCwA^km6J#pL9a1m@y87Vc;7pTOM4a$OkGlYut0` zZ}Es&zwRuFdO7!gL5!1Z%(Vn$fJ>}R{#0M}QL|WwBrvBBhTn{ehNaxahQE}+Cf`q< zt1{Sr2TcU+MEMU}NZMY^Ww5km17-!k~WGxBmPH4ANR~QJ4zF$y(i5DvkgS$whGa|5c?A>A&*0<+? zZi%^}5q`_b+bN^F_m-F~QW=ckT{_4Vz&)FYfokjGB?YD~oDKa>kGP!wkpVN2ZGwm| zk~HCP^|yCY&FHf5cn9CvLD5;MGzb>_+_Pg=41{R;JY0%}_ApPjqQq65Bc#;%!TWoA-xvAhYr5Q}POH=aS&_ zX;}Eq>my%=b1M6u!=CkAQOk4zz%*S~ha8s7Kk@xaS=^_;ecKfrk2cqE+j7`JT^8b| zh}FYPdGEA7`MbE8rxp1;g?W$)bY zICh9SFG`ErweFFFg9%^ulAYER$e)5%I9qs^t@@OsE#W?l`o)o{YE;J_BvrBtVJ!lqjDCmuT^4e9M9UDKVCArk6!KY zkO9ZaF)`GDrkPDK*EcUVT0}I-mFU`xoG$_Njn|~Q8msk_nqh3a7#Ocsd^VB~9R8N_ zmSi)uEN;w51ie#IA>?f9|m5VaW34ouNC zm`~hH3i0$;_6rRJ(&=qNcEHuyLqJ4xZMGl=PhZKCDT5YTr~;TL(h^X<-OmSvf@Pt3 ztow?7TmvHj?sGiqZ}W1SS^`2KN{&W9G{;(ZgiQOAvKjwEd`c8;E}Uyom`XAF!c8OU zL3Yt;nAx1x(8p2UhTdmy842fjwsJLvjP*BDN{>WY!Grgm4N-Rc#>s>>vP}08oJ;N; z3$j8aFud>?``1?0-xu5+;a4K#I&=Q4IQk5w{Xy*ZpDZYFF%!)U&cLv3DX zakeLzNnYH~@F3`)U)3%6cNyebUjI(KPQ-ou?Al1bt*y-jN4#X;bV?7UjAdnXHi&wq z61uh|#mCDO4JEXI$uvh!%?L8Kd4l&+Q}R;6|B=ZRihnjt;xm3Y+fu^eeQOXh|4@RcQ%=g%f4- za9C>Cb<}Txzi`;m3g7#`K?hZ(D^bl|&DG)MCy)uMomfi0kKV@>)2=TJ%cD#t;t4yX zc;VO!D75e^omF|E#G}KYqPfCFzT&stvJX?|@Nzw~E674h!Uo}x+(;Bg1FXqVDX5u~ zq$HYMy%}=$Kc-i&1jtC^QA&#NIaHcANbBM6+nxfrFGG*XS`08HJHL5881^>6n(PE} zKSl|btSwcOpW4>Nczn|HSr+)S`IroBEvZkmIyT2U+9vj<+OUZC6v*C^#FI{u-t@fB zXx+#!bF<_1Rv%YeT(k%{j3@MD1)+XHh(^X|)tNQw>$~GOqaq=Y1459OPC}iy;!6|8 z@a_e@BAS_pu}S>%_^HrDiqQg^Ri`>NG&*wy6Jt)l^OEJfT; ze;}HYM#AfbVJAI-n~Il+u%F|B42Iv_&ef_jYaYiB82XOd_s_^xe0xec&io9 z1lmdJ;soEKINJdY;drAiShpM_tsFM|g5f=ekejC3!KjCth@w5yM#G%1W|&t$M9gW? zEH5&8S&PLg1{gIwU7$K%lnC`zU* zYmeS2SDZTBFE#L4$)rd;%ku@UB?l)0EP1T*T9itzDYP`C|H<=lqDz`6hSf2LI8WEj z%CLP^(HNd%FAfvndNFcPnRA{sowX?Sj2mkZ$Db|}pPcE)2$J)c0VmH)0khFWG7qgOZlI;aa2lML{#Z9n_CjG#_hoG=J)5$O|xgA1T*=h)LyhdRm zJ6OS+B|i4q#C=xR=-ky$^=(mnvYZwz{gbG$_SK`!&%kh)vu;>2;#>Q6O^(>Zbe|Y7 z1KWf}`t=i(3-Q6t&~#g|GEqj_j`#%*Rn$-s`WUwY@#4Kc34wQ=7OvKbd( zcueV4UH^LN2z)t@A}scki|f9r%C>y|d-|nSl)Bk~vQ*M{zn8DF0F zy4NVRgjy@q(viYBcj=9R$f+G=6b`}^b$ve80AekPi*5m{e#YUZGrOD73XHiwcO7>( zx{EXlEoN6TM0dr~_hGlPwx96a#TCBrrzgst z0mnZ-GUK5bbA4%#e4Z_gAWp(Wtweq%glG=3F*V*5>Jm+ZBCH2xziXmNJfVN?z!cq) zG7x@jeofFoz%94($SG8sx2x|tUQu*1Co;9aq-F@tPzUGCW%8n+!SP@C7&Hi@ZUE zK*UY;9sgZ%F=`F0M6mK9{%^(q0Rf4CK{3#wf<+_$9{|vIY>0g>gYpW9)zcqPzUXC_ zK9+HPB4m`&Ew4WFtIBa_x0_owb)CW>iH4tIJ=Q>*qgz|G(k!GZVGWD|Oq(O(W#fOY zS3L;K4$2PN?iY4cPZtQKW2>eItG1*4)YnvhG{6KY#gx0d^P2_D8t53E%_K%0_tXSRrNsNwG~nY_x51{Z zwR&5ZUzprl)5hMCL3gS`md2&WqkgkJWJF|Ss-Tbig~y{t4k5z5*HU>>QJ3e6$m}fF zX^lQiyTGQZS2aTgVL8Z*sz`w-k-FV^Rwm z2UT0#^t~GDjzK6T`qf*uNagCeq)a{Xjig^dKby&itS3V0E12Ptx^mpH z*EN!~1>S%cMx`}AK`fQ7A41EE%I25eQx4gYP?9pqx*Hd~5(8^K4O*%9m8)BOg4Gp( zRRy34#uuwT9SrQ;v%z*A;fB?u8zbb{MS`2pwQFHIdZxS7jV;As7=^ta$hg#wjx!MY z=6v-&5gc+z_H-0StBvq-aM`)0|&#cVKgOU~kZD7hsO`JRn)>c~L{r+Ak(5NGrA5NsAR}|XUzEg@lp`4C z4NhkN`9TSS^U%}JJ9%~Q?qZsrEz5v1*cM*9d>-bPH{*seO1yHG;uK60vagCdNe+5@ zl0-UEzw(<7#luL-&6#ONYmJ8aR4=nOD6_IlncuutzltI%AG>iJEu4>v{9~(M);fyF zu5Du5u+*egc z=E&m8h0L3D7yzd?^jG2JpPZkXtY0c=@4-hgT?gMdcjZPI$33~k z7AUUH8n`vjp)3DdhmrbMcL7m_<bDpSDvHmdktwFIHyc4&m;cv=2G3&-PZ?k?-x#dGl*L=))y*#!XmFf$#+UE zc+2K`WW;7N^m!LJ1ut#BZJ&{Q{RgQmARI~EZe*%m*e$2}%D>B6{8_797s^`OXY)&S z%3U?T{4ApTNa8rJXm9x$AHm(ugJ}w7AoAmOjNpO1!KH8I_-R1l4$=D6kK*LFu(!rn zOcnY-wz&|3URrwRNH%c=RjX@jV!Al{WeMXo#pysv?u+x45|sF-7H{uv9&Ux3w3k(V zsU?T6b%0o0X_PXSt1B673Nb%dTcKxMQeq-@`BNAuAF5#U$mO8V zXyE@`AK#tOzFVqqR};xRA@q0>tI z2qN`G5EgNY-Sqy1O2~7;Ze)c>-lf6 zlzJuDh1fr3)RU-x?>BD=rBTWGr-E8_rv(CD&vigZxMJA9plx1P^^~cQ%fZ*g1eFhu zc`TOs!%mweF7-(VdA3doosThQ15oCQhTeFy$H)HlA?9XUJk2w1Wt+HI=xvv@`Gjw^ zL_t%l-Mw6i2<6~1qgcjks|{8vI(hg}8BmeA%B9+3l8#F|6j;63 zJoEjFN=xZFa#(x4eRd)=tKl(-1 zZ%?V8?~0#n=v^c!b^8~pd&MU0?G33GnWI{I98P`83XVnoQOIvRtddCQxmNWf{rj`g zW=SnWa$}Ei*JG=*@?x}EukXxpzHHQ5c}WEoVX5X*&g8J>oRq~dJF}Hnx-%+Q+THyZ z5~+WcH}`8fUwZlKR-9}``F+KyRW7c%KPg5;MKqu68jt(g@oeiY7$;>)#iEUEBCm^( zdhlN@ecfgFQsx1H@TaeuOjoUk$;mh%B(4Q;@wbh-!NIY3EdPb`yL>wK`GQTlw$FVt z+p&*yiF~W#ed~Ej#0(K9?ISI#e2^F;`?ZO&@j~?K!VA9gAu8Vy-iF0u&6e~LuJFr| zu(txf({VE_YEE9OsF+ydknutVbcK@tpat1fG>sjtF({dSZ@E;>2yC2uBt|G5-&>Q< z;9Q82Nj-liG}Y|Y`1un!`IE7pG9ZaVBPuj&uo>AB0h=R8Qq}C-ZE+y^0(`JTk-7KW0LL+N9WjmUWK~o#tw{`bHlS>o4`b>1TSA|% z!j6e{>{X712${7vx5Kr|X04-#_JGHVnwA|eg-r#+xe_}_CbnQpfYZ=hRRC@$OmrVpwYKmEuP zUFmumL840Abvn00No-EytZtZ;)Nq;N4qZ~H$6CW7c;qL&)CY zA$^sv%yS@kq1)~r^}br^W-({-rdT;KjQIJgTiWYI)(KK-DkDGb+Utyv5t=9HBL9l0 zUlMWkPksZvbSx6!<&~h7dVfLgoH_F4b3G~^xey7x59ruVX}tw4-Qe$y#?$Gn?L@Bz zdC=_63PJHygG0>Q|MS&gR35@9qS@~ihEx>={ABABO}!g~gDwnCCF}{G_pG)d^jPx* z%^BnXR{U$xNL!%^@2_z;?n1)vcUqtfE6>zg@>1*h{HS;pnY$VMftVy2;KS4=r*y(H z;jfkW+aNqQL-p&ikW2yhpL-=>yL>`fOB+VgsuE+x<&gqr(yW}a_uk}ZGdDvvKoJ0Q zbcnnyD_?c#_p6aO&ETVP-DQeyQ`E@VxZeA7==gCBgmj{hM-T_LyA$hHFaf*{&f6@1 z70Cl$^47g=BD~;$VXP*K4|GD1;>je~RQn)TLz48Q$rdC1>r1-$`*kcVnbdt*%Xx&{ zx@YfbE0f!y29_dD*gwH`WoNCM*z>Q-Y?q(IM#MIb1I5d0oLIaBICG(VK&;N6#?~MT6zmTQa@0qp9puvrO*N z7}CAChtI0rmxNe~1ujWi&;x-dk|9Amy*O;gXMia;6rC*k9 zSApL&r}b7l=ph1;&LRIqJ?|bqXch)hDb|kY%rzya(yd4!;J#F~c3TJ8xevVAhApT0 zijMBbV<_xXUq>Qr9)}1#WT};yeyvgJ-up-G$&VAczN^$D?}<$qEI z4&+BdUm{C>>|W@WlEzGaA<6p#Hms}-A?h|G^guH+=2nws(Psvc)MU3VdoLD_i1E4y^e5Ox<6mL4>?DrD1~j8zqzco+m+)?ljkSifSjvgvP~S*x$%X$+c)aL zdf;zFufR9=k2hws<5`1_eKVTmu4x+4a9DPWuDqA9FM@MF-Ls&tervm_ydSDm2!Jpz z9Rg-0aC`9N7Uox_xkB^jBvW4~O~RPSOPoCW`#R#aevXd=v~7g^-*{iV*rV=NZ9I-z zKvO`SMy8|VhFi^PZ(6xd2rHPQtQT;dZ5*6%X)U{1+k2jvo^h8S==;2?6@qa7Sk5n2 zsx-Exo9|1J(6X4|OyFPh96oDK>8X4Di&uHUoQV~vP{5bVzf?#?H#s&PC7MLt!8n85 zF8f_ojc)Qr_&%}Qxoz(q6d;Cm&AL?4S);}b5_S7!k_rLr*4P<;%? zA*So|7@5iUa};3}9zgHe^x+6_ICkQ{mKyFrl<)2P?L^4k;cz=B3EnHUJ|8?bmV+ZE zj7QoNpqEI@DC>D{7mC4(4~v+*^dTbGr;G2uA7^3oQYqC#7M<61mt`m@XbTKH#goJ=RLjQ2`U6yhFZ7&Ho zIn}MEk4z*#or*xfGh2w?<-i8qxIFfItJr{fVyJrgwOwOaP+)?%fauzAmS#3#W_`X$ zMkSVQ_HUOdfJgH{)At5~6Ny+wYbFVw#V}9x&zT$_`^;(`Box+i5yFUrdWxSv!Oqz( z^k;^c_1`*$h6KRH275ByaTLgl!ojzr@u$3DlN*ytepgBJidjuXMMicsK#WIIpjiYQ zm}K|wfp6=B0F3CJN^2Br8U*ldo9yirGFWK;(UBaRwATTPp zI1=5G!Feyd6L1YWL>H@`)h-K_jWw{;P~gh5lEY?kPon$Y!gvw=C`zOmW`{yxe98B# zh(&=q=4x12dNo}q+w>u(7h9@7q zdUU8rCDfD)GAE$hGhKs~1y461n?wD8rB!0(#^nVmK&6s{p-Hwzqn`<9qlX>Hyne!; z$TYdh^j3h8byU9GCsOn_g-hW*%&I~%VP#ZzIq&m@Nvw1?8JX~7F$RYkT#`(GWWBXZ zd#G6M@Z{IvfXP}lzycx0YNoQ8|> zZ?@A)Sgr4Ku|*J^nyWhF?SWspEoCaTu=9I3VyGr}34i2)JxD>{adI;MJZfSJl27HL(%Z(e8DO(+Ue`HO@TLA5`YUE8tTOqm&sNMRMT2@#;6|LGdq6c$0n+a zH~QBWM`rS+B~j7DPIWr2OquV*3zOdili58ztb;yZPAwFGr}O2S`8q%I$e*8iy=^uH zcR5GX;pz`UUxxTS_EVVY`|cwcez3^dn7j2^KTRPi&LAmeJw(zQ$q?E_M)mCvlgcGI zn>S^9W<6clH4Yr*Ilfd$FU;6)!1zQ3zc<}}q~D7m!Mqq=b}PS#S-dGf9FL(bE|W>l z*^V%O946ePYSCzX{wTzh$HOwL59#DNh;8BHc(0=quf6-2Olcl>I%#JK_uBlpaSy{T zzFAqMh_C#=n@y#+{#Fkk+lK|;YzwK$oWPirS~kJYu|kYGzS8u zud1yTeS?;ZRlnIz(<^R!cZV`L1D^Lry+R~OZ(*AQt-K~g*1e$lBq>p^!;%f#!(Gpo z4U)!grvju`==JkB)k1cuXXwUKpHVy~ki>MeOMBgiklnV%QH+2==_bLD1PaY(Unwpa zVDArpHwzHR!88bXz?io1-bn$yNI{PJga;>NmHe3!(A zqg}5Xp>cCEiVZ`MOlxEpLKhQoY?k>YFg)NXZ4|ze9BF~l&Rcb3Ec z9Ac$!Z|Q%G1m(Xp?iV9y_JYaVqh0iFNM^kv-jNtP<3$?A{={M9?D}JBnkJZqG0GPi zBPh0Z)Fs?!Md+k{k_sAakIed5XF*MNPt zQ~QyxM05@r+y~XklM(N3?{N3t3JXZ2_2eEBWik*$KJL5si5N?|Uaq`~FH3}snoWM% zADs`rTDhkgb|~q!iAu>A0Q%>joOC|BdQ|j_?2-3$ubV3RPF+%jhc2{L;af~^91J)zZ*+Sq^2=O|) zwiarF{$XF8JcuRl)|n~9Idvc4L889;QUcW7rM2@96m+~jIG_KSsk2wzKItrp>_e&> zBNbyd=C9Tin41jjx4dybTmAxygYXHFgvzR_BCs!|7~wo=8Rr3v}|W zX;eWuh-%Zl11sB5QJTb4PE$x{Fi3dCokMwo9!yUIr&AKR8>N5r=7VT*JBIk5;9P}c zzQcwXehf*mJw$vP;TX|-m_AAPY{NNw=URgQ4m;u1ln!B-$l`rxDmXUMD0KQ&QRvzG zd~h)LrZ1zb;*tE9iZx(1;PaI^cQ7|UIT%$Zl!EY9!+JKfIXYzpaZDaGp1?EsK8B%S z)EvEoKMEnrIe!XzsN1F%$EjbTemN;`vbjXmukvTpiHsb#J2m!XvcOQo5_7239IER1 zv=()kZMLNSP~#TEz8zFZ;+l8;*g2o>IHVQ?uHjygq4;Oos8MgyG3x^gUXuURB2 za@I`k!?BC<^j-_;Kr&44&|RV&$vmk`@9SuVdKWvID7!O2;Id=w(OR^*5+5oKW))k) zYFG1w3@7jxWs5H%r*)*FSShEU_vmVv;|+N=E2fimA)a(ykL_%cO|n#^+Fc$@9Moj5 zZrKv+>X*U<)?@AF3v>6c9fIeLRwo$?GtY)`mtT6YCj}tz8*Nu+O65J*jL2!Z`WX-& z4!b7(R?L0=$Y(7Kvx1~j9D8+}aFT<=;;cx>mQ{i<@AV&|51q5hy&qxL)~y0 zMmTPkO>iq7y;^yzrWY-ZW8ky8$1N|(5|%OAH@>_?8RW2VWLlDE4TVZ}i2W|iH#}q& z=ha5mB}^+l5}ixWFm1LXJH?}?NYOH1{6@ymGaOTu5CkbGi|s;W88sT$?OxJhX5RBF zL>#D~D|Ce^(>uta{R*?tgBWEo`6bb#nRH*h_L;_yn>EIpzFjIVH6n1CE3AT7nDf3= z{yTz)`uX?a*($F#`He)`vwc?)?6>|&5ajD&W%yJyjVXBf9{p{Zf}y4F^S6$p@cumg zUtrY2l_eeMvtR=6xk6%LU)cYmJ2hB?VuHjJwf5@w&1)A zVOfAZxAjGf8F51im}nNi@c{hhQTNA7>&HNIhFMRTz1IK(OJ8vsIt86yVG8ampl!@13Qh)Q;1c{@`n&-L2CbJ)5_q!Wz8XCzE@MP~RP+=nQQ_N2e$##cUcK;|dAgVJ(Dd~0 zSf$3WUzA$6|14{r$tYT*kQWIT$~se=s7f;?-I&Q_4q%|D>rJ zH0gS|J{jO~VU10TfT3T>s^@(RzT2MFaY@II zqGVM?@;X!Q#+M_#Jf)eXG3Z<9;m0%tTm*=wwmI6~n#oIBI+rRFA(F{F8(HNqt znMCAO0kFiOv5BwjZE7EK+ZQZ@gL=&lI7QF$p=`6ELKqahDlR>%Re81IwC&std+t zrhv4l@nmBTm{rJHil7u<(y-*hxtxy49{ZcAuPz5@VU+a7%cFw2B zLF2#Eo|oqWzBYEk2qP5`JRE6z+#mCVLmtv^EWW$E+W=c44%5Qd(! zdEwY}U)rGEm zX?upb4|&qLIlin7l%w0Hvd&3d9lw&*W=XXFnm4)>FLmJ-TBOP_#tvBn^cHeTmiuv^mA3JYu;1xA!uW?=rY$M?tel}Re zblOM8w7NNCvFyA~caJP4myN{LSz>?D0$fb`wXwC7=nmeK7?O=`&_iMvnMqUrYYEn`%A}lPtxrB2iyUILDnQ?!u9FM;1W#Rit zN?y#KzEq;q^2=C82m&g*a>cZ2$QKL2XP@41ABe3nLvL1zI{k7?9iR(pwm$fi%ksmN zmc4{arxID}r_|b1Dz7-^Q*KP;dRf}t>lX-kd=#BxF7X+@xLFCP!nGZJb(QNM7P#$y zm+)|~j(QH5W|0OAR68=5F#9E`rV``%-L#Y|ITCcyyx1fkH2R~ZwyyBe=La)lN9XXl zV3|qk@JY-^qiBlao_6eo299Ny#lSs(%}sqphRBboa?x>Yixggakg3C*%V~UaZxm)b%QP+gq+Eo=O=X%IdC;yIb}8G;1}`Kmfs32_Q2+86W?7oT$Ygfb&lgHwg$`$CI3iW49UKB))ZU(F_F67$cPG;w%R^N*_>%FyO(!9j1qYGt@b;G z7F<$iO*Eq<{xbA7{9?xj!^M0T0PJY+87lcX#6NK!8|@z$9il3Oo{wr!Sebqn&XW7Z zX1v>eix-@nS;G_K(6y6fZJ94tqe-gcv71Vl0Id-ukAbdMUw*YbKy`QxU-yT>x|A*D z?r+PND^g!+t$xP*p|#zhXj{l(04Pm;E;o>3!|{(f=!RH1Qsq+En%lZ4i6WS8Nt%eEnSaQE6C!>mn%$K_g4!ry^8q730}?2HQK?70$9X?g$?Xo# zSy;Y3Ow>+Y)PzbFIj?2K-U3&dJ)Ekzf~}i`DVx%(9hOmJwz6yfzJ-=CtN}s|II}0P zA4e73f2)%8ElMIc0lB66rGAyW{fn!-(981d=4X8MqC?N5nh1^iLuL4*CHgg;637VL zbXV-+W)tvfslkHTJ1<^OSQ1Bx$w4bNP4@-s8YwOM75$OS3**-QoTU%!8qp2DQjT(S zMs)d9D(t~3NVaYrvG%i9w`bGjFT;G^i9%QE-7}t7aWwSrzV6`=!VkAf@B{W3mJf-?aaGkyji-;({pe|b;{dzGq zE6IJM%9-jd^Z6dcP5?B!Zt}PRj&8C$h6ou@Nyb)MDoh<>STROMf4SdYnK^%q?Xwdm zFtJ2I!=H5#HyQiuUYOaS;xCd)6{gWxK1e! z=>|2~M#SuvDn!IQZcU~n>g+~j)mv>EnmLX|W>fl%o80}*^9XGVX*F8JjjkD`WI4{^ zIP-f1UmJrw9lNU{b;HXrZ1#gf8^m3!_ut~F<#0nt+e@~2#A=s!~4>JBL; z4vfd~)8#GL1zOCv$mmjXGOBl@;!-w18gj%T-`X+U#W{tWg^pivS-+~YoKw+h+#wGL zIZ_%?3DNA^H(sJw<#($A6MmQt2nvZZLggjnP;*D57LMDEcSFVmq?ZezeSl3t!}Oeh z5rb^V%(jh*XSs&Bi$fISc*z+@`v-b;dg{P1@GqLsh?4icnB?`2H+jKf5 zC$t1cfXX;{XrAb;Wn=2A@(nwFevy}LxDw*hF+TdKDz#e)paC56Z>_`(yn1u;vgr*X z=59SjPQAYlgba6HD#Ay)EWO<7TeMyvki_;}PX~HH2I7FNUJH3hkYvDSuNc1vnNx~K z97U)n20Rkar%oi>gVn8P0jr#T-*3L-Scl(g9|M@ynR+=u-J}D-TcKY-iT z64Sp0+u*}uY1{m&x%>oS!M8_pL<5C%MFwgkpDuKWTiH`>v!q+iE14Ueh+uV!jYO9c zu0!1c=WeEv3&Q0`!^1;UHuY@Zl6PgGS0EO$^Th}}CPRz9-><4G^0rsxHr+`^Mx1p< zw30n$X2-GxF&d7Gxq&B_Jf}NrJq)qm>fs2$r@K1S;C^2GPwz31sI6S;DU${rB6^26 zKi%sHv#)nLV)J9PcKAYZ373M-!Eky63W(>dc9ikRZ5>O(^Pn`{^d~P;##au{yY#Cv zeSW-Aw{KHp-;=_a`CKxFh6ej45|>l~uFA2++9W16sH=9}4CY=Pp{R-Wu~=vdrK~G~ z>9OS8V@}anU5AkU?Rf_dBP#JvA2Xa(1QF_QWE$-v<$CK-TCqURCqKo=b36k_IKl1O z)(bf@YSJ90FRK@MXg1DNt*2)yZ_93Pq>L6=h0?ZWdM7Dej3}n8v}wYcZ-2b#ZU%0V z^A9w!w-m9i57K+vxvFgYq$aR3LSo$J*WO2b=gqF)47XJ&_O-Gycg zvK3fLhcCUhi=Oyi0P3$+C6l~vFchzQTe;eUda&|?5C_~U>OqwsM>$fA`s#FjmLy^7 ztGuvaZNk4^KpUSJ)O2{V|%N!e8GCd17A5(k5_09C;w zQeZFQy#5b@6d#`77xdE>rig-h(LnB7q3lye1)c-DfD6$32<=uB1)<)4(TcwsO`t{u zij&!;NuhQ7hqrwqT{$)N3onI78cfQW4sEYij%<$@apGJ84skpfZm%~0pq-ksSUji8 zgMHg!zz8+7jtI#cMx_!wc@1-m4kF0P%Y+ua+OyD~{{Bl%5Z;s;{t{No;Qe~QuA(Dc zLJ^VwS!=`wNcIU&mGC|c9~n*EGVM-*1O${}jXHGSno{1p{_?i;L^ zKiGc$oDuM)#MtQJ_llO=a^DGYobVBI0S{DFeO^aS2{zY{8%78Y##Ig3jHiQEK7gf# zrGvgorOV~FY(0LxdLUMED;$VL9oMOt}_qRNye94`!p~0V;sL3HMN1SfbRl&~g zIPCv|r@G&2XMffj1t4#@P;HYTO6SCbEkjZt-5C@DfR7ZN-`Dx&a=y}%3cccRNJSD( zb}vh^O_}Z@V@8(638Zjq2E1YW{hrffVVg<+;CUJ6%Pl;MjM224b$g7(CRP+XG=eYr z?&stFOMiasZS04Nv$0`3cvb9oUX_&`nShH1)ag0JcN{m~W&539*GJuw-4mX4;@Nuf za}~7AOUMLk@DbQxlBwM#;0!XuWq51WVl;eGKa&#wi=%)Fm}ZDRpn|(-P+8= zh%TO-cm8zZ^-f%=r^K%>;QblZKZZIVS4rjSl{#5TrMsML?5VoxM&$aB9FxzFkh*JWjv;ynDeP1fyw4{vo&2T>a+^j&^kEe$X z#>03X6@tXxW8^l14>oc7ZZg1KvzNV}t$TUFS|Z49Gt+1}A#-z3!Ym`R1UQ43v*K+L z&as;3A?^LL5^AYCxd9&zpapsT>WQEF^D_0j1Af1`Zp$X?Q;?|RK3pY`eKfwpc_js* zdJ2CW6A@B4RAg|p)5V2MgvRs}M?kIxth66R7!@a|{cJnznS<4=x)_qdnC-woUGEj} z*soF#`>7y*d5;gpe4u3v7>kbjIwnl4NHHHbo(;P1{&CrqDB&{aYAtseZBeU~3NRE5 z!3T?##&V`*sGp3K4M#O=%#_#rwG3C3#{9}D#RfDfOG9r8vy;44#|*(i7L3d=+&qO> z6`(MMuL*%mWNgdv{qN6LJ0#BE0Kh|TzyXMEZ2xP!m?Z*Nb8xT;IL=Z{#q7QEyN`x& z!aY*Z!?j&WtxDUo(&k=+lBj&$8|uijqE?NopZ(xxig z8mu}J5zHPSgwFH4;5yIyM^+4_ZWW@PKpsqDxX`ed=E1G{CrTZsP$ya^ut|qX zL9W4B+T!gi%Ou8Ix%uxJ{|l-FWInW=8L@7g&Q@x`z55{`*@9`Q$Y(jmV!5@*(NHlh zgj)JGg;4#Sb3wmUt8tC+HCqV?RL6P$gz)Io-FE&k(8IAub3AnjkBSY5`-|E z6fe+142CH|gLxx+MW1JP|Apu+l0J3k!IhN3VtdbhYdaWRw4L+F+txIKDOH!&OnP4q zHoG^mP}_3asz8tyNEaoNj*MRZtr=OMHtxPyt-udxWJX9L&zAV#zzhnb5*ji!SBBR> z?!o?bfj$UBbs4%(<><*O6dJ=#gOK&Cm+yW4f8rp$WhiBkRa3;oy^e$+og8(4B;A^e-TcPCDp@m zow|b$xFD4WSn&pg1jM9lHx+t)0>{2*ELBV8?ND42Yc0gDUI;h}U^?wBsO0r%YCfAZ z7hI188*Ig<0J9?~`^HYCfY*o14AyL)^0@cgXt#f5%g0)U#>{&4_@^vU{L5yaxjR3n zW=s9h$w{M5P|S3~{>R?ZO_RZ%R-^8suEOWYWd7~v+mi)J(3r~Qkj_Ky`{4Nj4dkjv zeW`q>-fo@|?^V&}DxbEz7zkOi|FEoB<~2)178;L6<#8oVNHo}NTB`d6E)6tBD^XCm zSsA++1Rz^3;ui~MMu?jF`talxt{77rJf z#zEti>-J(p6U7G9jz`wI#bIJ%OWL+vFuAwMd-WB{sJUBINaO7=&ej97E(~Lf>g(0c zft$csyt-TwXD?5J*(iK+0!0)96aVXZZG9Oxw%X=@mNC8YtsX0Iaz6n2rppzMBA7!s zGNun%`1HV-Fd}Am+L;lL*}lHoVs61ri@?c>he>GdvoN;hk0{ip30b^K&r4U%lR2S* zAIf%efD`>lEhY-Z1Maul-8?2WKvuBCT;xBy$*2F$4e0Nxo7zepyLw{ynMtX(^im5M z#2lk?`Ne@p4RkzaI9?cLaM^wM23JI4AhbukW5Op=tuDsEusC7}8bS`295>s1Uf+>` z2H*wjRM0qH*q>dRfH>tsXD6h}^t2~3rd5MTe{HOI-&tb0qIXLJDL^J$c`J&HTff9Y zf z$mz2@c-?NT65k}9`u^iwodsz{MMb5}t`Wrk45!kygUk9VHKnn?w;iFc-@)9#Bn^gZ z2|?F`Lc$?(CKG+6ulrT{%G0SRgO%xw`!&f z=@rE@^&be`!GeAL)Ggtly(8lRm_@Yk^BHHz>7lOSdT0nmlfwK)wgIH)o0oVU+aej` z+m9;Hw+;+mkjmj@VZuqL=-@qO1r;j|>N1agbFk-^w6BKt%cDP6*18fH63LeKy#OUe z5-!t5@JrQqU2L@cdcD%pOewgs!1O9Q7-FRaI1y3yH;z z&?P4Fypzbz3rpZ3wFBm57#SgFIt;pABT9zuGt5U#D>J_X|r05UoaoEt; z<5%fNI>pPE2fWZM0T{E6e{^Y^XP|ct^|Bn1g+mh^OCLPE+eVp-Q(tr0@W=Tkayu}x zHDeQ6s~`rbIhg=7&%QM){#xC4*!{fVSkDoe>Ur4_>nf= z_66?zX*O5D7*&H$E8lBSmYAFPS{>kuDsIW6rTNdzZa>PPRmzrOUP|6N=j|uC)O63@ z!(HDfP!M60_^`*hRs+O~ox2LL9_{Vz`BoUP+D$HMn_qhR==G#|Hd3{O{m*tvlMkgb zUQ6|w6iZAW`BIJx(6-rZ@H!V9yDcvkKp_Lb>Py+EfwV>~>=K>qil(djfgCG>u&sE9 z`Kdk(BEF0$9h;w6cLy0Qx4rOTh~KWjSbzbyWq@%deT~e>8B0wEmwFROVP)pYzkc*D zs6Dr$`4B@aucbw0XPlZjsMb2Bu~)L&s#ID8UcWU{z|j{yw8KZx-!ZP0!}z}D|#YC4u*!D7BPO1OM` zwO;9YEZQzK0MK<+pi3Uazz!i~v@MoP1gPB56-|{X=hB%woL`ZnoE+s^YM$DRW6F6N z6FCL)Emd0vHD8U+N5-U(^AD!c)V*6n+m=zDwn|(xC*{rdXqAo9#U*brbk-JJ4=zCb z#*R4~)gnfCz4CFk*{+J`XcR+-j%m)8l#*a?G%>61<^o(s&P=ID=z05TwsFADnu1VM zTI;wS2w@?!uo3z zOR;!*3=E8W9T=hq>76k+9NF^R66f0YdCoax;TO7;djEbJV1f{?Kd--t_k4ys1Ra)} z?K<1C|Ju+$ARxl(Yc3?dzO##RSJ5GgJDy6p7FET__$~2|^M_MQZqb(5NVO>gfG z9368`6ewsc6YFfB(PZvav=0v)qjv@mN_+58j_8wG4H^+Iic5a|ZhMHuPEB(&Hr6DC z25}vBTEaM|6nj7Yqk2Vuf!fRZTys8zUG^+G3R-r-wfZV;_<90Qd6PbcMvUM~w4BjSxii4qgQG(0r4fHgWdUPSZ|MPQbEV7nWBBD z4)GAxdetEFwfH{`MLfAo@#URVz%QTRVp@WxY1!gNHLF*|lQp!=J7*@Fa2zw?oq`wz z14091C!Q4?jB9+=$u=@d_Eotao<5Ae9BI)-@H*~ccRk8u4h39qq9Qx|u{M|L-(g54 zU%Qd7`1C(F$?@*od*6BZ@`@e>#0(poK|Eqd@3Hj?ay>5v+f6f#BrS0zZlUGDpV2DV z-oJ-2F0$Z0Eb?1#DRUV(-R0HGTz8|Hlzp;4rx*n)ZZUYXwuh}R6>4XFY^7BrO8(Y3j=-JEV;DfqoMExd9suUh#eY9V;WHQF z-Sex$QD5)SlZdq37;LNU+u2Ch@eb(>C>{**ekG2K%#-^%;8gQc7;4GmM{Hy`yuWPj zISBQNeM7hCjcDvA&(zd7n9Q`6nm^#f8moAFMKE8DM%^0lt?s3P!2GZMJej#btD_a) zm4Ytn6ir7*!kuf>dG_CymqzV6E($xKls`MBdoqy;wA4QxUwZ{PdoFIS_jM!q)l~#( zkgD@ukt$W%dVGqWoo79W)#_VUT0On6=e3;=(hKt@y@DPsgSGghNc6*_6icRb3;#D? z$~jMFZz|`q2>6?wCX?QLG7e2w)k~^^igkERs2Zd71G<9KR zReYrUVh+)(V|mtQ1_L&l*wD#kl9*F;F)2TpGo}aXg9$6%n>i& z>!yEWc%JazShVfttH76egyE%NhQ6)IepIz@_l0n_da;>@xexQw^eA$gF@t+w7r@l&7ns4UoPgABBVi z!Tv)JpeL6<_d0q#=_^IsI)EzEyHw7Ev@g{ych{TNsIBrUu-vcsUX|VrlHoo?w z28-F-6itUIqN8>i6r=Yu$-3MSjg*5^Yn|zBj`*_$7MH!uo)dq+7X;4v?nm=DT%pIy zIsVQT%ZCXcYx|;^Qy%t;pTKNk(wv`v%e>@=Ct%-pgZ2LH%8fYg6W`&D=+u68$Zeey zc=V%+6Ks#yaU_yUlmH?F3@jYFyu3jAZtTSvmaaxq&D`3+j;Xdo*qiCI2|~2e9^O2M z=>zOAhNh|3{kd@sS=EXzA>A({jVf^FSVi@nIBjsj65=0Teb6zAlxAYST;S$eA2iUT zh)P&ZaA}yfi#JuSBM`#N6=H@ZOzkbe&TzY`VBs!>l zpwOad5>ruRWZHEl&Zd0OUI)mVQec5S{@fA~k>?!9a^S@jxut~Aw_{Pvm}wm{f^&PV zG{Qd#xj^Gbui32E7?uxlE}B#s^ww%wfXMN?3x`c5f{SW8bZ-H5C(~WWJN9}9Y@)-H zX0*$Yc1pogh;6P*8sxL_Ri2A>3wk4D6yfwmnpxa0J8XJJHdKugb{Ykj*P5>Y&GV+g zh=*Ki#q0wOhlQPouZp#*6;$Z7a&GC0v~z=$yoBSoCX5YT&e16C=v|0$FS#*qwRy7( zvLsr~i{(m7hZ4D@rWkY?-u+gEsh2d;JjGe>S(IBMK+2w!q}d7cv)f85dI}0neetm= zxbS2qC2YIxM*K1&UYlE)_;#?=*q*Qk-}t1rk*mS6Rd+%v6`GjHb7|x(f|J78j#k5y zbzz))?LU6W|7P>roy7YIEaFC-cUEmJ8)RM)X->(*u;%3KtiP>Iz_)0Mht=)OV#i{r zG@u~nHAH1x8J1M%BTahn`Q_)*yyGq)lyG7$u`40owSDg7VNzSqFyzjy;o?!6Qu|Z; z0WqYrw z5EJZZ9pUfj_Lu&&&HT+Dq)$#Qh>D)*%1BWkMfc((EOS_DD{Cv=bg>5Il;+Bose0y5 z&S0Hwj74A+>>eH*#G(Y(^c~K7#$H|3R2<)ArIm=zvFifV(-dGJy!@?{7nOWx6JD>X z!y0;#;Lru0_%vhdT}bLU>3&kt+23(#ZsE=fLBYjGJ$-``Mqzx?uI?U>T*%K+yeaO# zB|%9e8DasL{z9x?TU}aYh%rf@QIK1!6UWm~B+XZ&Cv2qpEc^5u&7>xCq+Cd8kv5y6 z%sT*b=OjQn*Rf-@3!EbH)K)oHqfdlfIgW0=_P4$#@g4hT#JtlN_&j8!UiKEW2?2~> zobJoz-5mJNtt!cc%}$rg9cmb={SSkW@+UJd zggY&l^lr+3=2a7d&indWfbOpSpH6TVv;y*0>%)25|LbwrZ3>;3s!o(&9_4>M{x=tT z^nCrXDc8Rf5qo>H!j0*8sr{!H?6I4C}xpkqF}kjn5g5c~@U zy;lrIwEwtbI-mJ|3IRbR^k^ICFlagSTMdIrD)o4%0F>V;`znz6rwV3>qV34E=iU- z?f~8s{-*xV8BYP{r0_k);uHe%snWfY)BYEokgbwN z(F|(45+&vx-@n`>eh&kMhqRIsph?j2boFzPPaX_hH>rR; zA0Zvh25RVc^N%`~esl5&_su@f5z(WKpD@OSeK~RXz4jqTk&MMbhdwBm_Mryhg#&;r#FMZGSokp_O=B~eSgf(03{h3YvzdNV%EPJBy z>Z+Tc?9e!R`dzla5Z=b`ryZUgU);lS;Q{ACy%V;=QnwB69s#@O&`g z5&IRtRZ6q@lWN6ecn&B91pXtU|NKZxd#Ag9_G|#m^HOUWQN>?YQa@T{8dx}>`lq2K zp|3UOCmoYgsbmlA`H8+FGQzXn6M^qVl96~!W0^Ol5|mMiG~7A%#vs_#Lz_vcSSDj4enn)_CPA1iQ=Iws#3r~zkxO3>khR)5+ z$#dmQPfkiWIn_Zuid;Kx@FSV^Zj*q~9HHK-dyu9lFf>q&sF{J2|MZ?w-X+k@V!3$D zLU=DqZOG7Frt%wp=ibl}>zTv&+G;xShdgY?a$kWtDU#I1WrmioUzt|Gni&M}+WxL` z&Re6tR%9VUf5BSNwuv|Vf3}-luP2Fg>8$3@v~92&$Z-+-8CuWMpQD|Vpi!l`#x7h< zJiWNAaQ7fAfe*;W99qA<;N-F+ZASNK?loKndJsAvO+;S{I3p2k+hmHgw}W zTHZ=(y`prU*S4cwMP0zR=b>z?xc5w38AO~hy9ksh&Mo86mW7<`>qal~pU1ddM5j## zZT9c%GDH>BFq3n<4j=w*1FGrrWV~Nsohj$tkrLwbjJkkc5l!eewp{)Btou%d?gTa=s6B4mKqZ*}d~u`Xs0_uXYu=bQmo zs};I|bxo=xmbX`Rhd(xee?<&kAiW&k0x!CVUU^(jiR&;i=+roqh^DMX7~vqR!*kYV zIckl2l%XeS&fv1{M#fl`bS0*$sAqv|k04sL^)~s$>CH6h(Yqh25+Sik+hf*C*=TNw z+`-NBCz9_GbQWmLfH+8g8^sCAnW=IQ4gr<>9l0MD=jyizjx2X@SbbYSjU$pB2Oj#a zZW@bkJWAK~6bEZs&#dqcz!Ekh1%ql#y0X=d-CC;0KeH6K{OOpi7daJ-Xq!wZuQFL(&!6e z%3A|zeu-G$_V5bWU?BkQYyMYhdpe~LelcdOcZpcPvTEz~UQnZ$DxRX+nxd{|9iK9% zvFjB%b%Ivu2*GW>w| zYg1b@8)e|9E}iybC-E8Z$AgFf4gwQWDLXlXy8y2;7J$bu#B^STs?QO_^MCs1nV4`> z*O)dp$tWFpD`a-2%A(gm3XpkY!m;+2xnS{Y7PmY;&`#vA+ z%%qGt^1$=*bnpGVvg|p^j;DMrwJwE_o+ySDqKH@z|86@Jmq(Dr+hWI6k@Ig&kne4X z01VWu;0RET!QCrMpDS!=P49Fbz-8FnJp&Ojy`KoW zz}S<>JSetaYpDBmb--^HcJB$uKY=wZQ(WSzQZ_K!fjvF7@Q!N4=6pbNj|^&cQe2a2 z|B1i<(fDc#&}c1k@k7qThT0>8Mr(OXxg`%s#$t-Q$u^kDxJby~tQJvbkL*UDS;g_( zN+$5t8b}pj-V^-<78@&GUS5ZllWL0rB$nv7Pp;DdfeQ_?P%Iq&LZLrdgAwGyj9TOq^zG5x>Fg%(6DTCa7vH|FcW zy(OyPp4e{o`z41Gf_n!>3x31NDuJRT#pnZIe@JjesFw*ah9Fg!4>gkS;&Vj{3%eyf#|P9^&v zqDg#$WpvfqmdnzXXZn9Tlb8%YYX0)>ZoCo9*X{+|SC4Q&%%+E;yP$}<)Mt0H;R-BJ z^+|rjv>DAi!Xq0@A(nHRkn%R8}=Yw4bSiddKYZc+*i zDUYWiCWfx*V)r7wvG_%^?Dn=(Uu|4}c7`7gFQnzcmfpzRhI51H|agdNn^}FBG-U6?oIGCo}JeJM`%yTa# YoZvqwjyvObA8?ltkrgiepy&I40GOTU`2YX_ literal 0 HcmV?d00001 From 9c3f2b407acb3acaee1bb23b3de4786baf8475a5 Mon Sep 17 00:00:00 2001 From: Adrian Palacios <73246657+adpaco-aws@users.noreply.github.com> Date: Wed, 16 Aug 2023 19:18:22 -0400 Subject: [PATCH 2/2] Add Rust package with manual tests (#127) --- resources/test-crates/simple-test/Cargo.toml | 11 ++++ resources/test-crates/simple-test/src/funs.rs | 35 ++++++++++++ resources/test-crates/simple-test/src/lib.rs | 57 +++++++++++++++++++ 3 files changed, 103 insertions(+) create mode 100644 resources/test-crates/simple-test/Cargo.toml create mode 100644 resources/test-crates/simple-test/src/funs.rs create mode 100644 resources/test-crates/simple-test/src/lib.rs diff --git a/resources/test-crates/simple-test/Cargo.toml b/resources/test-crates/simple-test/Cargo.toml new file mode 100644 index 0000000..faf0c68 --- /dev/null +++ b/resources/test-crates/simple-test/Cargo.toml @@ -0,0 +1,11 @@ +# Copyright Kani Contributors +# SPDX-License-Identifier: Apache-2.0 OR MIT + +[package] +name = "simple-test" +version = "0.1.0" +edition = "2021" + +# See more keys and their definitions at https://doc.rust-lang.org/cargo/reference/manifest.html + +[dependencies] diff --git a/resources/test-crates/simple-test/src/funs.rs b/resources/test-crates/simple-test/src/funs.rs new file mode 100644 index 0000000..a8155d9 --- /dev/null +++ b/resources/test-crates/simple-test/src/funs.rs @@ -0,0 +1,35 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT + +pub fn estimate_size(x: u32) -> u32 { + assert!(x < 4096); + + if x < 256 { + if x < 128 { + return 1; + } else { + return 3; + } + } else if x < 1024 { + if x > 1022 { + return 4; + } else { + return 5; + } + } else { + if x < 2048 { + return 7; + } else { + return 9; + } + } +} + +pub fn find_index(nums: &[i32], target: i32) -> Option { + for (index, &num) in nums.iter().enumerate() { // coverage should be yellow + if num == target { // coverage should be green + return Some(index); // coverage should be green + } + } + None // coverage should be red +} // coverage should be yellow diff --git a/resources/test-crates/simple-test/src/lib.rs b/resources/test-crates/simple-test/src/lib.rs new file mode 100644 index 0000000..8383971 --- /dev/null +++ b/resources/test-crates/simple-test/src/lib.rs @@ -0,0 +1,57 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT + +//! This package is intended to assist in manually testing the features of the +//! extension. The tests to be performed are the following: +//! +//! 1. Run verification for `test_success` and check that it passes. +//! 2. Run verification for `test_failure` and check that it fails with +//! "assertion failed: x < 4096". +//! 3. Click on "Generate concrete test for test_failure" and check that a new +//! Rust unit test is added after "test_failure". +//! 4. Check that the actions "Run Test (Kani)" and "Debug Harness (Kani)" +//! appear above the Rust unit test that was generated in the previous step. +//! 5. Click on the "Run Test (Kani)" action. Check that the test runs on a +//! terminal and it panics as expected. +//! 6. Click on the "Debug Harness (Kani)" action. Check that the debugging mode +//! is started (debugging controls should appear on the top) and stop it by +//! clicking on the red square button. +//! 7. Toggle on the "Codelens-kani: Highlight" option in "Settings > Kani". +//! 8. Check that the "Get coverage info" action appears for the "test_success" +//! and "test_failure" harnesses. +//! 9. Run the "Get coverage info" action for "test_coverage". Check that all +//! lines in "test_coverage" are green. In addition, check that in +//! "funs::find_index": +//! - The first and last highlighted lines are yellow. +//! - The second and third highlighted lines are green. +//! - The remaining highlighted line is red. +//! Comments indicating the correct colors are available in "funs::find_index". +mod funs; + +#[cfg(kani)] +mod verify { + use super::*; + + #[kani::proof] + fn test_success() { + let x: u32 = kani::any(); + kani::assume(x < 4096); + let y = funs::estimate_size(x); + assert!(y < 10); + } + + #[kani::proof] + fn test_failure() { + let x: u32 = kani::any(); + let y = funs::estimate_size(x); + assert!(y < 10); + } + + #[kani::proof] + fn test_coverage() { + let numbers = [10, 20, 30, 40, 50]; + let target = 30; + let result = funs::find_index(&numbers, target); + assert_eq!(result, Some(2)); + } +}