From 06b8c7fb46268039abd842ea9ede986758c7b9b7 Mon Sep 17 00:00:00 2001 From: Kostyantyn Vorobyov <kostyantyn.vorobyov@cea.fr> Date: Mon, 8 Feb 2016 11:01:41 +0100 Subject: [PATCH] Minor corrections for e-acsl-gcc.sg section in the E-ACSL user manual. --- .../e-acsl/doc/manuals/e-acsl-manual.pdf | Bin 635747 -> 635741 bytes src/plugins/e-acsl/doc/userman/provides.tex | 71 +++++++++--------- 2 files changed, 35 insertions(+), 36 deletions(-) diff --git a/src/plugins/e-acsl/doc/manuals/e-acsl-manual.pdf b/src/plugins/e-acsl/doc/manuals/e-acsl-manual.pdf index 7a0cc6906e73eed064b795bbf182b7c861ce50d9..c6cb31bbdb707182f389100e531595eec6277a48 100644 GIT binary patch delta 15548 zcmbWdb!;C&)8}bsW@cuJ?U<RFnb|Qjj@gdcF*CChGbhHFnHhd&X2#3&?t81<y^~J5 zKT7)O+f@ykR!>#W>>ki;9MA-XfrmkaK{i3H>_c#{rK3MW(g72C^2ux57+tU0M|H4O zqha5960<q$8<nV)7CC>-rzJx&yKphdm!zc#<h|doAqTM{m-y&J{;VVj@#cPc_E2B> z_GQdUxVzv=IC}=4IweL|ieuC&W+LYEH(8%v|N2qIaYV<L!rg_=xQus=?kC(g5An(^ z)^nb>>yv@%Rxx0TtDdj8vHBE0HNuA8TF;(>F5i&ZIv+!dEAunpeyqAREB;WA=gV#K zW=Sn83!n&ewUN1H8GOvKW_)9z9`WY+jPw~TmHBwPdPxx8^uJ<F$0gl-ciCTaIvl6z zjtu6hW&J$YzuYu73V3>2%YM{$Gf!S}GyhTT)!jWbX9QRT2SiTsXj6XJ$Yb$vGILTi z?e>*-H?Cj|27)WO*;}<b9$3+|QH4<Uo~}^WU4M`mpilg*6g1(cRa>qLw{FXsiCrG& zE5nn;f{uuZwJ{fPnx&Y)J?DGZ<H|p6$teF(Mdjv|vmQ>6h@n139ahCoKJQ8)B7`Y- zViy1#dk8SK=W-_RDQap}FFx)qU=VWAXO%gwzV68)KuD+haQLWdjm_x`FtNZy*DUz_ z9l&A_$wR{xB>#1Y?kZtmE+;glo~TyOz?hPpu7rjuA8m)vr>kcC+Pk3$;`dZEYCiSX zUR;0|70SG-Kr30?q8%Pb>mT=llEr6F%SWT)CkKZA(@~<iT-v@d{-LD0hK(mbYq7)T z*{bxg6T`!4Ky%Lpw*x|kO4vn1$FJ-OaR}fBy0}kmJTSc{75guqFHSI{eN=eTF2vyw z^oN4j4n)36gG01sJJ@y8aj=(z*L0_-<n)Lmg~SUlxlry=1=##CGYL)+I8IMkBisxe z0C9B~hBg3CE|ic+DMqB;z?d~5_>8?J(&F%{fauRxuR3V|QL?;3PV41TYMp|?NZlU; z$)+(nnNkvFDJY^5rbxDYrY=XHJmTbh>mM#8H?{|H(N&e*U?a$z<I0s?s(@yjx^;^n zNT@FGtVTgwAFhO&Z$2mr%iFz*$~5K)bWYBwT)c^VRqhS)?_~Due7og4d-372Un16Y z;x{EaA)bpER`A+xR&Q7Al<UUwsy~IYL`3`;wMg@NT-Fw3u5(UvrOu6=BO5{+?Y)K! z4k1(~<BrFyD6Bk2f0-2&aTVZ_qAQJXPM390QR7f<9{mk>wd^+o$KP$z*=GL^=&Kvx zDi*X1mgm*X2Buz^Wps|;JM$00+A)D{f>4Wl9yoNgPLb_(&u&~dbk&1|P6<XjsAs}V zvf#WW)3Pw7l=UMUOimdNR{KaWXeutD+#@idkAG;eCBO=#Yd^pIVy0ZqLSW<b$V;va zLYqL1-%QbLr~h1|jD|a)tM*(1&Ui!_r8s*90?Z+OwZEMlIG#M;R8<Y#&hV|8&G?A{ zBUae6E2xwC+cU9Xz5>o%O6HU(8aB=aH~2)+(dqQ>0SpvWN%J|<l3~=d?lLajhLp}x zQb|hklP=!1)I&=7bnpdAcYhF7f^u*BzH}69$Gh}7w0B<1<1}j*&=|V|R}b(Ay_b@C zkytw;<5397>aPI^z4TOKcLE6DAbl5~DN_>dC^w=_#=rG*v<OMs>}%3+r$yq#Az2wY zU=h-<1%BvpMzI#+S9<d-2uv}UJHX9CanWvhtGCV@R$gqr^jj<h-z8f`KeGP#U4q;v zk@e#&DQRF@f$B@4nI;#Y?&Z8Kufz*;KoRa;WbVzOU!;b8CTn7b(ERl()wys`ML#Hm zxiNs*)3sXLshOk}1V`<c4A17=tdsaKm_2m|H-1`zw_p)oKa%e@_Jd~2G5A$yBQ#QN zWWR{MRp+}3-!KB-RsrwL!({iLQ_HbNrIyF#jSV@-(uX|s8C4|!!bauMKf1!CH5n?B z1ri8crA$ljJA_iBQOXP|E8A=h{A*8!ak2gVQP_|he3zuWe^xRMvxOJa*{Xw)$J7b6 zzu&XEh=D*SzVwU#)_kh^EU}%fdf1<6rvbA|wr)tbjPqF4i>~`qkHub)xG@~LbSMVW zf@e*FvB3v{TQnPhTg`2H;rYk7)N<d;c&`xs%9XcKC#{FH=RKr;&(4ty_lDA;Js1uM zSenslDNJoO_CLjW#(mJmF+L;-cY1#q^X7o|*>p~i`k_=C+5v53<dZhSqHKyWiAFQ> z-rozC>kU!WP=OOp+IC+RyP>E9KB~gJiynzS>bLmE;YJb2lY&IGkj;63*CyGD4;Dk6 zIX)bqXu-7jlZMRyQyf8^uc_$<i{ByQaNh5w%R#+1Xp(y!$3^qZDzVqj0S5Z!Yr07m zQCVKOMvVAyp{M_OR3#LmyX_YwrSB{+)D@g~)f@KK;M3#pzGphP?;qLD%fll5e`}Q> zv-v+g4cA`)RhcihiuIv%Vq$scw#vP-on|nb+lEm>MvaDln71cE)zVQ0V@1%o%PWc! zwe*~Skv8u{|12V8VPfA{ZVuA-EV<&NIEHF|dG27O-#1AeD8WH;al>`2b3$}QqbmE7 zlVUj=&?*0QPyO4|sC2Pp4(V-+!4t;h5V!Ab=<0+y;K-r@+$IH@e8<H5MqeQK_{6x| zw}E9Wl_QEAM3;K`CZp@{Shzy}qjboC-aN-5R(Li&<TNR=3yTq57v=@mHLFy3YAD=9 zm*^I$x2z0$F<{A3&^*Q#RYeVs!7$gWr+IEQP`KN1R8!aEWoGf!YNk?pTbf6(4;2Ls zr8`^**e)ZhaONXBpTIeC<eP&)8sHRaW;Pa{g*fV(d_2ts;9=a8{Zt_;yGZAsq7>mp zNuAW$0-osNxa0gff282RW*xk;k-e15D<tke`GQD$+h5WrTZ_Qy&1$j`T322Jh?SgO z?beFmRluJ=o5%ZufFbCMKi#jQY#~>@E0iGsy4iJ2w+CBb(R4iMQxr5Nwzo5y%60#q z)fKLf?2KzqOA(<_-VHU(+lDD<4&xe3_6A4<f`MVFZzStV1gewCmifYFg}AT<kI(AJ z%Am)$aaVk8o{e*hCs)%a;=%tIV%gDdahyPYi-dRN87EewbcsVhT8?wa8IRLXw)Fx~ zm^wVO7aiw(m$}qODD?DxN9sa3XWC9<$*2rbJKPnuw}M}eL-_Z72#tcq3bkYLBX>-a zi93ItW=SyP<_OFMjH86(@|srF$}H&^UvJD6{qXIE{3P)8+V}!PyFb>dg`TxisTeD$ zO%ovixT2znY~GngI_y4zX^X@WGzkFMWT^?*-pVCRr*xrGsZM>tEWGiNZ<_vVu(-nY zNPbP=3@mlN%sG$|s!r{u`FJIoDZ@293r+Eh3~Uk)u5it7B2nXVYKiIff2cEHTl*KK zpOanfzn5ZW7-%KSi0*dqm>?)58Iv$&LQ!(VIHGt$9kv)A#;_O_c6$tve69kw_#G-- zGc`ewA={9MZV*2xmX2<BS_eAb3%Cr48qffPGPY=OTox^lQkWBADi;E@s#Cl^+TT9S zky3cL=uk2J;u)o)KtW>#+Xx~j+XD>N);X>wU^6D#7ehH(%#_QJzzLrE+v8aelQ$?| zW`7<o>5b^7P`uak<A5C$LI6w~nNH%fT!k|6ynON);qfRkp0rL%^@>Y{L=r%wl5%%! z_eLDutZ%!ZQn_IZA-P)8a>LhJ-Vu@yoTT`(8SwI~r6;ObH{nZytq0=9C-}M{g9b-o z|9q7y1;tdgeqAPH@9G@g%*JtN|D@}}4$8p&<=QBI^p3B;{SHJKr2+cZVCG&oyc`tS zqFD;ym&6&VUaBNN23xdNQ>|g8II5G^vWvd%KpWioCmLzQ!S`4W@}k8|?GUCl`Io}C zhaNZ15bGJg$Sxu8k+7$M$L@(=UtJ^g)r9zYi~whjAr@N7hOaJNwr}7?(FQZxOe!&P znbBr+wF3>+XsPj=gaAcC+MQ_}G%;Rak1rZ_|Kkf>tae`jiH||cNEAMrA)FnO=P(zd zD6_wh-{lS+)z#c;(W$ef&}7P3vwzsoW*OXGpG-P-!)_wXll|RQa^zNm1a&`!s_b?x z?5IdQP*t+QnkdV&QJ?YKobj>W_)twW<Tq=_%G!Cy*~O6|GT<vA<8c;zm#`kBr(*rk z15GA-_{ff*hNbtp-Wm@>sDdm2+0kU!<#?>|d4|QYQs6U(O*sr=BovzXi+hO}`2t<G zM26t2w~s0Z0~+4d6&{!(30)MHWSz5R<5Md=3Nr14eJk%8P$k9wp|WVd0$<y6-exrq z64aKnQvbaKVkG~p)=scDmO@h|4G1m;%fVJRy6hzs;mDPPBV+PkHuG<Q0-OB=TN}2c zNl&?fqKDw-NEbzfrUwY^6V?W=JArT&EIQPv#q~!HI)t|PDVLeQwyw6qCC@#{bj0Yg z8Zr#lhf7{0W0CH^`P(&vup%Bk)5lg;d{DhoCKnssA0EQPxN}EV3=s1BL`u{qaMo~z zyU}RILW+ipSp-jvqA^*w9PZCzP6mXxjUS_WC;YsDKR(wttH4txF1}Ek?u5mGM48E; zpJ_?n29vcgRc*Kb{lrAJQ|-ZOmc;jJ9~GA8rS#fgVls~24+mpB>(2+5Tiv<cuY4$7 z0YK^8UjF5;1CHmNiByHI&X?;0C)Qc-Ne$jJ(btE8?0*%NKTQKt-Lw)^E&2j!pn|o$ z_XCeko~5IwGQik+C5$<kxnlJ|Ow<Ia0DJ4|UZ>FO10gaV7TG`7{t-2tgF%Kps}Cl| zh+yObH4=^W5QBK&%whTC&F;doA&6U%;KXTL)atl>afIN2!=FU$n~U64Hu4`gSZ1c6 zh2S(FT735`4K{0ZuqNnceke3JkrVIc6RqxiJz}-g8UQXdnymr`39biSerGFvX_lP5 zfvZ@3Dh^ApeZ|0*T#;%!pgq`);q-@L7jvC;^24v~${q1~-lpgCG8=C*!?S2Urx<Eh zgM|fdj-Gfghz9seacPjI=6C2?{y`aWuWgMkeI;=9N)^afuuxka1~`0!*0WoBnF3U~ zI55TFB!J8yKURf(3U|T^A!j1Yy+L0ecY=ft_lMa`TDO6z_3bqS87XLE#Q;{t36Z-$ zCeiY3a>9`Pdsqmypox@8ml2Z$WJpD*{6TH`6*%#z*r#5z)0o}R>Fq>Whni5kllQvT zTkCV>`Vc-A;#o>(*-un`GO`+{TX3m492e#v@c>_pT_-Eg^+3*N&F+eqza2eu1{^do zbItdm&83Bo$yS@NZ$BuN$O8AHhb+f-{UFqF1x9&1l30ZYsik>~dUnp3<9DK4XluSw z)PQ3g8^LUj8yi+K`Mhszl@HtITtWIhX7~FVU5L>Cg!1#%mTL0jpfqy1n8vE^r<wej zfd(*G^jU&3&=%rTRB83={yZytgDpxy+o6Vb`nO)tBwDv|ZC$sO!zsnnVf?7*<Fl<2 z{}aXk#=l^tepO9eS_eq4TlC21Re5H^rFkcEW-3ot#KgaP|Gs-Nuw-1e6WkTakqy7T z2toOa&&+jo{dgu~MEW&R+ORLH02|83iylb7LMfFVIf5xj-uf|9l{nX(2zKLtO}=%( zGca=Ug0@wwmE6?}1&YgSF~DRvU_O$ljW@x8OW!vY6-!vY&M#a4$s=f%yS2mK(ITtP zk_)R;#p%$Fx%wC-o$P?LY}c?tw${SAQnKH(a&hU<^zyahy~Mhq&-cD2VQ!m5!wGQY z+m5kYN|9#^l_yEwC*h9E5NL|LW2m_v;b1YVjw8EpULkj^ivg?dFi7w8?=S8ZyA@qY zD>tf85U$&&;tSeSBO2Ksvp=*}iyqethlL_6Y*sOJFNYH0_ceWhY(un6W<{f(=H^3p zFT%|#zz@=pvY>(KtKAm-`9pD~02P=?kfqOnV~aRMqz_v^{;u!fT@FoPzHVazi*!=- zb1Wp)c0?UE#UwCNkl9@e+h-rlRPPZ<;e;DjJLn{jNmzI+LJyAaPBPRvMs)g80Ir)q zft##emw-iru*3u5f%&Swi&g@RN2bx$Zix%>4B8D*^<<rq<Jdb4mMigE0~N68DYur( znHIr7?(ujF(&tsc;>bO#bf{!5)N~1ycIcM}EOvgv_5Y~ba9<Yd{u+}*gV-k`;X&?d z2aEJWEWD!Yk~X3EnD^v~_pmYo9-MoeCAd}r+%yv$z66fr6q?WmR-k^HS_XqDzF<IN zQsfD09mzZGLsXWTMKK`9tQ_br^qfL{;2KV#2yH|`0)95(3OcKZ>2nHQL7*aipD_EI zdmiOA-i+Mr&CBM(iyakCXTRJszc^1)v7x3PtJPARNew}<@O`hD%R|UgEy*a2jij-O z-H=-qZE)RQ2CXg?U&)eWW|F8m?`Y>JXZ=w^N&4`yX*0=!?lY=Ecp8XLl=DYwfgpM6 znH?HTP8Fn<;FPURt`2^nwL`Q!y@fkbGY##elgy2v+KiXgdlOEahy5;+BkJNwb<5%G z?{qB7dc-ukn;E@2aAeDASKW5Q6rn>;1(ld?5w$=Oisk(`k*Awj++7Y*KE=i6u>dIe zNPCg|%%XOV&omz#zXl-PI`(9#myW)m*OX6T<$<{xm!A2NSNAoIXASY%a_s0w8cM!H z-y@#z5KCpo!3rchC6;|XWgX=)4;xv}aPn(dk)Tq!hHPeTe%;MHs`KYgWRoFoXFm`@ zpNe|_ZS5kB+%&<VkY#`4{7C7<`y}nHl0d@r0{cTOUB-*lrw%xW9v=F$mef=4{ZpBm zYV615Q4P<0py;`uU3bE*wTmJnIj4u}FWacBW&*dLI|)O86}aIH`6$b`JBvDY?>EHJ z^6^02@%wM`l+C8)oQaQ8>N43FJTA@K%jtL#N07hH(NGBSAy+z3yEs!|F3hh4{r!i8 zh4Y5gp#4=qMNEKZ;;T50fZ6fu7OT7mf#Ec)T5iayBx&Juh0)iEbv0nF7U^5;Ip=tJ z$yB-YIM290k5v~HD|p0{NJN{Z_#6J1++>58SkX@Dh>T3sJ3D$zWje}?HnVSnBsq@| zuR31|&ggNBT%@~LnJ*KuaZ)C?#j1jPBx!}Q8nE`L=nj1O>m)n76~MIa*(x)=$Q7FJ zCQ5gZBd}m-K~n54N$5e2HYM#tmo!T+i&omfYh$Z&yDbvRjEX>THaK<@7zD^=Rr3{C z&j>C+#6CzK=kbBu@#X@EH_Vmn2ClCKn+0x@RwEY9MYtSbqF?uz6$2#Ix7egJO!>_; z*X#?(Cjc(h)06ll(G@(u2UXfS%kjkD*7BpPlH6#*FedALESM(9Gpenym)Z$X(M85P z@Huakm7`rTEypo~U;Sq?(e<+BZzQdaWPlXA52E`*@;lV9kGz*xbnuuYAufgY9G&{p z64I52-}IWc3c*4uop{ueul0WnJrE97pi2vtbAgB!g8Sm_I~mbV3xP{%|4KiUEXrfu zq0rocG!uz78@9?&Tp>X@_iW`WQ@OYdiNG@9jSQa{B}do;hp4V>x6C1}!E)(eLzte& z!}qau{4sf(2yQE=u&c0z<EmM&6Xk)b*E6}Od08REN2F39w#dO&!-xUKdfvT2sMNS| zL!i5n1})1cDJjP@4V3l*ds3@wtVOwb@aN~LhR66b=l+szQf7=*{VFslq2|3)Imvi- za~K{w?%GVE8@t)Ue0?sHCX#|Ix%R7iKy<hx*0*-my8Wln(DFoC%QMKljjQAx6Nimb z7E3>z<!^1NmL$L59lXiZ!;lttzvw0`@dB0~jB>B+rOgCF6JAT0RmF#Hk9Di?#A3fA z<3O8Bn(~jXXur4iz4gO+yu7^6IejAGC~6`I)1UVQQ=!J38esQH>!6LIzO3(e25d4@ z)cri_K=N(%QD@oV>pBP#S<S%u%O{d!cpFm<S=7FAbySz%y5OJbHKcn(d{M+Ibp)_p zTA`^Tzzr+Qk(IIjNYc3J{#|4r?cJ|6Tlqy|$X~hqM?e?LWGDYLy~XZ_Sl;{`E=gRg zs`3JjMc-Q2DEwUpgj?<z4a+iCV1Q;n_WB+5T)AP>@y8Eaxf;^W#c-Z5NQQ9_w80LL ztG2SyMVAnlLo@TSP)huMA6{09=n()qx%!u7_-LQI|E`^@n--)y<b#2I_OkNJ_3qSB z5S>*Uu8F*hzsLc4X*R_V{df7vy$WVU!%TL+xW9Sco`YXTVn5v)wIx&~BH?&<j8Nub zQG;1Fe#hW*Q>(Yi4RHRO48g}JQV_Wlav<_WEXb?|I;(@mON{=Jp06TciWlg>w|=^| zB7#M<`lzMNRu?u(GUqX7VZT;Lym+QrRBqQ8CQFDL>Q;BS_0YHp*yQrx66&yUYKJRY z<pQF)O_#Jgu8N0^W|r9FPHv4rtNR!(^sp96UroS^O(sF*A#Y_o>X0{K1M&Q=VH&-m zA2J$sy_OI&?#fzQL0<_aOo71nigeyetEX7S$9F@fL*MNHk+w#on1k#?kdT%ky(Aw~ z7VaSh-uDzQXw3Q|jEO+rN@?As>^>cE8*Mf6fh<~;Dhf=~*e@&tIr8yAZ<2FYF@}Xm zgKPWo@;4NJgH1EOC*#)mae5Y|fGhq9RAS7nvo-#>YqOXn7HAvPn*~sYbaL-?si3CE zD~dU&tEfzA1Wr$=BygoN5w#M7Qq=L!Kc(?`kbY4XQlZO90now6q)G@o3Al+<0j{D^ zEAx(6KjRyJTaF*+L6|Ac1dZsZD^;#Ih47*6ZzO}6M5ZgVOk2DK;LJV0%nT%e^<*!W zt0JX~vQH0ClD(X|#Q>xYz2(xzp&yU40fH<Wu!!mYOfkp=RF{=^xaBk_?<OtPE7><l zM&eMb`d0=Tky<s=s)|b#zEPWE-ESZ9V|Atp+HI7J@^f(C&T$-Y7WsCy3FYSCW*i02 z8ikt#e2&b7cq=8Poz;+t<)<BP-Y4z_OqSd=r#-rCMi6$(dw?Rzm<+i|Ig~HIwTof< zDU!q|lsGcLiI(UeQ_mifQp7>Z_D#MaQbRN(Krm(=&s8X64AX%9?LG%iMp-4?NeN$| z?&3hv&yxn5va2w%KBO;=tWLKtNxAzH?r+n?)^<=QONXMW;3sINBVDU%<c79Z{y{=; z{FOg6dWL=*6##eZ9-@Sujyhi2d-7&H3a%TzNK-xEL`7=%Tv8rbKFor~E(NuJYJVx4 z<J~xhzse8q=TqvSy;b6zq{>J2edjG=oT2qv8`y&2g8n2aDy!??NuW9Mc}tbhJ;Q-6 z77W8(l+>Gkb>KgW(@0Fo8<tlGIr%lskApqE4%d=0l>mj}ZP)HOS)<9U@OShgovL^g z&(^SCiMAVM^~%sThmC$8IFWpRFu0P|g@hoXlB^1&V2%&9#G)CwCVq^E;3rx-?ax4z zNn*fIDehZ|jIa(dNc`SWFh!ZJ=38NQ**D4-mP$6Ca6|?b&2Zjq|FK|BeqB($_9p)Q ztHz^4@iM#C{g990x2IP9oV{28MXc<yiJK4wbtWIOJG9d1ZNG3LO!Hd3l0(`_Wc!IU zbqQiG9Tozb9^xz4e}DJWF?QPJ#sH?u(NLh3U>LFh$p)u2gCFuU7Z=oysF8n!=o)h1 zXyt!VIdN}&SjosWG`jwPeo=uclr9E2^Ab%uNpW=~*tmNPnv|f&;F*d^rKk)R`};i% z;U_H;Tx^mgUM#TDvZXEQ<G&YweZ_r4uEnTj#mD|=<I^{iBL-~EzF5xKVX|9BX)(;| zVU9>N=}G6CDRJq(b-md7RIU`(cofYe8d6<OIsr<*CZ|S123kMwFym7gB`fgu039l^ zk*6)5OQFEuZP%!+hdfK9+Id|D&V&FQE6e7_$B_EcrIR*K_lN6sU^5$cU@IGqks;un zP@Oxo-39XU0Wwdb*v(RR+5-D}ARzr@!e}PTOucSw0`KTeW2>K9!&6;mHhV{z96K6} zdoD2rY_UHL{0Ga6PTt(KY6Y)Nw=N$9XF0m)ao}T?wi6mWEH={>&jtHuqg2f*J$@Cc z_F;nty|V+uG~3j!JC-e8t5CZ%A~~@rBaVBsC4cN20;%hVUyn%+aHi=CkLkMX$9#J| z*1ZCAKMJoTu1kj>1L{#2N5!$zFv}(ib{ZyHbX|p7aWZJe>7w#7X9np(c32&ww_g<v zFzltPZ>>6^9eS+}U8p?wQQ$Cf=d4C?ntQ)CVxj2ujvzu5o-}dwgUgaUDn1Ro^B38) zTIOn607){uJqtabzk8tBu(p@NA>M?Zy(X+2fpG!~ix(U(7mB}aBjUF=H4kCNJj*|J zS5b8XjB5nVw^Hxl4Px0w;L5+L<of67=k@+9IXRu<oBgXgV`JWsr=B9?2-jTs*wSPw z%pdE+OF)mU6U{A8pL>|pIMy-gCd7KBQXPP90f?G8%5VSFP~s2awCymPB(nXU`qCT_ zeED4BXt;iUd6)t(t|oZ!>r<_;;nn2v?OI;$?;1-CnOYo9lO%2kzFIhH$BC_}1QK{9 za%c^lJEufzAJzN#mgUC1ZZ7Uts7If#FemcaZ)T3G6hGH%mdvmCOLS0#ZXBI<Kz_;v z91!dm+57#>v3o7JeIrRKj=*EOB2+4%W(INUNkK=>y=rs2$pTGq_2u);>ZB;dkKFt1 zNkuE1c82jhP=B6oHot=fBGE<8AiIpbQCC*vBsZw0vY)^Q=6lz}T^FK4zAhL&x1#2k zqZny}je0Sm*WOT6S@b}Y-+Y}q#9$ra-vEYLy710#y+%Rj%H4A|$d`c-E{KokGqR4L zEe!bd;%G<kdsr?vG5~2^1I*Q4h5kD?IddQn<Z_*L+0ZSWl^xhHF>EV3S^OAps7m-m zugvb`j5EnN!=q6Yo@Xs{7Y~-S1-fvfn;VG<6nIJ*{a;Kw6-rc<PY&MLuaWgZ%K+JH z>n_K3CKyxVZ@M0=Ftk-I-Zed*McAB^(&L<K?K}BaLPizB*q?-#>&tERh)&A%Uki1_ zl?qsYy`?%i<Fxtiwk#k~h6W837w}CgYiLZV3qjE?sr;7d^P$59`iZ`ztM?$JgKv9{ zf=TmCJByY2`>8@&675bUVczraNdOep9fRsZl-M7I%!{w<rsx9RZ~h}JR%Fw0#E|a^ zm?Blj7IFQ5MD20TLP|2j_HxyR4PJOd+ry&4=$LSL#go8M&2@vQkJEoI-{%=OIm~(H zp|)*%C-Ab`+b?UXXnJmJY9fkk`TTUF*0uY-bJCm@i#aJ(czK8g&a~2sEd+?fqu3w1 z-H=Cj6QFNv(Ya5!DV%i{t+tWCFgjSlrIVjOBd{(chpG#Tz9i8ToEQ&uQ}ecG+G%T# z20M}_%EW<xM@37Vrri6(PwjmXs&W7fRuzP;ild0hXp4%%neliDMSV5U@=*EfK^u}` zA3*eX(*>{l;s<HFC!Gw&_jKR`k<6rJLsKV!PN^5;%=c;%Ux=	xe(K4BT{ZG4<x@ zO-Cygm*frfywXE*$vb@-z|X)p_{d}+m~(t8<aMTw3U+!i$`D1akT2jO1pZEV3hw0^ zIV_xq!FKvhe;lVsO6(7>C*oLOr@q$2H+lwg?3H>Mawi57tk%D9uhsw#s+<V<uL<K; zZ#E@`@^L{t|Ad~FJGLc$WPP3s0sG?xO-O<eg4V1&6AYb+Cc2$*CWX8=F!r9(pj|fq zmyZIgZefEqD}m1H=!;S(7|$0gvI0_{<7{w}4IWE28+VxNKd>}s8~)l%h8C?GXKIyH z>Z_Z)NEv_l)xff1iR}RPi)Ge2+lPxzghb18fSp{9E;X;CYxzS^r)i9BE^1oa_d2MN zNRKBoYq!QDgNdwOEH<Tij8W!d^?(HFBI?qONQ{j1@>h9XG>BesVaORFT{pTlfIbOR zgXDrF-6bRVH1@oEm!#!$7%r1^M13ETibJ%#+VlPAIe$k8g97ldPVG0jVp==`5}Ce+ z<mc7qKZIbt6&C;Zqk;v+o{HRTWd(n(d!c`WCxX%?WZ*39^l8a4p3PXml32(@qn(fT zqC8k3TJhdRW&V3kqO(0X!E?P|JOqwQ35x92?)yA^12}3|pXd@_pgb*IB{>4eWq!su zH5Gl-eYZPD_XB{>V{!Z^dlfm3py4XcT^=vJjQsF0ev&9oevEx=tNnR@dI$Lyq`?hG zP=Pr(9=8^Jpn>dQdjU)vn5tx}>QwbFcg}o?U8ir1L|$YZzAl5YzjszqeA@1d4a@n~ zLIhi4RU2rhsX~6WBEb~Fnp8J^N3GVTQBuyD)N?e-oFbs<aL@Jk0}oVgr-t&HZCAc$ z*Fux}SBG0YnWPPwrG%P$zw&c>Y8(6{SHh-ES_`&BFhaLY{}a}u4)3THK!Bb{0q06r zwS}T@4Zw%agaVXi5}r?@mT`{AzAUgQ<qy@>_cXW3hGQ`|$x(7Y$<!mu_u|@eiX-g( zBy;RV=u;VDh-a^%h@-LXry#a1UPfxbQ77cCuWg?gfsziNUys<|gKTwxcE6`@b*N90 zudd3jBTLU*YgrzqPHp+g=Bg{UW`x%sJKKUATU5ZlngP`4IB?>tU)Ri2@q|F@v~Pt_ zOF|8B-*TI_`Xtnr4X53frQ#V2`8VuPf1veMxrf)SZcKO)u@lT`OUG`|G`r>)p7ppS zZqY9~nZuGKCif)UC$Ilqz_m-xhT?;39f>>hpwf>s4M$VtF@+`eeW`5S=H;K9KMML} zO`eG>;s+dYZizR(b#7*7jC+NRBUf+xT4EbGHb%29<f1IppoG_;@E7%SuM8X>WJVqm zS9fn8seLzZ#T}&90p*Q2-hq6*afxWKq#1LLM|=;ghvpWJ4H<qKe!=_YnBD;&$<k|% zkDX??K!c;9=O0RvpfowDY;FBmfzlFp4nvfLmk5ySqBVO$5+jUGyZ_<CtzNk~^A1da zt}iP3+1#CV3h00pB71_P{_r&P`FQI$s~>c4e61O;T-CL`3m5Si4lE9ahz^6{m|Ryw zoD+0Jd(*H3_%}bPLXpP5;hqlvb+vE(<7o6^295S-_47AO7RgVBuzaep_Nj$$Y)mD_ z(yeygtxIE<4}OI1ksFt_M$22F38(kZ%7%}oKK`C>HYepVjgB5Jfn7Sk-iPj2j{9>N zAv=R@gp|DMvMCQcq8*SJ+aF*YdW)p4D5<AW+<8ZMMbDGuH&mI_P~&os%yl9d(gF8p zRF}7EhR6Ui=zj+D&tU%<Tx$Rse55NhI~zL(Z#sN3JjwsSa;9W>1T_vxNii{A2{sN6 z4pAu{4h}8}b_rf?Zf*(QuUucb#U+Hu1pYr=3=vorEFG=gZOFcS;rQ}D(r4l<%OE06 zobXQHj?+JxZGIf$>w=lyG%T1)BML-bt=sSyX_64(u#6@y`fv-ph%w?Oy6fB`s^4(> z8kqdLUJvD$sxPV@FTOr@=_ilwyS5A8v>OQFrZBe~eeTVwKIib43!8%vb8@HG2NI<P zLzsKS-tX7Ji4AJ8FGh;P3IOK!vG)gcL>fn0_sFsLJ9X$bHT5Mq^?5|x;EMS6lRBs< z*}(^~_og-ck<23UgH~)UxRF0a><14xwFXQHr@8aTw4q})U6)astZO3b9f>@_i18br zJ@)G`kH(kn20NT>rdRyulj|pmR-qa2^+z+_#~pv^?sHD*NTWFH2m*NaLm3;hI2$qb z53$XM(-4c1^^UPC?##>Yc-0m)%#k$nV1re7jio41p?HMDI`$~Aq2#fOmg9X~SV-pM zJ4-+MK_*b<IKqh6GHlWHUt+%;I&)Q6ePcGKnZje^&S$K)|Er^pG8B9r+iW&ok_$$| z!JS+`NTdXjjGsM_u>usqD42fZHpeDXf}X?6?$6M*<ICt>HXC#{45X=(&&0G2{pvqZ z7NdLXCd!<FySIlV#Ek6PZuMZxuJdCG+sFWw+nHB*c>l4n5wWL_3|QCVH-OR#vJ?$e z=O@%B*;6)h%GU}`<*Oe-Ic?iCV<R00=j_3%;~o~CTkC2inFnB>iPM)seA8%q$%tpp zUvw~2CX6g1?Pb6G;B4NbqE?reP0QD#z^G0kE0f@%KBM<7flDniiEg6LD$gJvpr(J2 zz1EBdspVvt&0t-YW$+E0)7vKgAfW%A;fXqmqpdGm@4tqYve0E4X{bw$Bhz_pi-ZRs z5fa=J+r>_&{{<KdG=&Qh(+#bfFNa+%Or>TJmwPCg|B;d-TPZ}3D^saW|D1#Z7Am5t z@-V>C2`2jk1)LJBJrM=cLPQT42G-Kpsh)N1%{PR>q?%}=9L0pP3&I7A>Fh~}7&GO( zV}*qcXSs+LVm(g@##<m4!r7A#dHc{Erf1-oDJXc(#{}?KdDzhDtoT}v%r;{8JRjCx z14-E9OOpcobs8%r*s5pV814YpQaD>zJtx=f!yR4+AuV{{1bSiZtWl<W*}Pk4Bw$Pw zT?gsPaTQF<ElPLpiwSdN8aQ`ErTQxee469l%{QrrKZ&rG1z^!+P$=FiC=4Neb;)Pe zieUQEf_{Kx04EzN7Yc%+P-|@y*crk7PcT2p0K#dUCdhM9*lBckh+I+JX>51M)B=Pv z=#Eg50@@>J-%z0f)+5-LP;e76JSdn@auYf{n21nx6DmAtsZcvMm{{oD9&a{q1*qg6 z3l+$+ph^>h3>2%NOcR_8<b$C00-VCMkZ>XvFn<fVZ;<(<SPYPehZJ>qOyKgp9Cbt) z##$kKbqMpJ3ns`qh>OAZCXhX_@af7|q9Ldl{)yY6P^45(WWBK89e%YJIE(nbhJV3) zBCE#<siTbx>C2GgUqd=|+4|?SD7YQ^*B2%orU;&#@_&tn%O~>}TTTuXHGP1}#uk#f z66MHvMvqHZE`p~@Hz|Tg2j-RSz;R>_X0LVrT0@6xE|Svhss0=N7QB!4Kfxha@c#$Q zf~g3zW2*?)-xmdjyo^XW=0R$;M~j;Jx$!fFpxr@jh?3J0ZH`UyZHs=b0E-hbpN8Us zo)B@HhG>HNcc4te=rk^)=)^38>zFUY>j3=A;gu60%v=*q9+6LNP3VW6nhh`TBXlgK zHS^?>iRu$%n~SO!2)&M~k07aEc4P$s)dWa3t5p#Ydd*d!Aef(aR0Yh{1jsgnRf9qG zCPa9sG(q1@Ffx$-_lNN<*eXJg4RstgrpN5X5OK1vz<GeVrHA^93B3+XS}3*&bp>R# zh@cMSVu*){;4)a9$lrSkf<`*jQ4#R%P&iTv8<IkwumkigX&Vys*L3g_czmFN#o&GL zbZQl8T0rbJDpi^|RO~G(_Xy(bE7(2d>4&Ot(P4tKwM04T|BU?q17E;Elwk>ILSj#F z|2qKxBpY&(e=?`Ksi?}bON%5Vh>|PeKeK_G_;08HuYsu`Ees5MK|hiH4-86j&QGZb zi@(>1=wXMLMS6PToLZWycstb*n?)dzT0D{U!{Q4KUx`Mba`-2LLjMnmYie3Rd~cj& zlIjge|GrVdI7eoeDY#MSZZ+keQW`5`^(VAXdF_1c0WI<%Q?R4Z#|rh^Ls-OmreHd` zmzA>laPA5xo~!l4Uid%BiQFq<9pBY@IQM@CIcvIHawBd=x`XW1c@;kKW292flt~r7 zVjD|DS;!c{;~Zv`Xlwv?b?RT^9#Rsg#3b5R@l~YKM&B%D#Mg#`<%-C6q>2BE5kDT+ zv(}sATOH&(2_SyAC6-&l7KJ0aDj?Db8WgR6Kze1K_-6QTcgBJji_R73_~ZqYQrjS} z2DKCr+o19V#TQ^6A<<oV&>1cvYlJX}IMkk^_y*+_;2x!Sm%`%$K}jZ9b<(zeo+PkG z!zWdtJJYugl9)k)lFASdX9kdG-+dVB4)>0G^5PFepiPWah&~$(EroO-a9{@DPaVFY z_hloD_0AUPxYg$Bz-WbN_DDE_E$(GYF^24<;6LntDPV!?Y-*N9b&r{0ma15W9Vk6q z{w@XPv!ewTXT}u`%+N^{<Nb&J8`i>@3IA{We>DD2um3lw*EK+PHjK4kw;MRZDOQb@ zVka0F#%zU)X1uIRrPLLmru*fXj~H$LfU&sAP{WGLO=M;)3Jl`m?;eY~?7s5VKbH0h zafS!fVm<ij^A^bQUYUXlaKl3>U(XfT5XVuXBQ5w`jtu)uVc{bm(c<x_h}z|N?TVf6 zm_Qk6+vcF<sj%H1_|(4dyWxuJ;mMN?W4mR`c^C)au~@8d(X>M^qx61Z>cZGc<{jn6 zlsPWd@88gM0HidifeD`Dzc@Gn2OE95tZ>%d3_1ERA9cpt9eA{Zj6I_T-kX<vexj;v zb@k4wV1YO+2Mp;%j0SvqZ8fA%a&0*=MlNM_&EZ$&0pZmTn7@qZ4En#@4<W2&!7V9b z{n|2)azu07ZsqBsUcdY0d^^_1TnpdYMX~N#UiU5z0v^i4_$M(gh-lX}nb$Y;qOwDs z!u@*wu);rX(7pL|I)A?RK?48EauM$+dBO1jQXd8HJNg*#XPjgw7jYH;GyYufH)+s! z4euL!5Nkf1@&<*##9uEajJ!+=s^T70G5Gs@K|}8gXV7!uHV+7z%J13^R65W%_NO<! zkFn+ms2zf<MZq=FXL&ov0(s!P!^nGM25hZT{0<1eLKy>Ejl2_#e;ZStNmS%A9fT%_ zp)SDz#x(w1qEAC$pk4MpTE;MC_5*8jk-e#2+-^AI3!JVOsV4%_?%s^8v@qZT!?SS4 zOF#TF0XJ}&s>I-9=wcfXdvF4k8;5U1{eA`fKwEh4hs1rXHRh=HulFJ#VZ6Q8{;*Gs z$t_gukI3gw6_fsTaIpeR(+`uvvu}lUD`7<^0}s;i9-=zG6=?f>M0ikh9r1l71(>u0 z!>~Uw2xNQf*drAggRKa-=fe69I1H9|3<^t&2wSQ!^%%uWvs1;^y2Luk#a_9$^ThyI zSsYKbqrOQ&2bMQzy3JuoOBT8<?XP$!RWJzFyi~9kV=mnP4smk0$SRVs{<i0+=DuOh zFjZQ_1(Le3`e-TM_~Ur%XG{`onu~h*@E&l|u;k8@zk9i26VH7q)nT^L0lWe6Y~u7- zlRtR+RyYiJ%W)H9`rE4@K)-wY-edqBvf6OO%-bE5K8$BBgVDD%Z8*jVc*Z3}4~9rn z!Lh3JVN=L-<B5Q!b;=seQurnM+rIlS@6b`xwpKaEwgfxtHdgIT<(G)pEpj3eDpa+H zFxYCMh{(E4aZC`KrIB}71HZtHoW2vZ4HN+^NEMj*UaT3=XRe{!Z=N|;Uj@j3T%NYQ ze|d?a7FeM2V234J!O<4)(^qMOD#y3EoI6I<yd!Ry*T=szOCwq{xb!u)^{h~WspW)T z9ad3<AJ%W)3S+Q%i?pGk8kTTi7{!L9*VV}9qqB5Mw7oH82dJ9>=(Z$b+BUTCtu5Fe zB{j&keOB7VeG78US6Kku5>TZQw&sZQOP|3&SUW0e3_0V4rqBJ>t&jN=-H}qbr5Y=& zm6Ucp_{FR8Ak1rvaXmEPBA0djvCSEv1qJJYM6F)XZUkIIu8th~%&R&<y9{oiWV|O< z|4aIXA6LiL;lx$wrhR|qU*V=Mm<1kxU%dh0xNGpNwg95Bkec^CKm@8yN35;#jjVMk zUediJ40}?vlzZaN^M}pvs<y-Fip2NixJHfIi{xi^XBK6g=7SSf`-vzlm8pC^XkEns z!et-<rRO6WdqDwkTPRo`l||SW6ggY`AlRLByGxWtX3zcqya`CdKF!!Wb^9E(o}J9@ zIXU0M<<EPqy5j+?kA956xi0Jvui&d!3=lBBkD4l;KBsgTA}iJfm!j}XfzfLKtpcSz zk^M1myP34zbw9Sc&Ctd@Yx+qkTTgl#-W|mtna88(Sc~5jm}?b2)Q0($S#+9ZPw-2U zkc{4daRFmVD!aqJTJ3Um<m<0L20MHLRPOU#`+W8tzhVG^iw@U)xdk)rQp0`^ZDvnF z9>hObN=wp&S*O(ymoFoajzQeoJSy28ge4pE$Z5|Ti80}YH;sg44Hpsewmdt;rW)#| zTyB+GnQrEL5<Cy^ra56=n0w?r*L<cwLeA~xvD@gC5!Dy;+iacSI8)Lc%c>Hx6^{;V zoZOp(2TTCgY2rJ$bph(m?4hZHYP|MvaFahVnpo=?keGT^aVyNpFOKd0+gcUV9jVgr z9&*U7a{L+9`OI9y5RM-5J*<m#xa)c=Yd@W+zNtXF5Wa?vAIu`&!303GqN1-#ua&Q* zTb|c89HSgTXmG3tk8*e=&aM!TL!%_6ZWJ;^Uep2PBK*nxMdi*V|8$QqXRaARn7DZA zze79?`VWxry+J*>1?L;NQFOGU=Z<rfeX?&47OD1La*RQA<y9*#<)CiPwr4AxHhlBE zk?6@cG2T;A&{;S9q0Oz=;RjU?YjG!H7Cdf9OvdfND&#u#iQ{@{mG1?|qUYDf?vNk{ zO+c(o*mliDyFR136Mo6rn>lzxN~WbUqWv^eFU*?<EuB!aeO-~k`@-s+<pO5`(u=X} zT+ft$vYlA-lFaWytr~QprR&9h+j*z~G79wEYQ-rO?fK~9r*eM0-G^-o=z!HkSQkG* zUGJ}XQ+2qzU=ITfQdb2F8;<klTaNP708&sMjjU%Pi!5^w#FX8k`_xaIye+cd1zG1t z^H%3Z6w9o|cZ??v8^)Th8`T>QEd4#sY!uG5w(0HwrKvHk_!gP)rhu|HqUGic%kkzu z!{yHMqh|1iQqe=OC*LD^RUnt)6D;^^#&Mw7V&G_l(9n@_g}saM38*h%0ba!d=#m<9 z8ZLHvZi;DWirELIHUh~M0hIxFVY3*8@U{1ni-mJ5-Ol!&DW(Hl4$G<JzS{id1}X5@ zg!Yr3cd5dsxUtU<UzV${6Fso2-vf-+!dQoaE;=Xga_T1pkJ_&K7qcymuE&Y_<|iBm zi>_3$!?lWx*Ot{)fByX{rzuT<Z`7kJxhmz7g6H|yzYa?C_WZH6FMeS^lSEfuQoB71 zHKbf>+b0tt4hCNbllDx&R-HeDiWPL6!dAn*kVglTRvj#(s*9gQR=3_$QvD{aJbF>J z`|@Vv5Zt8~e`TKH6!^`JO!>uS-17HqkFtv9HKu0pJ5}>YU;`hjaWM@rsBEdFuDSlk z<<J(`Ay=7Sd3W2`w)styR9ISabxM<G$G&;s$;UN0Ul>9Lzq<~3yC^0FF|eKwzuST> zk@j7UI?T8%Yd5_b><N3^t~5*6xLj^mdqlj;sC1rZcs|gBwI^qZuJfI5zv)m}B6?ba z4PF7}3tyqaHDNitU-dcg@LDl-{Yo(($Pu+=j2tX1qB&1WcmFP`803izu)UBJ<y=Q% z%=M23acq)KPQ|Nu9VJNoEY<{jV_$`Pt8e%%tTdJW;qB1)0fi-S4PiPL&^MxRgH_~G zl{fHiJL(O*aD$Kpnlk;q9aH919&F^75|8Kq6g!yG6nnZ&LHhvw@3lW5O53{81X;u~ zV>I*MOKp5Izn#|V&>B?cjX7!ldDI3)RjYys_OrXSP{{)c+1r##SBw+V&@X-m>u*-f z?l@7f@R<M7ubcnL;QhgU(fKX`^3)0(lI+X%?}&lh__=dn-n{%lQshZW@u}-j(VdUv zE%GM_K-(bM8AAm)52Z6!%}?&$cNLD{9kM<~E){<NrwS)|DjzN;{(F~6P%yhAkBcz% zVP~8NZxy@}4CJkJ_edK5&1Frds;xl2udU*HS^8l5{fqBnOGWx%Yo6s|Yqo4}%MopJ z<~9VtP5)inGITjFwJ&VK4$wZ3+A`jdYA-V%LcAK^`T)V7Vb}rDY5C|Qtp66T4I^0i z>|}R_i`XMpM|ZVV)$(e%y7`Ve{6wiW(&Y3E{4p_ZNtaFwu`B>*LVdfyJUff-`3!6e z(8EvhS~1B#3AtfcUM|-ZZC8s@et6L!r`zfqqrAwWzymwm$P+bT!-I$jF*V`E1DAsE ztF-5;0AS2}bl6a0VKICDYim3>&SRN4AuB@81^;2QaJpRP=Y9x`|C4C$6ul7Q(_=)T z2X<CF@{lg+Cu<E~r(ODAmn=H)XB!-Tnd50rwdO0Y+7A#v{`57X)W8x3k+|hDC_e8e zpqF8=`lj9#AYp+OGXBewKGxd)%3GHr^Z<<VrGo|VHV9eZo1%=(V9emP?5TR8+y%_r zn!hkU?KMuo_(GHlIFBGYAdL1It}nE{r#H*_1z!}vZd*2}u}%|S<>^=c=Z*z3jFsFU z9wZNEEcS%amyXsIc18WaNV6FQZye`k`)hLTpO6_elx_%?juvk2=^5Xkk<t|!;Zfkf Od_kb5mQ<EP_`d*r#nA`= delta 15566 zcmbWdbxftfvn|SI<L>V6?(Pik?l8E!vvGHKHm-vV4ucOcFu1$U;O@?y-#O<c_ujnZ zCGU?)R@S$wzI3{}(_LMg2Q>Q!G{ND3aL90A3)JdgNOt}#^hY2aXi{I!eO(5p_f_YL z4YqOIrnGz3z$ww(I$u6No?6Fld<;M%4sVIE15su<*--T8Hz2`XJuIYHEpK!8^73ul z-;}4j(6YJ6MD?j?@+cl-{8mqfW85lkGVb#SSton$>a5y4N(6WB{$jV1$ZNIlHR}_i zWc51hIq%!`$#88us56(|TvNtcrxqVOmyX;@o<3DWq+5SVggTy%<MZ_-OUD_Tc$(YG z?trF8&cwv<Bljb~Rs4Xf^R3c=ZPgGi^_uN7%6DA4@a=i`o)q-sdB>QARpiI({&?&5 zRE}KGBhcB{<YT>ctEcbB%hh!|?`6Zm8dbxgKCRAW5Gbh<)bmT|6{X0zUgk|L@=Lw7 z{8uWSOvIv(DJuoMS7^S;gu>0WoIJfL=rMkbAB9GcgqN2C)M`wkt*{dZQh!FAckx)P zxF~5jGwJow<U)3RWzv@td2MrW;+zVCnAfM3bfz@KEmKzol`kZ?zr>6kVo3bWMziA^ z6Bogh&-Dw01;rmSbrx_IU^yBsE*G5ApHTDIsJA)Jdp(X}VnHP`+<v_&sl%yk_t7;( z!qOYNjgFHmarcujybJFrl>LS7nn3?7q#`c=*Hf!BKi}g=wyye;!uD9I)n6EI-tyCx zR_V=eaYl;^v{27q2TLW;<O7SyIF-2O57DVCr3iy0l0j$TWJUi1i6_$QX@e~DvmEtG zSI_g~+oZcsNyz)ES9D(eLN<-oGTDmnHnn=})+Qw(K{wE)gQ*h%S^ec>F-vz$kXbUA zK*~|*sU*a=obaE}BE?_VGk@Cw_KxR(muu%>@32^K>ZVlmovTEEz^oeJ*SvuclN2&j zFuXN7sALMhzX(%eLIv*HH=GE4FFVy})#+la;SJ{dd6%{R&U{P)hw(M-@KkXA*>HKT zntVJO5-Uo-syt^}C`RTzgc=4<h-tG5eYql4-@s&?{hgXT6|T$UX~nnksgNOh*=D_Q zH;Q-<f8%0ni&R<@hCftoGsnB`6MRPyhszxyAj?I^WoUx&0>Y{Tdc0(N@4rqu0miRJ zqDfZggKCpJaQmv4*>h4~8G@I=Zh031@9JB__4^r<tWS)XdgvET4gUJ3yG(!8b@3~W z6GhU)_F*C2>xn~F_>{q+6(zDq3Xc$D*E4v<>2`yTH0X5YUke#>_|bQo9!t=@f(E>N zLCc-(ZH5`&D%%DsbL-TdG7#7&jIFpgrfx#)Bs=(ahUgl5?lKqohx9YMOY~vwZ)U7F z$@JQ(a?unq0hPZbTnCSAPm^IBj7ALewk7+ao(qDN-6_b8Ffa~WlMZ9MbhkaVpbX}T z;*|>zzvfCtAHd2w*L1CEex9RCL%C~ug4*pL2^+9Wb4&~Cn*cqGyh{GO_W{yIy!+2K z#73P*!o}TR{m<uDQJ0E#X5%6Jgj~3^EhtgAbaupsIr*@#S<_BlHK}l=R0Bz{$B@wl z$cEp&68gyrq(d|F_pgi<5(`AsFvJRu{Bgk$f~OIL9^zZX`{C<$-uszM1eIcrpeDGh z2Y7^mOX<QWti7>`XoNJ4+dzZ?dMb%KAq2p#ft%~J8HrA`JJA;7&!%}=1hobBby+z3 zQpx==eGz^DQqqI?BLzVZ-dN;LtBnJeZYJ%|&p)-Y(xWQQ*Nso~LinOdPx#OtBy3f~ z$OaR4N%EgW){k?fq(PZrwa(%jP?tmH#ZG@#z6;WXOzc}s;_jG3j6Aos3M8gR)nrIR z_@Nt8t2<h=Sw+LJveW&^H}!pPqT;X493(KttT<)et_PgLkhcOUNp{~mdB%#|hf>>C zoI+l8H^ZXR$NrXlYtxNM9{-IXunp#my_o9hIko)VOt$WShSIJsR^4eW1@cHwgCNip zE}~$-^TODfi8!2A@&9>4;msd{7NbQ2u6BGVAao^&4ma@GdsF#EW4f{Hq1$ESGKgah zIi={mIC6Pz+Od7nRrebw)4~>cn^(y(!y`(6Ei<U$#-MY>V8VHT$V$*6z58;*uN0C< z<SwE!Jejk;%_8t^?`An$0~Fqwey{A>y=9`)x*nkR6dCpV<CmKrz#neUHTc~f*(;8c z<G3cF=d(+H6Z)oRsy+51F3&TL>CT_|cY{0Z&-ROGOQ9l(WlQCw<2#uu<DH}O{am<e z1WXs1`m{k|rc~7!N^t$SpITRlLFMGi<_k6$^`3*o1Ftxl$A50C4K!TwrL+kagIf7D zzc$)=RID-z;{MhgeH|XdWGJ#=NhGeC$+XK0%OE21a3Q3t*KyqtSWwW%EK$2MNfx6e zk1FtIu0EgMEjzGqjs>Np)GFXSy48oWC5IbHIfmtx`bsLpwP64btk-eB(!}!m&im1r zlJF8^@(rfV`@&Ic3)H3diziO0GfYe(pyu30Wk6-!4`yqp098!6*>P-Aa(Z_t3f1`c zcOWaC18vE2x@`$;)C<^{5q>fTp;O-39(%{W^$ym1t7grdxJG{1DsJj4mL<8z#T)X2 zksQk2&zAVK?}{ta-t<xFvB;z^HZ6&_7PDH2I>XN^(#}Duy&&I-$&54L;uq1z@t6?U zyJ_K%ai0q(1lCN>aW|`Dzt{qQ?fWGG&(D(#_&ix528&QJEWZ{7Xk0GOYTYE$;yKvE zj>esDv6Ld?cMEm>-!CQRINLHWAgG?RF~)xY>k2X-UZ0f=0K($DT~^yHp>|LrPsivY zE@CcE^mhPUYEbln2gF()^UNkpGbG$Fr${TKj)*${Ob^4uX@URsh`R<KG_1OjXw?<E z|G4{$kALX#5U*{E^~Sn(nPw2!vK|#!;=lF-N-wbi_hOg0)*n6yJ3$u1@sDQ5`PR9; zS!jmFa>h4VgkPTxTD!0tf-H@f@0+NQ=;0_+B<Rs~HK6<Uhe#EwHMTd=Du4WFeZ#fb ziY}8mUYA<Hx%n|w5@7Kd6~KW~FEyDRso9VCNt$x`DaKBG_AUOcOe|UPVTu!a-;|$2 z!Hk?-3x5d(jBKZz(72y(;iCyN>KXaj6xWeaVB`+`Gz;BC)`-$XG%R)ZIMH7zfm-%b zsyO3s1ld^fI-XTbHrmppNw<9WL2dZcZ&@LxK_*J9(=r=|GX;|$_c#Op`U)4t8b!ix zMU)z*1mpEBH&Tijmq<t>@W+EEE}vOV!<S`Ulk3e{iZrXf^$YJ_Z`^uzK6;%V?qC5< z&eoWw!|@yP$)b%gVB&JmirM;;a6h&xGb}S~BWOG=iQ7k|j0rJayp)CKLyQn_RPutM z{v0wcPxo0^02LEg_s7&XV5FLLXHXGdenxt99q(dGOeO=H(1Y7md4NjvF9!A0tfn65 zY*^l*CE4dRH;d?E%xJ^Kv@hcOUA#N+6UindOgT`LJTQ(pZa#-?M!0ck4Kv$o`bqxh z&mbftx?CHXet_^*NCY%ME(QDL$CG1|gD9O+v?R=4(j<nA>(SsyjjAp9LJ*^pq+l(P zJYX;{=};*C5dAK8NHV+J7zA#vV;{ZcWP9*~B7KOf5p5YJ+Z{&#n-Zy<F`65!xHZLX zJm3z|mmFJ-PVo%=M<OZ|`Qw0nH`H!s3uIWtX}I&KTfg|}{A0!|H+8|WAR#m=8VZ#k zfrP~&d}ko?=w@Tbm6S~3(<oVivq>&Sm5+d>k&l`L33qAop`XZ8=2#7?|J?iIsft$z z%_-hzCeK2XK%`0_FAZgTz4olYRvgzo>Bay)+IN>N2rxO_#-`>aD#iLcfjhWK5adgQ zpE5}%T@n0<GBMss2P<b`pkP_s45Vxla`V?{ll>8#P>4DgSHlkIP_#!hzt#&Hip^x? zBKKzVTw(y<m*=(Ekv~Q^A(>K<+C?Slpcz1R!N-8kocPD$bGsh)12mpqCGk5;YPG>Q zr(r+rs_KWoGm>T`ZV^%>VceM|fS`%-g8KZ>u-^|~;Nr77-vw?un9|UN$plCj@XnIO zgAPJ-Kd&CPM$~?ZR+dYzo5cm>%jMa3!X@=M9*;$&Bx8TyPlkD_UA&5m+D?+9o}^Ht zA0<WAEF^kNmuoj6OLH1*;&HWZ3lAGIIh2qH{lPkPcJ5^qAt;~|MuM(R400!Xr{o30 zEaV8g0K}pClE#ocH3<#m^tv*oxv%by=E4IuXR1GP=)ZCp-&QcnBm=izxG+ufS?|&U z{g6w*m0BW1osz8hK`)0>!i6sy<O3Y5nCb32hg=lI^jc6JE9U^Hac9>fS$A==*~`U` z4*Q*GHWc<EnEEd~!vO$HhECF60f$$PP`?*ABnRj#rW}thR1yHjiKZBu*~dE0ei}7I z>IbZYzkPC6#tjrbfH!ME7n&ZlNNAt5&U51*6yeIZ(;_wzjhdqA%14%EHP5_8v+Qso z(((?@uxwCUccbpiyIbBCs>;&oKD{#pN0Aw(mPFp}O{j7vTG#3c`QIu^5KjMbV2Ow` zBQvkIdVW}Coer1NXgInCD<rLD4gQR){Z<&LC-RE>W>3oA;R}0Nv^)(mHYDJ6rx=D^ z{+*-v?F;q<A8q_X^Xc$e)X}02>$Xwf$A@`6CMLZr`{TIG=kv+mh{sv(X=BiRuHa?w z^OaT5y%Ao(=Yz!PY+nP*0msYDeMJ10$(zUfeKX$-K4P4(&9;z#pfGr#oI(kJ=osNm zp!U97>C+Z$Z8CJj)!Gaa)bEV=tY%x9;Awsovq8*;b9WQdtqCSUMbp>~_9;1Sh@M~v znv)wrirGjH{F^om^r0ZL0U|mLnsJr`Wf}e!S4|BN5OprR(4P34Da-Jo$Ouj)RG;3w zVEfD<r0%(GPIIdGs2aRGJY;Yi*eeP`2oTNOpnZPQu2CCUR|29oQ^kO>OacJ#VyNB% zUFn%QC=)bF{G7^W#-|SC5p5xXmrI0T4Qie>%XLV9xrGfJA*}$W8_BdyhuB<N?cw^W z?-jaNgO*xOVGyai%KbdM`Of@5m=scOyVzw2x_ZjKZ<-@y$3~o#L*pq9sT+TBUbi$+ z6c4=xFF?#-;ep`C?^oflZ<!i+HFi=pzc8-1YN=g@xQj5{SiPS@d+`*p2#up}6->59 z?H2@3x(rs*_qhieC{h$lnG3q%hdeV(O9#fmF3a5NXgu}f&*`@}WV~7#UHAmHt)}CS zOM7!C<)wZui8eg0xX=3O@GhDm1^|EN)dem}dup5k(Lg(RN`Fo1#?ONiv@JBkqu#6| z(gjr=@gp7|wfL=JzSu^)sXC=(_lIa@II<ql$dw|waPlNBDUdV}l5C?h)`rTiRxo@Y zu52umU6U^B;PVeFZ7ey)bC5w=0<*9<>fQT&+(?wq);?}4HZ6kt1u|BgQEKm5@K#UP zJ^Q=<@_>r54^TXtgd7GpQggro6kOR8=$PZgZs_p?Jg+%b-+Xnm*00D$kJlaA?MPFg zgmv49lLUKrc0^2EY>h~2g!*6Em#i>fc;N(p`2LoV33ja9a2%9Ol^P+KD-HQNY~fc! zA^Q$SZh@3TXfspkz_d3{jukEyY?47lo_pi$P6O#sdf$M<bkSQv$u6h<lGQ_`s&nu` zAARNhIw+s+$~VSk5-`#Bs^r?zB@q7j`)^q#n=xN$<@w4_arc-;TWj!u3mQwDq%sLY z)4u4vU;COzbgOav=+O}ka(4>~Rkd=<Stg3DE+JBfxTF{kk*2UMG9QT-a;oF!78Ggn zz%i)kP9x?^zTe!wtqV@gEi?1gkB!AsXuKilq%nlMJQ&4`q98x)r4Ac(oa<{DwDyiO zG@cdcV9Qn*#w<r4s1j2_VmM2862am*N`*)X$wdGau6bD&E6cY$Ir=#&wJ&7ZNZ%st zEQF~c){Y`pQFquiF#==g25c!~!I=5;P}3lYG7buEa;BiMCF|yT!ZYEra#M<ayu$i2 zwBS*<v#<7B^t2X8g!g;F;#ypbT{}Z9JJmotwmwN~c){PP0WDGBZ-Fo}9(hf)8MAwF zX%04!yAdMxUkXjX+|i<rIjig=+c*%sa$dvu5{CueDlWlFK)Hk|=*XPMT8aHIbs`5@ z6$nbx5X*Ip0`aT5Mu8QD{H{NNazYTx*FYz;>$T()8x==MW+|I$gj+#7d*c^OPG>p1 zdiZsvIOe<4v=v)*R-~U=*5;LMWMuT|sH2bPRQ$QW)GXYT1qnv{SJ;GMdpTgjEfJWK z2Y<I{IP4Jrq5`mr=O*vKNz&OMhpT|dl#*IJP?r|==2jx;y<Q0I9^Xt=!W^*h^QG9{ zl)k!YhYD}7V{lUO$%gLcrlFQK6aPvqZ!5-$0b)jJ6iP*RMLJ44N}q?UF}DtzT5@LV zk&y`qg!I5G6-?#m{yemd*Kkq5yRpQ?GNbFs#R3@Q>}j5$oiC`LMzdxf{pkf!dg+&J z&-y9k7H<Hf-nWjgntqO&GVX-j)&)8UJvWYq+b|q^x^d5ZC_0KedJ;%FGGRDRkE_-0 z$`>K&>A#6KF8IcX)rotymEF#{2NcbuDbMO<L~&BLKJVBH+x%|4p$ef={{lxgO`j|k zw=iBTX8h?2Im?cWu@^7h4f_rP-nTEXb}eH-TI=yy(Ge{pR`v*0A7S*+gnHhs4x)=) z)Mf{=Zq!`qXJ$uH*{Y`+#2LxG=f6PTpW>8q!9x|&@pe?K{w&aP8i7k&E8ckc+8iV2 z@)LD|XW?R$bHJ>##kx34;EM%a2*phFdmX0hZ{(KAIh9=d8y9b&^U5no)<+eY<j*Eh zu2^BG8<Ath3*pb;)}+|3ZjbgTL2AXUf60CB8f$f+!g&-MD0QI)gG0+YBR8^2ueNwW z{v-X(TYH8Yy~$}vMiz!JY!n0z8oyH^Hymx_av}5*0Qg#SMYOQXVd@|z2FjU6i|nl3 z?KY;6Cx7eO5tMe^5rF}1zgPOa-Ok%mXpzDGon}yn_6Bu8qe{IzOf#wz!{XkhBr1zL zZb{p)5H-YGIaT!?Yy0txjA0H|Dip=Z4)QVu2x9e8u>vBW#3DP)B;WEqsV$7isny6M zI8-q(KpoK$wOJ1XI)4jBOOgpm^Q(x}5iRfaS|#<#Erb^moyS0mgdC1E9YaYACK{mi zdnFfcDrdR1?I5O&HhyXw#@uJ9M3i*%sjSMHgbB&?dYe)nsJ&+}>eH}jqFmTfO<Y(c z3^pnX*UAkTJmA#9bPDrit>kWrct_PcsvkTn!nke0Soa{=+YstMair@S5FpDu9Z=GC zu<u1yxFkGkbO(y8=q<1IW<tkVNt9ajpq-f+<Jw)&`bO3xFLAaiT|kyuEcRWQiM@#B zd&m<z#6FH!4n%EI;+n8epB-2g>pfLbs2m^^!9(OYkDH+Jr$mFYh37CmPPri2$z$=2 zIzK9RMilME|Kt)Di3#Sg*y_TXD%Pm>ovy7?sXBHD`v^q&FHzN7NY~aa{ric!!7JW6 zmA%Zc?_fS+^%)kt>FyB28s$){GT~aW6*=>3nWtu$v^Bxqy;<q@4<yox1+g!GtOZUY z2Y(y%oJX{ie>f>)lNjLRCK)DCp6!L4;+uM7h#FB$_=*zQ97b@I+Fx`}znAQV3SJ6x zLkrG`B7p{X&1^P&?Iz5(kip+mI?uh9pd^}^)aT}xI5t#2#on=tvi^#-=~<tyl?tT4 z#k|;KrsOtnnYZ2#Ce*zz9v-n4Y>~lZ$GeK`Y^UmfXMecPqluybr!_oPykx_jldXIY zGyQ!73oA>WCcg?R)VXUtJRs0?C_nB+@nueg@i&OW=XUg$*a#ec-6-RCk_MOYHx}h? z^2*i|(aH8>_{E#sYN5I|34hX?M)Hl<dIvgI*nwBa$W?}kjZO14YmO*5hPs#d-vJyd z5yLn%JvvB`2Bs2q2Ts4v=bZo{j&jEwN1I>o1yE1<CZR)G*x9REqxib_aI;_;fU8$W zjYS~dzX2(&f0+29@<_EZRUv1Az;yna@N8u&%Gy7dinEK-I+3dGFOI)`1+dSXwOsWt z#712Ry{&J`5__*~CS-)Q^O6y=Jfy{366x8NXPqbpDy~jzPc&TS<tnBXT8>%9xXPDM z%RP6I%|Z~}&m-g<iZ&M0#x`}Ly6D^O$D=?PdP}Iqa>o%D8c|tVZIf$jmDj!6LlXWC z9rj2l7u&XT1u?w7BG7UQ<nt(V*njgu!!&=2Ij5eKkBEtES%0WV5C{ZxKYs*2n?Zm4 z(6~@zP91Pl5tQ3gQ-gHjDWI$3l)bl)QMyR+(NxZYQ$6bK0E?*3l7jK<Dl6vxXw!i# zMGukemf;gQ_K`%tj<_Z_Ux5VI@?XfM6E_{2!0McT{M+CyHF<F6em7k|u`kKBAw&ff zEpi{O!^%BG#*vLHy|<fUdKr}?iX!Y`8|lr1^)IRGjhN7~Jd-AxpfLJ><!St>-U*t| zsV4CqG#@P>l&IMem&L$#aLEy4+e`y3@|sThX=R&;98o9M;1@O@_jV6M*3(}C#|ykF zZF+qPE+kts)qlR1__{KLhREp|u%VwY&Yr!N`lVBM(#K;5d)qUV>0U$GX`xZXH;t5M zyN{ta_Ep&jH8H0T`1tp{=EU+r{xmlA!K7u?^|U%WQuX7yf2r26mB#S?tAYx$KiC)y zQ>bHdbVXX!n+8$_Tbl+%TFPt64NCaTEy_i+#B*5JkpY-1OV&P<N}TWvVPxdY(~&+9 zAm{stGDeedlcxhcLQvbQH_7ygw{CEDl^^lY+~Z*sBN5!Ya^K0TfEx8A&=7(@d^|#E z_AlpL3K~cZ-yk3+T0{~{L{UMpg&0Y}N6sqDy{s^}Nxd-dml1D%y1!6ySYBFKcx;mM z_vcKqbE_W1R@<zc$2s|s(QT{;IMql9nxtg8jpB~T{BAdIx(ygcMud&`5_P$iC>vW1 zTJ&^p;!PZna%H01PR)wmi+9H)32y=A@B)ycZ5wCJff#`uz4`w2rc)r-zV*8Co5(u0 zAOt3YmguHG24lscj|_LFx>RmeD{_AGVf*8M+WLt(wbOJ^B1BtePtZvcl!QJ=MnxTW z{B>}oVr_4SDX_9fny%y%o*Q*_q_@%+yQ(U$!pR2jxSLs>zMq5?{FU+u*e0&DgE(og z6juY-k(!Owuc?!p*jj<Uh~b74YsoPrTWGtc_!G7?okn`LOSh4^4pA+Ci@HLZz=67x zPb_VzjReJtaW}{8*W7=%8&siPbBDaK{@Y(9xl`_cvt=8}J60KH%o~5Sbd<J!K8VVC z5(>gsS6cyK`pQlFdbP87X%?f}Jnl-H16hyWD~_iVG+pS0=dwUod4Os?h^xntZ80hr z<ny6~(ftKol0Z4I3SbRo5N!nxSq%nCsOXO+(r&`pg8j!!h|RPgZx=V&j<H5rEZy85 zpDv7LD$%y9GuFy(hdyznx>#a*NC*L{q1*PAVk4qc$<pckN_qN4?aF%N+@l#a-96A6 z4N@B0yVCySTvC|a6{Ot0I?BCOyyi?e+*T(tS!+Jj_h(OGs%QIwXxR#QjrOj0CFrw= z*e9u|o>FyHt(h}Rh{pGUo4yW{)zk-rnS}xgjSI=g`#;Zsx|`1XJQ$#96LKPid?ZaS zQRyb<b;DGJ*^3KmC)B7O5xVbZaI^;XRL(q~?~_-O-!=HJaRTW=XDHqHB&U!Ld8rbX z&=Z_k@LIUc(J2*wMPrQnXgaV2b(76y$FI)<=TIW}do6;xQ)WeT<3Ix@c=Gu_zM?(7 z@0kZNdzOJ>X49qPw0>&Jw5X>n<$j?l8RmGwaxWP>TOLNewVy=sO|UFaJZA9q_WiVQ zbN7|AV(R^@%yXeKq?eH1`E<&JquvK?_q;w`pG*aAm~3qZ8S=gOjVQehpc?jce<qbW zZEv$)1brNzyqjm{JZ&=l-WxuTdaODR^}CJOe)a^_P>w{a#g=}A4<K-?NK$Y$*&}qP z$=;T#z*`s&_f5pd|9${)HFq4>1i|!8UzKaUSv=$Sjd!_kKYJZVqrL{UU#4VU8}TdX z{($n={6-zuYu7f#!IXeU9Z6tMKtOGXUTEp0v>k?%Gw!2Te-pUrZ%{LY&p<6<J&<de zifaTasEZ5rNYX&?kb&YGYQ9{v6WkZL5Ui{OF%hc;(Z>avu=L3I(hcH86Jkmkwm;LT zuvB``i_dxJ66jk=5FARygdA7URZzJqJ#~zgtU8G0nl!iaVRYN^D)``J5ywIthI;c) z_iu)Z1*}y!4%9$<$?wAuh4+fl?s{)Onb?DX<9odhyo)>yV@z_?;W|g3LXy;YD5m^y zuvl{z+s(K?ayKf$QVL#)t9<$Cy8&DxiK=cX&YKwdPJM-to}vfqo}C`Vuk~y7mF5w0 za^Xri+8#H)@_`h-GF5T~n`OSoJ(Mx|=z#gK{=eyB6>x;Uxx^zPg*d}z<sDXKGcTa0 z?%#rfH2o6{3AcVGUck{mnd&7-gzZp?wq0&^#2l0|+1pY3wS)|$52y5IXa=?nz->^q z>hl__$J!?(iZR2Kdtdqx!rJ#+HDvxFY2$aH-%^SJ$<|2USp~h8xH-7c4nuQ0*1Q6H zna7>k1Ldr3a>c!8Gx>GLIaa~4dt{&v&a6{I(|tULiI0nu_pa|O;YqN0e}a!5x{2%B zUV)G)zT;nE5*2Hv8uc)AlP0c2EBy?Xz%o})$4xZ~vL$M3?-d&q3ZRpY{*?07WG`(c zNt)&~Qz}Bhw^cu4X%u+S=~3XJV1W??yS9=MZ?=DtYWMk#@3|nX1eG*i=mY3r&(0O% z42D9pOpO6BW7-3;T@+M4i!l-e;RS?!9CLHp*+%;kuSUEHe1X+$HU%N=Xo?}(qS41p z1ysCQL3Wr;E24hT(b@sT9<DX1lJWVej`T{{6{vGZ3d#paC+GxOq>#FoVMaM)nZ3|? zo15K9ilJftRM7v#lvkA`1%p0YdGVTIEJ!*-9-T-3_9McmCjS`k#|lTQ|JGt}@7OJT zRBe(sg%6VKZRuu*EEiv2dl+a-a1<2vlm7)jK%gudsC9ek5Z2tkz}WqbrUeNS$4K1M zFu$tK*c=v$c3Ji3mtbQPo{!K~8w%jngn9XU>u9L8s_{V1s)1B%)gj2Y0)=)#F81aY zk+dpp<ZK(;vGw+bxrQQT*=V1xeQ7SR<*%CwneuMb(307t2I9P_wFpV*HVr#^ur86L zIa=-`d2?lW9xgpIl^&Ed3d(QC=Z7;9iRxgF=W;sl5U2HudrUO!t4H`lvrxNs8^@J& z>#8m%XWrUbq$LfF#duKUnsS+QhGV`9&!0HwN~m&GyZp3W>@WhSVBeMDuV2tIa+)bA z(CKZajj;r@wlnU>iy1ZdnJ5ik(vKMW6%)Ae=h9~3XJx9Nb88F}sEZhH#o7?Rl#PU< zija}*lBnIaZG~NKasGV*>TzNrVW(4buq{rmAzN6VQ$O3ZNmPJJ@rl2!;7x8mQ<oyz z{~}edgr$xN|9VBeeP(Bn^5ri%dY6er$sYj5=97ljav}nbi;3?MN|3l;r!y>lo0O=; zn~-6DUDD`l$UJr39&wd>08T+Au_M{H#)djH2lxZ~5cm|xkU-PI$GlCV0$!uplj{Kf z(bVP|*kR-`GU5+V%wiZuewo1QsWxhk<ve{eDSjg5_etWZd+ouIHo;|X@4XX<D6$c| zc}iso9Zm*l-GY&^G*)x~D|82t#cD`0JU1Y^<9qwfTQN)bG70L$lMmUS(<IoVu7-Y9 zrJWMYl}DTi)iBWkmiCs-vKr0Q>rFFD%=bTPDUfUyd}@C|jTV)ri)ThW$q;%MyxxaB z{ueK9x88jvMq8pUt=u8Pt{vmMG&J*P(DfvLV15<SQ<My;lX*KfM?!mNk7tA6`ac|d zuhW?=)csB<hUoiyunq_E)2-|tt46dKj?Ds7dpkZYWUJJIh4e~YD2{v<oIby3S0XeE zcvC}LN8u`gP*B8&qMV!!9TN}(J73{d!?_6DUt~~Psd_bfb1dl9M&bvK9r{()AXo%# z1)$afwp){};(ip0YOeER$%x2|4Y`Xx=O?>Zz%9S62+0Bv`G0Q1^jw}TVj?mvAF_rC zk(uxq!aOe<!B7uFQoM4`cZPF8&wgYnAGWg`z6kYz+BLdebcR@nQnaP5FuA|J56*R# ztF;o{yoD8*L>L%nqZ;dxJAf5!+}E8TC#w;7=Lg?++@vGtz%_ntj?M=D)_=6K`F~jS zgb-VAHsO$`8Y<u1$DWT>a$w|truRIb)PQAn(yCWPoSz15zQ{byYUR~Tt-q{t5+Be! zqH#!ZKUK$K7VV6f(|7W_g2qR5`jXR7CSlEy!+*&6o@~A4G);qIf?xIQT1M9_z!A;& zpgaY_@pgX%=miu2cb1wh6n(odK6DNgh^Mnt&Ov!Lsq;R1L34;NkYs2Ca(RyiTfJq5 zAz@{Qa+rq++C*x-G2{pKPi9?lyc6AF_DHR=St>`}GD=6RJn<!SyCIqf?sop1ovP%u z1OCA=Sf_P_qZ19Mb#uxrZ7p6iaTd;Y$EFko21f(4Ki|XKdf43X%N<$qq{S^-K<s)= zYgQZ;dwSJ!PEd%AZhg=Sv2d}D2abbIw<IP?Da?mTjO@JuPhW=>-pIqXjuFgSyYnvj z%(*HW67jl~?Edm~uY~NA^=Z^?kDv&V(T312({#qvvM$i@!h4`Or4g>4erY2ZLLkp| z8blGeyVGzUaP`Wso&|iG(3BENgS<DG4g|Yay?S`rb1va>2(<_9#~C^{tguaL1c__( zh!OONy`-WXzsF5aa-vQPYJ&!5%P~fsSmPBM2Zhr%kB08ASojp_61Dl})9xpx6Dw=y zyEXN@?br-ASv)aOj6z2_7?`?il$feoo?wJY3i1nzrlu~`h#d&mk@+atL1dEO$?VQy z1hCSJkNrGZw448~UcZqbnoCO?*n_y2KN}$=2+tr%sLs1?-kzg|%@dBT9`$lGTASyN z5JOIq-(`T%Sn$YS^E=CND*QLdo~jo<yncMj!Qf}FvMi;<{9SVL-~4emj6mks`ss_z zC9JOnCn^W$UR1kks{5rc5#$7NZphj`f8;qr>E1T!Y3zd~T|T`n>be-Zc{+QVT~NWb z-aOfR3urQYO*(C!j}p{@@dC~U<X@Qb%1(J=uj6UEog=S>N+;~d%7clITvA;_*C?~P zN_ERf2n1(G8<DhFK96ol85(P;5iFg)x_h`;nmPUlIh)%d@bN^&lR^J8n12TQ&*0kQ z$>81H=-4>9*ti+l*lF3=Xz3AHm7KpynR!@}(Mbt#u(9*7aj@~R|CgkaHVqy@os*w~ zTbf^-O`KhvpMz79jfeZ6ieEySM?#ukLPAnPgiPrFQ(}a`s%YtC?O{X4&CS8{--m4C zT+3i$X`Bd?KHr8~tG$acBv)_m<rw9!9GI}7-LUWk`DAgDlmoV=t_E=L$vYQum|vS` zxCkBeOsBm+1AMg{wLGVKJpJc74Ot#_M6!M#hJL4BJ}EL3peS;;ekf;!@O?R$TaL2A zr<>7HFmcY6Mw@F-?KS2izPekST}}g8@mI~1o}3(?iZ=sns(Q=vdoQ>MLq_hn%NqzM zX~6V>Jx8bV&G<IT+ej}D;8n<$GG~!MEiQwQrDwxl25>{F72!-~@7SGZ@hVD7<@CsM zjuq@oO0U+PXNm31Y`{W6Zz9(@Ovc^fjCI!P5O+<$!Lhx{Jj_-?FVEd7r6Xug_{d(t z#2~lL^xuypijbFax={l&?piBsCGJZbVny=oKy1OiA9t-~{Afre&J2NVieUq2FAndy z^F#=dv(~593PMEjU}x??CEG-((jx=OqA^Z___4!rJHnae>;ql4#9o}coR<9os28ib z<>Uh?wwPYMyBubkF#5a63Q$AnfhJo*FaKRmc|{oh9diZh@?UGn?hJlcp6nrd9>a;; zBE*A`6Ea%st6G|0e{)wFhE3%}bXJ;B>MHp~fBofMn}s$tOBQ`mw`YO;JupYsSDkRr zjCey^*KEQ#fIz(RbyEML9d82Gy&s7Ux(@zE<-X;1DWr?6FR+$-ITZ9lR+Mi)sb%V^ z%HyBHy^LlDWo<Vg_oV_SRZ+B6?CUpm9Ck}jjZ9(bB&=d}EX5Qa>02z$vJR?Y5&B+v zcEeaq4W`_^O)QPd4q<8}bqPvpwE24R)jhRLRi>>aSj*e3Mk{Np80a~cHv;6yumP|r zTd6bLxb{>NBa*l(T`fo_^Tk2bUSFSrvrI}wo<%MuC;cqVEi64C1B297lnp`?+S26W zJ0Tj?F&P^Y8sagU7*ttle?R!_bpGrsp^3LDv_mH4^CF5vzYZBnFtcE<iY%;Uw^IvY zJb>pI9-_T64T40a5+c7q8TiCs0B~^?Ks4QHA&5sD{}3K=vI9-oLMwjveY5+iyA*nF zN(>wiBeFpn7sE6?VTHO4`(89zM?a;^4(fth2rf6p*HwPtd1acz?pwoV^l{>+gERpC z$Xg22;$pY&BB(32MK=x17HCa_Z}b4RTXUwKM+ngYp;e*CUHZe^RMD{_iJY^zAsvW4 z&#*m}#JFwnus{TXW|dsPGXhU$2!ClK#u<VZfTOtJ42cH>u{iAvz6T%!jBp0%3UvYt z9s&G9jlsM}z?aY<uqYk`OsKdi8y;k2sF^7r9zZ5k&6EodI1=h=DwGXD6DnuQkquc9 zYHKQx4X_H;Gv&z!9)$YBX#sKO3?ZH}R$xR#=`>*s+w$Z3%^UxFbZmWf5Ur-vRlwSQ zyGEEg=+l0`U{nmJqMa}(QmQAi0a$pEFIVEBs2J;p?&4<KZC(-Bm``L)7@?Lb1W*yP z8D1^$OZ%PwM0I}surZ5BSx_bLG$jAyh$bTb6mF^V0u`~k@2L47a!hPw)GkZA1fDEQ zwFDmfU%{UP)imTQ3wF}Cr#f)s+{sWlpZt}$xro>k)GlVY%6}sKpWp;=LR$fOLd#>a zprR_e+CSvp&!NLkw=uWyZ=VUh05j4-MM(OssKE-+!D52}HgE(XBVc$Ngxrt=FtiQ4 zK7bKt9fA>k9l(er2mxY*6=ZMWe=EVLJAthFtf}cIA!<Ejf!GWkJTP%gPWROk1`Hc% zIg82ZEaIyE(z=IDch&*|qzx8L#j3Tru~flY$gt^_T9klc-9;NVn0V;@ejhe~B2-#G z78|xAaDD)Z4RZprIYen@f(=zO?Aa7uSFy)Fu9=O_@cSf92habc7>ahVej~<0$f7B- zF5*(iJp`iE25Sjh+zl8B3qmCNN<91kJy+I-q}cZ#uqVwzErZ9m(T=Fy@;SF91pMa< z`)yUAYBcG0U_o#XEI8=vqUee2!W;TUeAOK#SJI4-#4X(9{~ut(A(q8n29F7X+ocRo zLKD%4LlcpBn$Xlm!)kMGS`>Twzr)tR)<T@fR*@D5g}<Qx14XX$NcWrz)2gD3Xxb6r zmHIH^VLv@QtSw?2rHSO-FeK8iPh>-|_#(fq#3NBT0{(C606*6{I)4@PJ12ZQXC+L4 z6G@x7xm_@Q>Z~BKCA}$CZyJ2HKk4<o=V!66RfCgF;VNQYPcgZ-)urXHg4K0AH|qzK z$c>yH-~UhszY55`BRBBftp86ihc9m(oi&LN`|QQTl|H2^AbE^b&Y3>-MSoRduz#u0 zWeS7?I~<F6&XGQa#xMB?DTPyNDw#*}xGr&TJ~Pl()nVp0i{$Np`KSss&*jXuWPWeT z3@}j$)Q_8Ml}3a7?{qX%&2JyBFVFtw_%9!4O{r{%uozhzHFCo;!Pqv)YyVmth;2{> zf)j(GO#ZnUiBVTU{&`rd2NND;wU@(_fFS%c+Pn{&f@ABvG*yXyELw4qtQg!$nO;t% zh4iqiKtB`;5wEOY8#Y2{!VbGOtQj4IQJb2n67{v;GfVhrnBiB!$EIDj0~H1k8Zoke z-S@`^%-i^?=5s778zb9=HEO{6-;1^5ZJLM22CCNaPor=_{K9O9u)!)-i<e<101f{? z=pR_8ahQ$%NB#$X#Qit;Z`uE@`hR66_tYSkhri&IYR5bMSAc&iA=hSb#~w=_f9kMC z=w6L-C%B`lvhl#n%*ev*-OLMtW8@beNCh>PP-HGdm=*gWm-Z~Myzx5FY@1{-C<*?x zkBO*pvc3S`Dr8msy1&SC2kajnhKi1I%uFPp$>)&Z@+2~dzBriT*q=41W`ZaiX3>o} zs)WNciIFHe>Xejc?ypb<gGX<ShNaS>Q<?u1<ua!;Xcg)2MwRc@ZPW(G1fviN+N*9q z>bF&Vx$8r;{z2v7E6Mj8(Hi#*!4P-<rw_j_I@YvWhOSV%1YbjrOAuTTF3S#!0WUmm zA|?v~oEJQ<`@F&w4vQnRVOyWeGhh%~A%c<LWl?JP<Y16nBf=gPt0XV{wBzCBF`Q5Y z%PBx><)Ol5-hOb>8?ilrVM8AS<RmED5t!;S>a#oLC9#1Jz`6l_5hUGlXtjIkjqoT! zwegta@<}@g+&B?0e4W7@9HKS=?lIGB?Y)4XzEl8{KB$D+41C_U2SvRQR5oaY#`@b? zF$;6)sVoLS;TR{Pfst1eDTB?F|Jscq#=Hy}h58JAib<cct|&PDj`?;$f7J#VJqK$m z5gOQ!mvaUQk6sV-1`TxJoH^gUmk=)9hW$CiAJI<&X>JF`2BQeWLG@T7xfB6Hx=&w2 zuWWm+@JHT$gj_*WfNY<N8gF@bYcIna(C-N2pU+WtO+?|kXO6aY;I|9N0{Zm6biSkZ zgx4Xx={#MlnDJ6veyBZx;7dQ>;;#^IpE5e%y&A7fkZxYl2S0VEL{V@*e!hWh&4xC_ zCBQ(l57pu`!(x{Tc<H6M^CTksutuL8l<>F^5)uJn4yI|qu&nNN?Ti>gB(g1!c6x-; zcrXkWPsZ+`)gj_!YnNHvqJ+XX)fKyp8Nc8etB#pA;V%(hsZ3`ea5<vjLsQcgF4zai zn%)Txa2_`0GZmU~iwuk12_cfb{kLC-x-{O1^MyyDu4~}+O5?f4velrQB3QH#?CM4e zCLSk!MzQUpc5A^AU5WEm*P<xC=w|=W%63a&Q?e&jHX)l(g^OtZli<>ZggbSN_-D_h z{=1m2uwr(fk}esjAp#Nqc5iAB<C&|@EZ}!8+;3R~#s?g`43r^(3N6}{AwQ?S*u(l> z72Q%r%zCXq5vO{4_wrG@h4P)d#^VLMTN}QmcgT;O3M*L|8z!@uBw!Cbl3xL+e#(5h zDYzsxM<}S>a|Z?hg5XGTAD<GSEZu9kEJJgoEPG~YddeWE^m>4O<8oz7Y=Fdx0XMOT zF+Vtymcb-~mOXTG=WBWS71pqU4+E^Spf;aT2xj2`a$7vi7gw6WqVjmG!pVT?XG6Y6 zvt1z}kKVa2J^%zKOMP4sM#DSa-93AUyM&N;=`ve1<B|fZA1z@nIVC(li1Lg=5OnAk z1{wR%>eWj?a1Fg$9TnOgUd3olEXx)rgt`@kCTMN%)EkNc8zq`(TYf)W2v4?)^D(!4 z`&@7zI{jl@rqc#{G6n<V!e8-^fxm8NVg`r2;gaYsBa;{=Ba$q3KrUOD<J7xp(}*hc zvf=PR)^l2+o`$Q5xIy=j#?sQO9}n$U5v38h)0oDfE<+!^Rl$G=*q)I96YH4mnFsvd z2-@wD%1gSuh)eUxNBk$)x<65*>vP<&%woUE-oA9Qyg^xt3=tMF)`puf_=XGiq4!=; z1Zbf35>vb>%;H^`^Y_`)1x&w`uXPWdF?GA!&%m@G4}P-cY%1>3T0LXh-*ZyFM;N@v zP6iQzDBrT^-|7Py-%Jv&MiF*ZMsBj^ihtWyx({%Xn*gvB>lHb@hhfBge?{DNf)I>f zQy6t7I%0KgT)JkioCx*(X8;~ZhNa$~;A<_f{*MZ0&{PAGA?CMw`x>(jtMiaD7v^*Y zLq^Aw`d0NGd&<L(Hn$l2$Eq3Q*UZzZ-7aO&O~>g(0b@p-QHB@tvR3Dcr>MqJ@n4Ug zmg3GW`K$V*fXf$KchC3M>TbZA(xzC>HgcB~9+PM{x%{b9Rl3)Z2%1a_nhZy#n!LMH zOa9S_1MY~t53eza8>SQ5lR-{iT}{7|uYPvT+MtrZY<6*n2WLj$hC`-P;)4t?YYR7M z1?U02390kV)O*p8$7JjmGZNs|sIF`$6Aw={fyb&{^Q7DICd8m#>QtMEa)E(sL;l>f z-l<oW6|qCh5kjX<o2jGqd%MB1rfvh$9uE?v=(?_7a3NS{=fOPUVea9WhvQpdI?raW zKSViFdr`^6d4r1=tV<Zs($YJ5u2>M{!#6Ya2j!fSsKUi7ij<mY;DjVbM)qIN4_B+~ z10Ybmub;T~e3LkeZglM2X?}n3+R#6Au2ry!Su8zG^Q>d?=@N@1hyhaw+oEtPUinj- zZy(+4x4~e}+S{gHAKc-uql=BqLEoK#k${i~h<2^Tgl<*6X``PTELL|}jiy;32C@yy zHLs1oiU+YygBe^6=4K66a`kE`?#mo4aM$$~M)f)eZoG86orJC39ggF$7c?%no`cMM zhuWGw2}hlh<&oVQwwuH8m-X}E-JNHJmyQuI5U;Nn;Qr0uV~@749*>OJ9k80D9k4mi zLu*HylyIL_9IgI}w)4XEj<dp`Vu3+nxnu`gLkwzhok2(y`$LcEI^4odI-$z^b1$1_ zuj%F$R`6Y1jpL?*eCNeqW1dWMQ#w4H4xJW-E*<!l<>;B^m?T~nv@NNe_Ev>1?~dPs zd=J8wrjH`E4<TLxkK{E$T(VEu(68aULGlYhBQ3rCM<z9Pu7dY&yS+6aD5{)>*&D*W zBZHuG3g&b3m+kA8OZa(B{Q37_W)5nn$I=>|_B`A30~k@x9FypDlOl|ub=!FYz?tZQ z4D^LJ#_;9FM^d|c$h0k#$c*yY?HWyh_{XiZ?~tI<fKHX)J+c<=>&Q)yb4krGuLi{} zbBjlBMrx<?w{Mf}YIQH5wvF;0!$Uzjg=b~Aw9C4J6`d2MDIM3t`rMSu3hsO1uPoaN znKywrt7N0WO{RuBuh&-}4BhX+|CZ!3swT!=SPM*0W2}X!6m&Id&Ds)b+Eq}8_HvSH z^{%WP;$7(<I8puUgV7eqn=;bhx+C;RZ$6gTqT=`~Dw;WGwADADt2C{jPu1~uHK}<; z70AmfIt=%m*g-)!k9ptD_7CagUOQ`K-h>?4d-a`eZnb=$pw&lM9Z)-tDTYH$>f}dQ zQ|<$lAh6Jas@)PzDxh|<IBT#OtOCDrB$&{nJ`0qqo3LuUY6Su;jK3W{*kjKJ6*RZz z{@1<oI|`lpTO??8u<+k-jBDKAw%}UTV6I=Q$gW-);$Gg%dbj)dXX<xR#kPUioF8OM zcc%E8q^Uqduc{hJ5S|@zG1N}dg3L}*>fiTSzrMRso4otck{wrEggg>7Wz%HZ?*z2R zMjOuBKVQ=taFqunD{tcGUl1#6eIBiCU~di5f4%7;z=1$*kb^~~FXKhEXpe`*qtA5B zTF<K{(V4hoZ6B#U;eFKyH(3nZufJV?VpqA8?@gMNXQ6?(?OhVooBME>DK~tHlYSUi z4{!H(ZA5prnN{bdU%gEVJ!Ynb8{|AY;v%-+o}y?UDO2;3*8Y6(ZnAqMyV=%?eDVKR zbJj$BdIim%1C)c3*+qZOkf@bkl3I!-+0Nf3S<`H3vLP#?zG42H^;){C#uuv|&SJqR z{FqlR{Lgtb1e7@|I;!NoGldJ6iu*5KRtE7qBPv1zebVc)R?0JPOWZ4OEB$l(61?+i z;6PuP!j{JB{`RuWUr|$z&#&jAbJ~AIZOxPNL5OFd$y(qiJ?9G&v#2$-H-qSF1CpQQ z?e;_?BTjIHsoGATmeXT*OV8_N$~A0Vs_pj8r|+0@Tav6@zq%@FCUnqajF*S+&L`ho z&^NeoLB|%8R`KVf^9OrN)q1qOtUwVhxN(*B{CyqtJK%%kGz1$O66C+y7aJB5a3~}Y zw7`uK4_P{Z$A%LR{8!y#Lsx`+a9qGLH9=Ma&W8lDeKomU;pKS<Obkr6Fo~T6F7}I1 z=tG<}j6GyYzkacXZ&WGI47D`n*9DxdbG&9xR5%w|tUl^I08#@7n{n!Zry<7fMsf|E zxS|6b8Ba5{>9Cey2;DAqIHH}t1cd;QhjtA_z;{i%|Gw1k5Voju&JbPUYgAL)K<fiV z{xV$m$&`D6g^wTvLY2XsI~w&E+fErzy0tB^M+jX25gNvO2w}i>XNF&x2$)su31ct| ztvCFNI-Hd}0De~i&P3vWqY_ZYS?8SegYFYIJ^`WWM8pVL+|BT$@H}h?)YQ@{G6??* Dw{+iS diff --git a/src/plugins/e-acsl/doc/userman/provides.tex b/src/plugins/e-acsl/doc/userman/provides.tex index f48756c39da..cf27296c588 100644 --- a/src/plugins/e-acsl/doc/userman/provides.tex +++ b/src/plugins/e-acsl/doc/userman/provides.tex @@ -101,9 +101,9 @@ unsigned long const __fc_rand_max = (unsigned long)32767; /*@ axiomatic dynamic_allocation { - predicate is_allocable{L}(size_t n) + predicate is_allocable{L}(size_t n) reads __fc_heap_status; - + } */ /*@ ghost extern int __e_acsl_init; */ @@ -135,7 +135,7 @@ constant declarations and global \acsl annotations that are not in the initial file \texttt{first.i}. They are part of the included \eacsl monitoring library. You can safely ignore it right now. The translated \texttt{main} function of \texttt{first.i} is displayed at the end. After each \eacsl -annotation, a line has been added. +annotation, a line has been added. \begin{ccode} /*@ assert x == 0; */ @@ -519,9 +519,9 @@ restrictions. The \eacsl plug-in may work even if there is no \texttt{main} function. Consider for instance the following annotated program without such a -\texttt{main}. +\texttt{main}. -\listingname{no\_main.i} +\listingname{no\_main.i} \cinput{examples/no_main.i} The instrumented code is generated as usual, even though you get an additional @@ -565,7 +565,7 @@ The \eacsl plug-in may also work if some functions have no implementation. Consider for instance the following annotated program for which the implementation of the function \texttt{my\_pow} is not provided. -\listingname{no\_code.c} +\listingname{no\_code.c} \cinput{examples/no_code.c} The instrumented code is generated as usual, even though you get an additional @@ -575,7 +575,7 @@ warning. [e-acsl] warning: annotating undefined function `my_pow': the generated program may miss memory instrumentation if there are memory-related annotations. -[kernel] warning: No code nor implicit assigns clause for function my_pow, +[kernel] warning: No code nor implicit assigns clause for function my_pow, generating default assigns from the prototype [e-acsl] translation done in project "e-acsl". \end{shell} @@ -647,7 +647,7 @@ even if the \eacsl plug-in keeps the maximum amount of information, the results of already executed analyzers (such as validity status of annotations) are not known in this new project. If you want to keep them, you have to set the option \optiondef{-}{e-acsl-prepare} when the first analysis is asked for. - + In this context, the \eacsl plug-in does not generate code for annotations proven valid by another plug-in, except if you explicitly set the option \optiondef{-}{e-acsl-valid}. For instance, \valueplugin~\cite{value} is able to @@ -678,7 +678,7 @@ plug-in is running. \section{Customization} \label{sec:custom} -There are several ways to customize the \eacsl plug-in. +There are several ways to customize the \eacsl plug-in. First, the name of the generated project -- which is \texttt{e-acsl} by default -- may be changed by setting the option \optiondef{-}{e-acsl-project}. @@ -760,7 +760,7 @@ parts of the translation, as detailed below. \begin{center} \begin{tabular}{|l|l|} \hline -analysis & minimization of the instrumentation for memory-related annotation +analysis & minimization of the instrumentation for memory-related annotation (section~\ref{sec:memory}) \\ \hline duplication & duplication of functions with contracts @@ -782,7 +782,7 @@ typing & minimization of the instrumentation for integers \label{sec:eacsl-gcc} Due to numerous instrumentation and compile-time options generating monitored -executables using the \eacsl plugin can be tedious. To simplify this task we +executables using the \eacsl plug-in can be tedious. To simplify this task we developed \eacslgcc\ -- a convenience wrapper around \framac and \gcc allowing to instrument programs with \eacsl and compile the instrumented code using a single command and a very few parameters. @@ -793,7 +793,7 @@ In this section we describe \eacslgcc and provide several examples of its use. \subsection{Basic Use} -\eacslgcc instruments C files provided at input using the \eacsl plugin, and +\eacslgcc instruments C files provided at input using the \eacsl plug-in, and optionally compiles the generated code and the original sources using the \gcc compiler. @@ -819,13 +819,13 @@ is enabled using the \texttt{-c} option. For instance, the command instruments the code in \texttt{foo.c}, outputs it to \texttt{gen.c} and produces 2 executables: \texttt{a.out} and \texttt{a.out.e-acsl}, where -\texttt{a.out} is an executable compiled from -\texttt{foo.c}, while \texttt{a.out.e-acsl} is an executable compiled from -\texttt{gen.c} generated by \eacsl. +\texttt{a.out} is an executable compiled from \texttt{foo.c}, while +\texttt{a.out.e-acsl} is an executable compiled from \texttt{gen.c} generated +by \eacsl. Named executables can be created using the \texttt{-O} option. This is such that a value supplied to the \texttt{-O} option is used to name the executable -generated from the original program and the executable generateted from the +generated from the original program and the executable generated from the \eacsl-instrumented code is suffixed \texttt{.e-acsl}. For example, command @@ -835,9 +835,9 @@ For example, command will name the executables generated from \texttt{foo.c} and \texttt{gen.c}: \texttt{gen} and \texttt{gen.e-acsl} respectively. -The \eacslgcc \texttt{-C} option allows to skip instrumentation step and +The \eacslgcc \texttt{-C} option allows to skip the instrumentation step and compile a given program as if it were already instrumented by the \eacsl -plugin. This option is useful if one makes some changes to an already +plug-in. This option is useful if one makes changes to an already instrumented source file by hand and only wants to recompile it. \begin{shell} @@ -870,7 +870,7 @@ A list of \eacslgcc options can be retrieved using the following command: -g always use GMP integers instead of C integral types -q suppress any output except for errors and warnings -s <file> redirect all output to <file> - -P compile executatle without debug features + -P compile executable without debug features -I <file> specify Frama-C executable [frama-c] -G <file> specify GCC executable [gcc] \end{shell} @@ -886,13 +886,12 @@ For full up-to-date documentation of \eacslgcc see its man page: \subsection{Customising \framac and \gcc Invocations} -Runs of \framac and \gcc issued by \eacslgcc can be customized by -using additional flags passed the tools' invocations. +Runs of \framac and \gcc issued by \eacslgcc can be customized by using +additional flags passed the tools' invocations. Additional \framac flags can be passed using the \texttt{-F} option, while \texttt{-l} and \texttt{-e} options allow for passing additional pre-processor -and linker flags during \gcc invocations. -For example, command +and linker flags during \gcc invocations. For example, command \begin{shell} \$ e-acsl-gcc.sh -c -F"-unicode" -e"-I/bar -I/baz" foo.c @@ -905,8 +904,8 @@ are output using the UTF-8 character set. Further, during the compilation of It is worth mentioning that \eacslgcc implements several convenience flags for setting some of the \framac options. For instance, \texttt{-E} can be used to -pass additional arguments to the \framac pre-processor and \texttt{-M} maximizes -memory-related instrumentation. +pass additional arguments to the \framac pre-processor and \texttt{-M} +maximizes memory-related instrumentation. %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% @@ -916,7 +915,7 @@ By default \eacslgcc prints the executed \framac and \gcc commands and pipes their output to the terminal. The verbosity of \framac output can be changed using \texttt{-v} and \texttt{-d} options used to pass values to \texttt{-verbose} and \texttt{-debug} flags of \framac respectively. For -instance, to increase the verbosity of plugins but suppress the verbosity of +instance, to increase the verbosity of plug-ins but suppress the verbosity of the \framac kernel while instrumenting \texttt{foo.c} one can use the following command: @@ -924,14 +923,14 @@ command: \$ e-acsl-gcc.sh -v5 -F"-kernel-verbose 0" foo.c \end{shell} -Verbosity of the output of \eacslgcc script can also be reduced using the -\texttt{-q} option that suppresses any output except errors or warnings issued -by \gcc, \framac or \eacslgcc itself. +Verbosity of the \eacslgcc output can also be reduced using the \texttt{-q} +option that suppresses any output except errors or warnings issued by \gcc, +\framac or \eacslgcc itself. -The output of \eacslgcc can also be redirected to a specified log file -using the \texttt{-s} option. For example, the following command will redirect -all output during instrumentation and compillation of \texttt{foo.c} to the -\texttt{/tmp/log} file. +The output of \eacslgcc can also be redirected to a specified file using the +\texttt{-s} option. For example, the following command will redirect all +output during instrumentation and compilation of \texttt{foo.c} to the +file named \texttt{/tmp/log}. \begin{shell} \$ e-acsl-gcc.sh -c -s/tmp/log foo.c @@ -945,11 +944,11 @@ By default \eacslgcc uses the first \texttt{frama-c} executable found in a system's path to instrument input programs. The name of the \framac executable can be changed using the \texttt{-I} option. For instance, to instrument a file named \texttt{foo.c} using the \texttt{/usr/local/bin/frama-c.byte} executable -one can issue the following command: +one can use the following command: \begin{shell} \$ e-acsl-gcc.sh -I/usr/local/bin/frama-c.byte foo.c \end{shell} -The name of a \gcc executable can be similarly changed using the \texttt{-G} -option. \ No newline at end of file +The name of a \gcc executable can be changed similarly using the \texttt{-G} +option. -- GitLab