From 01c55716eec8d517b441e5dbc4f6d05dcb2c4be9 Mon Sep 17 00:00:00 2001
From: Guillaume Petiot <guillaume.petiot@cea.fr>
Date: Thu, 7 Mar 2013 17:13:42 +0000
Subject: [PATCH] + get_sub
---
.../e-acsl/doc/memory_model/article.pdf | Bin 119320 -> 119412 bytes
.../e-acsl/doc/memory_model/article.tex | 4 +-
.../experiments/get_sub/Replace.c | 158 +++++++++++-------
.../experiments/get_sub/oracle_getsub.c | 36 ++++
.../get_sub/test_parameters_getsub.pl | 8 +-
5 files changed, 142 insertions(+), 64 deletions(-)
create mode 100644 src/plugins/e-acsl/doc/memory_model/experiments/get_sub/oracle_getsub.c
diff --git a/src/plugins/e-acsl/doc/memory_model/article.pdf b/src/plugins/e-acsl/doc/memory_model/article.pdf
index 68aba819e021eeb86b20d70db6d34042494b1538..9442066c1b36e315776d69c92986282a8635b8e5 100644
GIT binary patch
delta 14216
zcma)i1yoi0)-Ris?(Pt2b_XHd-3`(u4T99BQCdPkN<tB&8>9q8K{`bcB&3l>1k|_B
z{qDQ>9C%~AZ;e6CJ@Yr?zt&`Bl@Oei5Tsb*h7(45J+Zk2;H6mt?gBE?@&H1B&a^>*
z7=R`X4_gE+MymQ^xYa9ic#dWst?*h18?2_#K_T906S)$<2T7eKfBVxdcQ#bsqxY+|
z2Bgd2xHzAE@5J~E#Qi8Gk}#>Thg9T_vJ>Q;g#cBk>=F-iVTF?D{>PWl&af2qq0dw+
zhR&ssz88*B8D-0shDM<#M{>yXx3Ah!1eW|sls4z+YKyu^wa3Et!ucT!zdwLhs9%9>
zOY6M2X|ieB1&RE5Kjl9A(OlBKW)LPpF>Hd@a+$?etUHrtxA94Ah2Ct#sj}&3P0i>C
zcDz$HN}BI&o{)n<+>@(pE~fKkrN!~LFS~Ztxf1x<^k#{OMjuDB)0nH)IL*|NNWbm@
zIB9S7qIHko_-*3`&j8p?w+H8o^d5YX-07uB$!}=Td?2;u&O@0>%EE8&<>k-7)YNf)
zIrlC$QRL%>XWXGHyu88ki8Njs&%BY%X>D6{S!7a1l;)zU;N!~28Vv%RL0K$o^LG>i
z@?c<xhf~E$b!SoOD-gp+GyMsli9tqQgY$L7>}d0+^X!dE?g1t3*1C&>dW7J3JMu?f
zZ#`2eQ)3f2xV1jO`cKI6t8P^^q36Be94pP@YcD7ws`!DXR;-Hx#n@Z8*))`uuT;N&
z(wyTE?<)VJL)q=$m{V{&?->-JKc3MSw}Krb=q_!{<n{$1zyPz$K)F&`ig_s62fu^G
z&!Wo|yK3ij9PU(&^Lq3sFW|g&ol%^@=I+B05`UE|XqR!@C?X;F>6%p?z|Zbp0oy#S
z`ogSs6Pq(6ao3h9{_)`P%Zia_3ZQIo$L)fM)`+-HllHD}?M}9@h=fmge$dPJkz0QI
z_WdzwaNFFWTgG(GdLxbDT`Q`f0Dm^vt^GZ8=y{8fmu;}wlz!ottB{Prt#b9W`)V~#
zV;AOIZ)4-x;uan)X`voyhcOO@HE<;=kO+_*jX738>4Uwra?Ig0PHVP&@!DRD`u!|q
zNA>h8KVhg0rHqKW0JPvMiOLAR`C#!tSUIkyAa{<B{`lg&>3&DreqJ$06n4_?V^t<7
zkz3x%7%|1q&hw`qD<rtw>F=JDwBrj@)RB1X%gU3TdiQ?IILNq^HJcx!T-(U|!3Wk(
zPqV}0W|?fHT3QnjJRDxsuULbQy-~(SJkq~aLr~18^f0X$4}pC<C~X1Hk7!gahq?I3
zkA5>h%?zKPzSH+GaKcqo*vfB)1qBtH_3wRQ%vGe8mV+-%D8rTuQ@gKZC7HH{uK`F&
z0~2rq`05P_-~fO|TH-BzY_j~c)mz+@WMj`9&c0AkgYc0Xku*xNC2918!T@lZ0-*?6
zdBaz)Y_8G}Fi8nyEqwj5gW-qn23q|!R$09U`5Rr5q0!65q8+g(%2j22``g<68olJd
z>)iAMNT`m>$}^pqe}qYC+~%S@xwS7f<|>9Y>TbQTtza4S1ZJ;!#a)57$FVBRT;wIy
zv1r*Z3(47oX{?^LdszPPKCk^w6L+|Z{`}Kv<)r9fAS}jmv!P+u_^I=lchQ7;EbsYc
zf|fj&c0ka`l<vvB--LOR_-<>DUgWF3-*rk2_*9u_o~u~9J3#|j&E=cF?Rjv1dt<30
zMm(Al8Xn&IB8i8wHFzYH%B<f++ne}4Bgn>JS)Wa7^3Kew*zbl=qHtZU;;>?hQuNhX
z9^Eeb`Re5+pL{^wAWmg|rV4UDk&x`2X_djWj*+o1*SN<Y8PWFz+lzA$3i{YZp>6Yf
zIJQOOp<(nw<!UA{l{bTx!lqvIWj)PzbZc$jDKZtbIT7rrld~#eE&tH^=xy&K{>V5}
z+h%12H})0JX+Jm9?w!j}Zb6VcXbmj^^5R>Z$P?4+Pb3N{wOSD+X4gQp1Rd9tJ?{{r
zY4rCHf4I{iP-!+;<R!5pr<Uomi>)R4yMyY>BkF*A%!`vL7C+N968EDlVZN*La^coQ
z2ir%VQUydjbXdy{89XEQ2zH06T5LAb2yTBI(0z_O+)QUK{S<bV*pCexOL~cZ-JyG8
z|1JFu;eOMtd%l)QW(S7RzwdQ~HwBp{a}0E5hx*n1WXfk&D7Dig_+>PhYpSQy)0_>?
zzTaN^NS=96ve8s-@CR%he`Aa9*-X^^o^8q)rQ(EOiML%A-CZBMgGW=;K9AiU>@f(u
z^77|33#a1j8lz=!95!9&)6b_DM)#+cVhu}okLBqU(EIHcy;%_({r0lmjckRk5@0WR
zRm6;+_{}PQ6&JL+@fp{*PU<dyQhp4>QNDEPOKc)s>QJl9u#0IDiTwxgY4tU}VcHj|
z*s}M%E;vZJCd-B<a!FKP2e$vXoKNh^(fJyX77^v1Q~JzF{TB60R(hej7is8LO)>_y
z$Es^JyCYwhBP~X#&Lik&UCB%KTI~m?E~?BgP(22eAlH0`P1U#Q3ZV)H=yH4ogMIbf
zYT~OZSie4Au>Og{57uN4CYDpVS^GvGwwMw^VdYG<M2^DaGI-Kc2INquzsPU6zpZYd
zG$2pTLJc9Bz+wYas+V+hFGs(OwozqBh&w!97HADPbg?gutQvS7BrJu)XKL2srpNdJ
zv}YW*)lRpi?kzjBzP%i<T$3A<^>c6;aaDGl?_oPBxI2iyZL!WAQGCm}O~I*X+OI=(
z#FNMSPa$lA&GftS?Pu*K##JIN4J;DAV~?KlpCo-}@D}9~G2bqBF}FkKZ`dnzlXWg0
zmVH~nHLj2ZNf*ZpF_x{5LSG6KaIudFvKf}=Wn2ggR$G2ZXL^%E%U|WK+MyNLuy<R-
z3sipv!<T@4s)|E_TzD*C<f+aBa+%U9b%SvpiJjr$i>Fkt*ws(=0DZ<ip8}xeOgm)3
z$|mC)v8qaq0TyW%&Ck)lq-A%pcQ^HDlh--SMdnRO`Q+Z?`j#QSJq71+WvlzYbMt@Y
z_sYEP;SMoH*LqmW=?fnZr^y9To7ySx*TJ24c+rdB&qN0=DCB%x1b5c)bv_m{g@HvN
z+|?P~A;JQLCK}C&8$_P7+>JdY9XviZWTVgT50#m?)w|^*U#_d77k_uzB${_w5-5>k
zY5)9{!LA&8A*tW~3Hj^G00E3oRUZ`i`uFhY513jweoWTMXCd)|th5vNCFr3(oFR`z
z$$t>vM9`N^h71-y&TjYNp@j(<OVbzpy5|*SfnFaSQQO6j<(^9g49cnUYoZ@=OwK#f
zJO1hG`h#;=j&;x8oyE?_*W2FOjmX~J&cnuq2n^x?a{ToR1OWxr<B})Z(z8yLS5{pJ
z2zH4=UI(83ih<NFpWpfOEA5rHCLl2Fhqn-#UG&hzc%zZoy*bybwEf8gWOx1ggy7FF
zKOG&}3kpKKcu9M<u`=nf&mAKgbANIK)l}blnS(oc)V=5VSSm%pNlp79xf6?mf$2;!
z(KCMgOdU#&KHX0W{BPS2dZ{NOKj)m}vzLgdJ9C>H*jYE)pZ26vs+%o|?miG?jl3Pd
zjE=oEC2nlrY~B|3rm|tkwX%)P=R7iFh%v6Kp`xE$59l^UcqR5hdyMfQH-i04k^V~8
zSCXv8hw1}?<{1m?NH^PO;KJ??=gfv0P7<y8bH8k9^e~panS&eW$BMeQ)bAeOU!&t<
zo)I5FW{{4s*1sopSj&AIMK?rLUn>LLszblcck{=_pBf=Yv~YQ}JPiy8Cf`elr4TYE
z{4BiDJ!~f_`qrb!jMz90FrT6XR$aBHt8dEU4Jb9L?^gTdL`t`3Sp3K*?o8r|Fm?&i
zoC}8`=(!4c9|cF?(<AC}uB`He%6BE*e`x4G_8&s}`BNvtpmQdqeM~PsH~1-3!Vb_V
z4in~EDdp_0;ZAsN{Ug|qO}pohqee-UZ3A$0&q+FvZMv&I&V|7bR3A8poz4_cb>F@#
zNJo+9qfQIB@_YmNY9ph-`no-F5RdI`>lTuP(<(3^M{RI<N4SSf<~4t`;BUq4Nn)go
zbsN^h9yP&e<`mWKX=$QpehRg)SIs48&t83%4m!OT2dQ2T*?N5D;ZWUbd|f{E@J(u2
zGya7zecft2U49819$jOWVo$sY<u76SMB-V+!~-v)bwA<0i{hqv(9P*tKuZHZ4Dpou
zmPC#0w*}x<<$e>n10OtSH8#_MZ|BE6jCe)E_bp0XaSFdg*B?eftXRX%;m!5|ZI;%w
z{2FQ*ujMtW&aljVwRwc?m(WeCUwq=C9o<cnez!I#ql#4d#fd3LMmI#7D|{G)ZN!l{
zL8^SaCj5Ny{nrIqLK1tN`t<I80$w9Z<Kmd^7`cw>3>CG&M=03TpS!+Zh+{()h`G#T
z>t&rWGCd-r+{CHU@cidMJePGzw2$gCeo1N|EJfCuNPg&j<M*Eo(afEy+l}Wg3l=@}
zN#jk}&hnO|C1Veq-#hr6%TC~zP(2h*QJrVxc+&Kn!A&qlaSgv@!jSoGZc)RqaC#Fk
zl-(c3VM^~$8vuIRGYH%p<~i!`#j$PC2@SXkAn%K2XQ&pti^luK>hpP60qyu=VSLkk
zcH%>5An4934f^Am3{M>0flemnLO7o6W}Uzb_j7@{*_GGh*(=AT^|AcJg0B>>rk@iH
z^Yby~or0brI5N&%!}XtyVm*e=zIU<=hpu2q>#EAU;?FkdRDG7Ak-J}?9<co}ed}Gu
zxZ8x=oJ}~KzM8$<#_i_Mfj;A6{e@R-x3~B003W;6IwnXh_9ZQxQB*CGqMZ3+|9rP(
z`K^{;5mO}Jdwy4zG{W)u)%0Qm9Vg^7&x$@u1Dhzhq18>A)htzLfCggbt(?-j#K}QY
z|CJcxNo<CXlCZXvN4&r>bJ9z)9Zw#9U_DY(P3E0UU*XqRsvNm2c<8GI*^DrpW*!6V
z<uKUm312LmdsN@E_&>vQqLL%d`ed1iya{acrJ^Z+GmQ>#6xNn`NVUe^R|(V+n{?^?
zDB7eqGaF6KiflZ(J=5#pIbCfo1l)BZ9RtENj31Y+5z<f(Q}+b3+%3l<wVaIdJ8*d>
zy<CQuHVm%Ylzu1QV1vH>GWE8$`W<rWI5H@UhTzQdE0rFSq{;W2v;^aE5yb*HMsfTq
z8Jx`(KB0Wgh?G_cv3i1&)Z9u3YiyfcODh*$34Q(v?-kf$&D&MHE4b#1GwF*W;@<b4
zhAOEK;PO7f{oQOp=dkCl5r{8%qO2iXn&L|us;}uitbT0egK^QIesO<xjm&1N&MG{;
zB6Bcabum9@X{|PO>#*kABxmN-ESVW0X%WWRUZoZ+`&@6P9ge8dLftksML=U(Kr=-F
zD(jYYGkxfXjukD6$0ss}x$KFG(fZ?=){#Cgngw3HiP$Lx1$lqg=a+XXGgF4jja!^Q
zDZIA_J-ldI#)F}WVXS-5FZ2|@>O=!brcVRn^xk&KGgv%T!d*P;K-1Ev?`LggVk0I^
z65|kiNHO;<y@<RKsCU)}lMO}oJ5y{^{;$%sg{tW;60StBeVTSc3rN|osKSD<L%`3Y
zaCv;cR1aL)k38p0NKI_l>Vptv0-h4Hy+r4yU||P7lo~^;g+u^Fmj<$0imMBWoaj|0
zx*p2l7cP<0_$#1-RXzt5?G1X07iNXq@F$8LWwr50S4g{iRyp$BQ(VaiStJ(i*b5xp
zweX$Hxr|;u%ppjWDl-Fm?flA7wy}ot2qR9uy^bQ441$J6w6}yHVyEyNE=2?GhyW8#
zPS|p8*J}zm*2Z)<3C#=~$!6DVHZ(gce5HvelBGpEXCa&!aCDKAlIV6SBPJ+MW!kfc
zT<8dh`mYBCXS&Z{a{r37@6n%7aC~tV@WXwXfUg8_#O9GS&h-HB{Wn*gCDB>7F;l7T
zkaIYG-=eWt!V9vu%3kU<n?|k_o$8q_-8-FbQ}2zfJWH+V9~>%>C)=Fg6O^o%Eg!=E
zZhO#&TnUr9SM}?G2-4*pF2AxEv(DmJ1>XqzBMyV{$4#VHv?hCo-6q##WqJC%BXKc7
zTIGv@8K|%-QQjn%Fum0F;3ELNmMpP02iB)2V{B;(q=coE7MTqFP&*9F?>?B7xl=vP
zw+`6#&Uv}4n5+O9cGunP=jVJEm#FDS8Q0mw6Qs{8I>|Q}Uxj+FS{ah5oxbS6n|lW>
zt}QTpOHcQlJDe?2e4uzeQk)}9<WGKjL@FaOFTq0}F(5$ZdoVLKv}OgCF)r8C*_5ZY
z$644d6cNeNRpr6PHBdy<l#q5Y<X7#=M9!JM+5VjTtB!vAPKZy#1D5EZ)R_c_vL+Qt
zY?2?j={&35iM@oAX8VkAX5K09HQtZtZ2Wg44oK&^>{Uz6^-_f$c~Z&q7y5trVYt<v
zoiBaVC}a9nT}ob*3pI+5Sg&wz8QLF4l4!aTkqw5BW9xQ*Sti5At?~Kp=Ijy4-V-CR
zn>@boR{D9{BdxcW=~gfLKYm7<$*3roy0Hqfdhus>db4WnX3t2+IP`+wPr?r;(Vx$c
zrut+yB@Pc3&#pYEU+<=ahGfk|zqwXW7w*lkh6DvquobW?C4|!VI4nawZ3MXGCB=C3
zntweK97s0WJ2VJtze{v0%EaX1RMb<GK)#>H>PiVG_s<T2Z_17S=#5FiIq2)n(2%of
z+sjH-z&SeEcO{!*dciDU{o|ZuJ33&eOn7>i`(cpIH0o#C`ChAqbAOJ>-7iB&TMn86
zKN_F3pG+o%!rgM}qlOK`+PMP<H}8>-e&;z^SZ1{3FYZhjmt*d=&yBU6d7Wa*@VR9C
zp^>V%`_mOF@;lDQE6dD#=^q9QpKER6(KElt{(U5y&`GBEDRnkDp4yqLgMboEt_{PD
zUVgJT5{MJ@Ek?=g(F|EJ&r6dYAT>#-Zn#Y9s>fUNhFP1L;>I*^5H?T2NR-oei2>HF
zqs0dst=8veto8L@2}=yQZjC1fvsatpl)PDzBfvQ$dnh!D`{}SA8D*a&E++4c=Ndw#
z1TiF5s@-#BSBXXUy_m5rq&SL2a{{xXC5PrIo@){baC+AWx<vHID2Pe)DN<Gt&P9QJ
zZDsOfm%epR`bB(v`#J`l<fwe6#%zPl8~?D7E-(%C{UeJnfk+#k3fVwzmPOP=F9KBf
zgzWfRIZodzXOVbj|Kzc}a1&0I9|0)dZDn39mx$rm0cmf%>4`~by0^<Y+6Ro29#%Ds
zb(adJwCx>SqA_;2mo{sm<VuHtxXfFCQkW-F*8Rafm7NH|K$3&@Se751KfiP4gqh{#
zaLZ;{p7WXUbCR07wiQ@Wx`rlw=M(1RT;%GT78|mi&;R{I0<G}ibQ0MdJq+)?wAXUt
z&Rf?)HpNIl?g1XNeO2nUM&BkDq%rlKc_<5i8gTk%P2=-7o00i}ps8Zd+C>JJh%NYg
z#;QRxsT9SD=HFM~#PV(e%akfL-yFwXw<wVoUx#wpwAQUp9-e`(=7oN%8XpDY86@-P
zYmo*i%e~iX<_@KA_Z|@W+V*a_VQ-P^t~x;rJ1NCGS?%Pt^Z0nq#U1oW1MhgOZ;aFL
zs<34FgTa?DbHoqybWGs1sa3;!g38{@$_$CS#SbbfdBhf)$VzDWTn~Tq=Kq>8oVmEm
zPbOph(Co8-NqPOu_t>Kvb`!$+svM7v*!j+&0jvJE)b*dWeae3vKsZS=S{dyg7Gx6C
zIW{I5uqRwZ6)=h?J65HjD*(-tuXuPr&Sk0hirz}^TRQg*f#|?ht+vr#g<}K@@hP!m
z%aRf@5!=J*(ks!vezK3CUGJ{+WQMXBvy$kn&HZzGu>jM6F(F;KEcYld#4~K$G?z(c
zXZc4|dGVN`FYjqa03WW*2kFK)B`AMq6>Nu>tA+(}o)Z@I1_#(^g1+zMEhO$xop(6X
z`6j}{)>NkGU8?K`UyD?(%K088PRZ?5_+e&lo!W#tzmnDMO`;E2c7k0ME!EE~=%&i0
zaqoSsm0+6EkIXP;%e4M=;Mag-*9m@~UgC85GV*dpb?UIF%(hO{u7fGz%g&PK%I#eC
z0oKGmsg#q3CF&w0v{&#Qg*&#y;|ED3kLVpaT8Q=)Gj$c(w6q@OsW8cQoPO&QEgnBK
z1AHRdqBjXe#x;8@poU3iheHZpz^{CdimzVn+3@gwHpe-q@lKypjKi^0Ny)P=OzUja
zmf)*iDW%IM<xlgfNxkjJqgEujdE}()lik#h?P%33ltdysjP^^+J6w5>Lr*>1y|-2N
zDQZ&xo9?q$kq~aPuc^>xnzx~$jCO_6Y{dZ*>sr}`UiU;*-%!;;6OH><{jA<zy`>v{
z@?s+kSS04s9*kNNF^J<}ioh2?p~~!f_5vnvvlii7f^(V|!Qq(5c6+r76yH3%<Xl<R
zcrnAoT^;=bj|t5^aI3vBMh9DZRkRl;h9NYgChg$0L$8NXMMPG(@g?;;fmi3ROcg|@
zQa~G~G-3_QxcKS8-4iIs2i%|TWbepv9|J=3lLyD9o}}XR&&lN785hzd`*@*HY-0LK
zSm8@Rl~U9>vB8&Qn39v{%V&8jzPY5>la79Iolvg+3Ryq&>>j-aPHB|H6fNhIVqR(a
zRm)~b<#!TXkhIBNkuh#)*l*IdRNA+QoV&@d{pzTv-<K7osoIOL8Vv2c6ph^&Ugt3_
za=?nmp#c^2Wgq-G;V{gX*K6zYS~1p%+&XAV+MJ6NQzC1QnS0LFC}VGt*nB8;9EK{p
zr@pGl!$6sgc3$HHnE1Ra*)=WQV64sFUCMD{PON&!ahaSMp{=A=BgdZ=ZCo+t%|o;(
zIx|K51m5P+w(q_V5(*OPU5J?Z$#Z|WycJ9CP5FAVr8{YAPnZb*t;Jg}e`Y0xriwPF
zj;)e%<Z~Ve|IEp$9yqq&rV6W#fchLs1k%1y8*A1wL*H+mPZAf;jEtx;7VhAYD;eo2
z_eP25;Z>GNuIV+Ijr8PPHas|ge=sil!_lq#qeDaHcxunB&kRdcY(>JK=tJG3UKOya
z7Al4n!E)*O+h5KexmgD%QHyVAbal^?j^b^RhCzurEr;l&`8{t-ZOU!EcMdl{;BjxI
zQSXlg%b@j$%~wprKF(p4xh~Ru;*xP&Onjra2xfc7{UD}g%bA=;GTDmi-u+`LqQ0-<
z+~XZxZV%Y@IGi|p7yfX<>1Ut>MeYh;5Km;%t5bDt+hLln*;>9lzf;q;%LCt~^h15u
zXr?1t#&FhR%Mh6k=YHJ3##h5GdXdzjgwe5qEW~L1Pr1%0V3JQVeZ7r5w)T?y*||wp
zloyo$$^PV%7|*t7p7KQ#fkPYzu^&DBpOH(t!1!s@a%x(z+UUAjtKr&t0bOnIijBTM
z?*(=EQACM!+65F=$`Ef2QqoiKIdldlemyesrOQ3iQBNtEJuahY#A3X+e09oYw$L@r
z5rVd1MX+RBcuiHr2z7{F0zK#kh4V}LPe|#ip&^IBswWQa#Q6^#VZIxs;X=14Y64Tv
z7|-DN<Veq0NnS51tp(QJZpmPI`+HA&1uSEJW~ZSHgjNQ7t?+FeEzFurPG!t0g;|wZ
zIaTMy)84*&pxXMVf0^~jtH?2j>du|WsHX}QlsxT?bt3%CR%YK1CfO5c#RoXesN1Hj
zTE{rL?j60G>%xMLmfK@CQvcjdfq=k&FQ=eLRQ*BJ2ReEP5-9>g!a2Zjga{l2=76B!
zA}}DVel(|y7GGV_L{mjQEwt7Z56FQLNuw-br$xY#7$ras7!bmNfd94aLZT39Ty-E?
z3=af``TO7Bkthxr6q@Exhe$iCs!Lm{VXOD3=NRPvAFYCVin<ygFc2uJ=;7`wE9((p
z2ILS11ECy97&x;o1fVGaMi7Z=IQ#fGyE_^=+xa?iK)`S!Q8_1TZ#{coK2ar6RZ%rj
z4N*-|ZBac@Yf)QKTMsukYf*bqM^UFtu}}a9jr{|AcTrzaUng&Sdr@D14^cnS2bu1n
zfEY9!3ch>y-{=J7zQ}y2uWyw9o;`gk#Ql}NQTOvx8x~vhm1kQ{Ha06y<@@kx5{rt2
z>I`eA`ZZ}Amp&86<rVQgea}_L_q@=yyHciDzBm>4@s^#0i#hm#cyrc!mJPZRNy(3>
zFFxz-QrlB!-#vc*?(7;p=Hh)wZE0zVPLpen!mT!Mw29sr-uW)=@q>lVj!SVrIp$}#
zvk=lvcP}@aN~$4<?x^6<j(2(Q+v#9LVnm7E6QI~><2@ODUx7c36fzT(ztNW|9Jko4
zQl6dFYV#}x^6-HJf=)(kYrP5yAFJ#OS=4$@Z<pfMMt)L>qI&Zf@mNxxp*GW47JZ-N
zDOJuR`#x_Q;@Z^nsPptss_h#0xg#F$$zy@?vJ}oKSyue}G$MMIsl!qz+^dZ}dfw!m
z5)o@+r|E`V1&h=g)w4(7JTJKN_1;|T<o78xF9^I>?)7=a*=_Ri*7jC&F!_1XFh$3~
z=eo#)kY$Y!wM}RL=e@*~M%rt%hH2;^oJ=di&A?NcIA?5-uEDM3<Wwilucg_h{4}`u
zW^7WwZ4XECBzWojj$kV735WZ01N;|oA{DIr6EKGvVsWx``R-o_%7NxB5=Kv6kIYCC
zV~m_itAEJ*POF*Mm)x1i6my08!q>~%6QXf81ODKt9P<mOR~F#(Ida1ZoQ#G<@m9)A
zX3t4zHk-cCBLG7fiH#g1^IgXRJvMO%80#{Oo(W*j-*Z*e(EX^R$G1Q%=O;71T=p2W
zHSS58(2{}HGrP6dCQC(-GQF-6(Au{%ic=A&RcHUaP=@+9VqkrYgM5A4n=_jOxSGC!
zh18E~-*35(|9TOBc&r2>r;8@2OFt6IQXvwAur}T%Q*ym;U~a5`V$H85Y&75tX0>@p
z^>mbbjqJyJs;+hSbj#a!_eNWjO~1Tujo1z_6XHQsQ3@5VJ<l+SwHxKAPaz?rjS^O8
zWgGhHEX-7oo$6gFD+Br%KKQ&QBhyz_Tx+z+W%wtZL0$>}A0&^*qH_p35OnqN%eSd~
zZ-;Uwva}6R)QCBQ@>Pd<b<Hud>oW<RV6+3EzQ25EKwXdTVW+5Z-+fuxRr4>z%<X~u
zZ<d%HT4Srd<8_mj=;S7BYK-|B*rek}h$`)vNyP)8t1FRU<3iC`JG1(uTa5(W#Yevi
zxk3#iz?4;CuP?Ydli5?yq&?Nk+#A($R{l*EukMnM3k5`SmNO1M2fGTT2tiHm(+FVG
zB`Q3r9@Hy;7$K*cO_h27%yFZsIT%ZYHz9lUzC)9+6MFT`VLO?V+l%{vIiUVx?c35t
zEFN?|Jd*tBx#Sxz@1j<N-??U+q(2z^U5R=vy3?>m{QVh0%nmzsXlr=uk?*Gu+V7Ho
zwQEv_nOq2EDJZUWy^-YcsELg=cVhdRTbTWjk3l^ll4R*u3!c`mbLn%Rn0}=qhTL-9
z{pVSpSk$M4_5+Qvm);}YmI1Xd8nn6uuymsDHqad4y%Zr5yuiD+{_Uq{%(=qXfXFkf
zce@1T!#X*Ov7iIv@LjZ;+il-&RjNNVOFo+=fkn!@mYP8ZEr`IFYP_fGba#+vcn!kt
zW(&1_>5hW};kU>1UFw>poY519pXPR4wxW54E571nR*6x+?7pv%Bw$3vOG3T>WS3O?
zV>;L^f1+G?>QhN6PAWkf0p2XsFp>7NGIb5oIry&1YJJD=y*sk#m6YfA{K@uak7<N|
zjTCSzm?=uF9d+Rf3vcte+-D2Rz97j8@BJcR*>ZMI-r~(8#|g$l!qijEI~rakeq5!}
z9I3qRkgK^wasQED#(j_gY?0evE@jm6I^z+cG;ARz26TItUk`TL!;{Qg_f9rWuHH#L
z-f`LS_LVuh+Ol|4i+;6u4^EiXnodF!ERpI>nICQRO!ZP(GAE7JU4m_vGJptP0L<g*
zqTC}0HjodFD5~$TYF@3CrU`oxLfMc;zWCeQZS2kX{;?p$qUvaHo5|UPiCh89@?E!k
zYtEO?N$;dHMl|%IGpOW|kqzH?219LKyHY8|#f1)hFM6G%9<3RuI)?j<d3u~Ek4m7d
z)|(=uM1630x>w>pl?c<CP1=V@yWqOkNZB1MA)k!-z0*@)w~!9hC~xzJF&AE`?x&8U
zeO&5ElP^}g2AoLG85|}qW3nn=!KGcN0=Au?45TqdMPXG{lcjB9TK=cLmZ!dm1aegi
zZ=E(Mw`lU<N3>a;-FO{h=~-eY-j~FSV+q0GeucgBJV%zN;vJ?j#+y<LJVrQ;fuuaq
zTe{XR_A&LJbqxI-?e!=izX}-HW9+(<KUq3jb_Cd@yd<I1d)va{%iAbJTF)^w@u9@}
zvPg~-B}%8k+Nu|ibkcpFeS)O_cDZjZDY+f_TCR1$z8P(7k&g|FT*vnt^1w@td=7j^
znQJFOO7>l}MRn^-=@4TRiCX_I@les-_2J{8B6kPxF#h*E{L^2Pp33Sq4kW?fB;(UG
z(=?|y(7*^7DivS9eaSA)j&*$Mou#FCr<_VsA#<5IbCQtb?)a3$wAu4$@65<Ed^I_p
zCuE2MhedoeBa;fQk8j1W(np7+wt1dBMn(38S@C>Y1lv!R%%B&pMU8u5Rg(@nw$M*?
zT3!KMo4rBAodSKj0woJX+9Dz<g0vPnQb-TayYQMY%)c7q2T$z^3$Y3$u&Qz!{Z`~w
ze?C9H|J%?-=oYZ}J2fMIL8he1)<IF1LLFenCmpl#-`ka~FFTm~Zk5G9)UX7xBx$`E
zDwkp{F1LrpF)1_6Ep_i$7$8m+BMF}=*H2Uo8r<IC3n+{2p+4(&Vlc`uWdGS3h-Jxj
znz1ln%9eb!c2TPF=|hKF?R{t8!RV^7z+F?H7@hqP^hj~qpJFLm4zLdEsM^UR#1qyG
zm%h4bwDo+DliV)g(XBcP&zL73cd5q^QYpvE0@ErunPBpkS8P*spLYV9Klv93X1(*;
z=6ezrC)pw>MUqNwJ1nnXC>i3Pr)*`Pd2VqL=r6gwf4Cu`g!mHQBKE*rqlC4(jeK_3
zg3gL&U;RY_Q$5j&TG>>&%7|zymBO<FgDh<-4YcD*M<DQrHqC-omGtlT-^q$wPpF}h
zhn2=3FT+BRoo#7gKuBw2pP{Pb%sSLnh51rEpt1B^#F^kAph_@rCSjDOjKFZC6<q3Q
zAy=<irTf8}E!!a1NY~I<zaN6**H|J!$`%<5o}^My6n{G0xXj%0EGJHF$o@iC+0qt`
zhyJ5rZ>1&Beev*$wLs|g8_rd){2xV__bJX7#E!n$&o+JS{kgNa#J{_BTrrg?6kS1;
zpohc9w3=Q@O#8fyZgt9-`;m$caX=BF<%QINz8?O1*}+P$r#MNH%2Ju!Dj#h1$wrHU
z)0t?hz(PPZAc3xuT7Gg(m-T|V=y6FsKngwWnd_~E7o^REFv$~+u+cT=b-G{S+X{3r
zu%Eeeg!}<x%H#Fqq9&AVt7FqM-N*A?#a@hfH2qPsWB-{aMJl=z5%F?q?$7ZvrZ{UD
zB(yDfP3d#@upqs=MEfD3oLE4NxgSw~RD{<71&(I(NCl|;U|Zvl5QLQ5OlxBO^BB4t
z@8gm!Z^*&VerD`)bDb)FBa6{nEzceb13JkN`#<f{Qq$|{dlVdRJJnTb8-*QKGHebB
z6ceR_^Qa&?VC^mYrimC=I&Ke}#FfAls6av3n?D^VwJi-QvU=jD6y2Xkh?Gd-Me7}V
z1kZk$uFbGiJn?-jMm&3;o|H^lXKoz*`#e7@KZ-5Gz|Fw4ru^c~WeobP<(PMO<o3h4
zh%D%n^f(QPr!<+;ZSTHTCo+Z*$9KDiO<#c%JY6c5?HLGtnQ}y-`Og*S&P6M}(f=ln
z`SVBlirvs~6<Jn5B8rO2XcQI;At<vI#BZJ~=(*SO>z>00HM`mPFF&df%Te&(=<YW0
zwx>BCqArnh>-aueWnXMWP7~A!-r#nnOH=LH#N+99Mu{e9#nZocw|`VTq)z^M15n(;
zRZo<Pf99no2lHc+UUQSH7x|^DYhh@xenmM<R5MpeH$<v1B$0xh?83E7#$Yo(u_kYj
zeQGnc^|&Z58m{ko3VtN2@yf~34qake*~hEo5-wvu!Q{nKMHgi67qqo;Kr+Ysrd^a@
z5@zr<edZ~x88PugY7-Tf;%c!P#|I0Fc+HYjqbwHv_OcUx2_zz%*{!ETp$(6X`V={7
z@ze3xgTma%*jXLmUmxp~`ISq@NH%>qMn=r??Z##f|LQ06F*-dge@W*kScUFmK~evt
zJEaU`FPpu+uOUU3=8K!E3WrpV#VkHux*V1S`407{91@uPSkP(-9wVKvu*g`;qLx?S
zF9z4200|Jk1<5__w(B^4GA=Esv{vK9H%ULu6Es*m;5xrtyZr6af3fpDw0&oRyF%QZ
zV0L`Thc0<{)N#?I`Cjj5H)eEM;(lE83e@ZKed{=|lohFugItCs-gHUMz1bqayIc=K
zTMnghX{0+1!>q3?&gSaT=S9sMJK?d-%T~&3%?uvB3a^)f<h1$j7OufEjb`;7jfjTQ
zu>}fcFU=@Y+r}A1y3(}97uoN=o8O#8`z?K)@y+)M0Sv_FjqmR(TQs9JR8?qYecDp>
z>%X;X^ESH>^NGK?MQ0nujrze3?K;-crt39jXej<Y0V)ssvRQHeK7}E#j?05MUO8O7
zfuExfB;@-h_n(Yv?SvXzzta-)&k;30pM3qpYTx|Naw@l=!UOA$I7j<gF_uQymO*eM
z{`OS*{&}%zK74~a&(X@pX8wN1mA~6DOWZQi6v~E=3l+&vW^IvIUp|sy*}LIo3Nzh(
zHdJLaF~z9+XwOaCIA0cFDCX*VdwL*$zmU$wx1_pcu%nRVko1KJyq+MURPQ%10}*X+
zCFKT|xw<o5J6F~moCrXI2oXRLC=&BX3(M^21PBvAK_Zw(Y((Z!CqU>H7$pKlfKl*F
z-Yx)`5Q4(6VjhSQnbutZQ9>A41O)~G!Jy3SE&z-W1jBp?LIL5;vt0l*fXCX-8fpi!
zg9_U?AP~YJkiDHS5OWE`QPxN#0%2osZ|{&9_!iLmzvDFO0mzU-gn<ZsFi;Ex5raZA
zU-SS(u93d>0OJ04`jUD9O1%FYAMc1}QuF}0|5sX@W%~ds*n$us0t^H}pin^|=nfEg
zhaa;h@UWA&_O<7e7yIiI;D0zWoB9E<XgCDU@fSEi4tEZszkY&1a0n9mPZ|&cgCbDZ
zX;2Ufv+nro`mZbq2}b;rhLMFKF-wuZ^I>QR#J^-Y|0|3kBH`d0jG0e{0n}(X@UL~s
zKXt${i<uiV5d2y^KnNTO#jIYg$wDDFVuZu~A2j&CWKkID{~IJmAp&;8PdEy*)A@%H
z5D0{TLNZ@{0Pv#0*MI^-5J1#*N1<?xl50AEFc|E*qfi*^uRYU00zx4WsOv#OVVM5;
z7a#h+&ZFRv8&N``AkcMTBoqk077!4Md2j1_;0P4(M#iCF#6PPFjqw#zRj}(upkOHI
zItp+Q0(spC1Ob9vj~IdgBW{!g0t&oQ5||`lUSj$uTo5P(d0iNYDf{buKorKxHCasA
zgRZ9p4n)AN>w|(|h=12T*?(#Wh6KY9nKgp|9y9`evjQ+nzw0i*;P9Kc0TGDn7{NdY
z(DgQh0%14sg<`z_%f??h`Hx!=1PpRLP7Liv1wf!MDC8O*7>uCTlLLa?Oe_Sm9sOHy
zf7u6O`Tz<38}Z*X)Qvd+#Z=jK(4h$E%>jS}qOK<bf&@dZqXj{tF$Huj5=@0+*1Z4n
z;lIcr;WwKdi5V%^`Jjj!PGeBGfhrgX2LB5|O#FW{g2XI$uNy|)fEtP!5Z9mv0TFQc
zjl9Dl*UJ$EgkYNOZ#MpgKjvITUe6~4b#od(peX3|M#V$|z3wy^(|^|ygkn1S8XpJ<
zLZWZx4h8;eNB-CKUu01Kk0B2O0k5HeaRrFF9taqPxhJ@x4}$!kLjT)LgrH#Hn~ZSS
zjlx7Bt`BG+1cij$ki`t%>#|_X4a?u*|5yJ(pdiF`SfNnNea|(ok(jxA6B!ijx?v~;
za^tAQjN%(9hGI^6^bNzn{}~K_haZZ#dDLM_;YPn>@Pl1X31)iS7+f&Ke_9*;pB!V3
zeN4vxnRhq{GrF$Rz`z@A2Z!ElG0Y(Vz8)L`g^Bqe`Y`p6ghFoQ35nsnR;`$m8V<Ui
zPZSaaxkmfzh7@+K2r+F3zh)SS2@Nx7(EsoTLquY}{z(I3&gC0N4HOK%adbf;;2Tgw
zVW59k`hU9#iondmf7>Aa&;1@00fS}+j{_vF<mKd0NQ5jz7A7wPR#23a!9<AwDnd|l
sV0j1%EOS@l|I1-PboVZikFT}2Z-BSG0}<wK5{7~i-M+1$rAYLD0L%-9$^ZZW
delta 14163
zcma)i1yq#bwzfkzh;)h4NK6Oa-6<{IAR*F2cZVR|El4Awq=HBzQj$_4jRJ!DkLTQb
z?m2MR`tP^ateM%f_qX5u?7g4&UHhBU68y{({3KHxKv<7gvc)BUBh?fj2GCE<1@Hmt
zQ{MxG05qw%SORF?o~)N$ZlNP{R14_W%Dx&(9Y5CP8_P_iJ`>{-HNU6+vO8Wl?B%#g
zZ60`4!FO11P_QX4Dn7qc@9VMn<sSYWCLhR;!eZ6On=0m6?<2$tT~p%6_lh&lWbqly
zB$PO9oF#E$MRz;9)@)@8E4MZD^aBl!rBBa$Dmqd4ojhb{9*grjlZH^`Xi{Qa^3ivD
ziA-8z!3+>DUPi?I48@)fi@UZVBb7dA<=6S0L`nEXsOq4EyHl1r?|oCg8Fv6y6JB^c
z*4GYvIBRPQFlqY4#G1CE#@Wa_ps=rg>sH$l+rc(P=bLXT_Z4`_^ga<0jYWswr4rG2
zX*bhAa;vo$fL_tu*-G1dx;s7el#gDwuC|k3$Xb25QB0-hR8e`?>MV6%j`H4Icd#yv
zho?kx_xQ-b@~D8Alc#}Lq;{NHqh{&%7#!YA_PN)T)rlYZRhT_%*gcQ+3>BSJor-h`
z=lZ^|E{pN>?$#tf8ZKrLO=;#Tp~|n9YJ%HLn?}8g(MB&lGdW*rSo~cf>fXn;L7IB3
zm#36uFpVd{PD_GM4?qtRfRDqBEmaOyc4AiSFF!GJk>3yOkY*shx19wl{{C_G1(-KU
zEy?@#L`)1(!d@C_%0>0hyVQUu`W+Vrla(kM32Kv}z6#k#ZEJWqT@y3R1uL4;dItIr
z8%7s2>Cxyd%6Gdu#mlqbDkxZMB?Mi26&A4%9aH2}u-W>t`GmQ{)=M9{a|{mJD*onR
z)Q}&=p0ex+iN0ibKf^X$mK>mBxu@x~l=jh}k(*Q7{LxVPquPQZSDFJ?RQx<$l@zh)
z&@bHEN1^&Yuly{q^Ig3BjjX?y`S6FQk7e|;Eal3hNqhY|?urR0FVZd3a6Gg_pv_9%
z+j*zh7by7{n#A;d4_AvK?<3aEv=f-89V5W3FBB|CLj9Fke#WJ5h6wK4rw&J8#ru=!
zQV~HzrLy`Y1Aj<~yx}ZA=62AKJ#fWMFW058&UTfrlhf?6x3=;~C|d9{8t!{~+~qNy
zsL`E_5Y_aSE_|WQ<O{gJOuOv<JYBwjuQxI;?UQ6(BZ=#QlnmL%lfI4g!}LojqlNL?
zU$%13xWO8IsphzBOo=U&%U^gO9E~jL)O>-CcPL;XqI3ve;ulBA2c#C@BCx0fQ|EA>
z5D6;jGZh~{p|xvCeTc_H3->zmopcoBH+wR}gn~Z!^t7+^;r*h@)J!}HLJpQ3n6i^R
zqgd)Ho+@BJRS=&I@TE~39}WP-r^XQIV2xI$t`M-@9$m<?`SF?J4hRpq6-p&<Ta`*h
z$PY+Ll_C^CS7^qomfEx$;;P7Zdxq6!{jgY6&iw;=fmJdJ7yYIL0*W8_#n$f1+<#S8
z)LAV}k02F4A8yfH1u1+euQDxiUc~+lO^=cpXY2eUQMc16(h=@fP3yBKJClYwN_<Jv
z6dKp+6!rGksjnYB@rYB)Cusb_$!nj_!>jMwwYlFWq8+!2qo-nfxv&|03#TScEe*;f
zhohAs%vmc35V70Q603VCZRLs33og$ebWO=@&wQhp8;cd!%v<5^ZVUqr%Gx+_9z{+W
z-976WIp{`)eJZ(e9K6kELMc{Xj!~D2PV}~tL;NqT`=fNjwS7cX^B)$ov>Q!u<0y&7
zV<kxCppO@x8ovA!oN!QFOtCt|OWx#b%DLK!;6ze6zS7f`H!+`xmU;6Fzl#Z7<!3u4
zVa(*)Sm6;&8W$~h2{3(GAz=NHeUG=b#csf)glIWWVIYB;(cb@S5pxYh)RPGiwk*y+
zoIbM0YGEQ39UXgzsVHTdG12a2{<q8cn*O$dB=kvtf1$VX)2}M@2;S4&!00!8{?N}W
z`y*pQK|dNarkA?*zPy;KYI5O;eR~u|&TmpxPb|`Pex~HfrnVC7?5!^CwV@4%y}sl7
zaXj9Y95;feyL#ACxvH&G_DRWG%WlG!yDuRfYcaX%ENOgP%E6S-Wy8k+gPB<b1M#$k
za2C4uhtfnwy7oS2=feG<2_KY8j}i6H(C>Kj`}U$C?3Xq_KMrj=db?2Nrl>NXZl$4`
z%ZkEWA=cnI@1EPy@H9u~=7_Wd$0E|vDNX1L!nv@IY$S<t^cUVC=#C(CM({=6y^N;9
zfVA-H)ARLxl@=@xsldVqz|pMc51JJsf`;fgE_Fawa8TicGBLrgv$9VIp5zUy`YbT@
z^BZEn_dS<IkT49tp?ODW@pi14aN7#)uf-%v3i=`%tfq=fMZkIWS^)69n%;Y9&#CJ9
zpk~$sB@W!M*|k$i2AMML=cOq66us}>s^_hYXhd=M5hpI;XSh0SB9nqsMOfgWl`<FF
zBbNy%LYY2jK9}3mhu@LIafmBe`-w$i!DBeB^1I2aQ;)Ff`xY}Ipz-t&p4h9Hs^2=K
zF;z>?k!G~#CXR8HMCTRTvHQX-%TVOk$l76tEfEsMJBCRD84QwATiVV{{Gi8~0SCrc
z&iijmPJ^(7BHN$2n9`y89TIH(Mi+I^s>B0nKsxI6tv+4%qqUFk)$mPH_0J3g@idxR
z9xs%ElPu@!siu7RC!c=_s~P#&chqZ+A_bkK_qm>HZ;6^MmFdr>lTLShK;X#Vp7e|z
zm#N<MP0v|X`0`uYu|%|KF<A-f)A-WZWZDkpy<KpdUwfPRGw6${jB(qv{KvLIw8+?S
zOc1kw*Shxb0O8AreilJ;v<6_Uk$ig<BQhDW9DR`*9pMMxjr2^rl6YWVhzDB68)?4z
zr*;d<S!)(H7we?n4lhlpJuIdb+8tQfr&1yXf>W&0sh1f7u(7*#IW)vGw->OZ>ci@f
z>~vr=%;!lBMcHKO2@Xf?oE<Kb=*!@+S=`x)a$c4Z$u{GbW(JLj1j21C*Z2I^LbBlJ
z`!Ngq8oL^=tWIWVSp!D^_jZ-Hmd49one|&#T6d>^iX|rM`n+eB_WfSO=Ct0-2x-wX
zY1l1mV;ecs2f>$yI+P7rE{tQ;E4A_t;fj8WoBd3Al5?5bjq^4OB5o=p>FCa1=mCaT
zfn8(?47Uo7FCT~}k$v~8@UD0J*^x@_ppjN#ajN$#JO9A(85SuCXs6l0OAN%d^ZB*?
zTBQ?E2$is(M%tja%@o4qfK@C$m~_(Kz=U+_AhnV-U_M=YHs(Gpe<v~tzU8Tqrj_&i
zSfZ?TOknhPH2M$zqawmhYZoRf4^MY%b7vxJ7b{l_2O=<t70CMc0|WtuHUh}wEosTV
zzIajlllQ?JK}falMPT3a*~eFce=bu?-PHg-si*FI=*Wz7zM7MH(pIC<Hti(^VWt%W
zkDc_Z{j0{t#Idp0$W%P@Cqc@@fGbFk;i!L-=&U}@lq#0B&x%)DznKDc6GufSJ~W|-
zmw#6icO<Q0xPpMfg6CUN+9T8RRl*&~JyqW^axL1jrer?vhL`gVzUJ=<%3d7MdUd2H
z^rQ?NqNQ=ZGS@U137B+$)-&8})-y>&UG*q!k_?y`>a9oeWWvAV1TtH3Z<Bbd^^p4&
z69@9Nv*6F72)|%+`6ZCqJ|cIfbNO-Eq-;1#5mD}Z)vi+T#wMtNzp*9BT5oP8dQArI
zPMl1-n`@Qx9&amQZXFNeKKe+C*d}~#mNnCJ4*h7XMHqnXuocN@oQyD578Q9N>Gf8c
zfTjj#@0rJnO+#MB3S!~~Zp~1T^B^02=@B^Az)0mz=Tx=93Wrk@UaVKOW<N^SFK>_r
zpcU=}qo}4EFTuAUpb%BQh_<_}qWgBnLTd#b6KlPGPQOm2XfKiVtp?A6RJ-kjDvDj=
z9L<zeLyDvDF|k>qDFkk58!W@Wvggygg;xUV1n~Grm@=7E9=&SP5EJI;fOh-tsuQkI
z=2H_#jiSn8ZUwe|rhi;tP?Vs%B)5T;xU%TU6p<t-+Bw3parm9aJhI?pS}!%4?fVXH
zP65y)NMyA%y_Zyh<GTZEcrR5Hhs3mz7P`&6s>C$5Qp<Y?+4zBns#b!bQXiX#s!ZaP
zu<!+yiv(}wC#*`UJOCvRUxH>EmVF6E6wdr%BK*sw6pvGgMel7Q;T4LuF(RVubFsF3
z_jiO$>-D#=^hez@?l4-P8`r$xW_+UFCnBjsl;+;c%;tctRoTH1h08X3n*v4t1^q&C
z;ZT>MZlJu)mNV|~cA%$Eu#nseQI)1ItU~G$k<wUb7G)ctGR>5@gwh*Nf&Ha0=GPL<
zc0eT#oMQQsF2{&FxX|g*Gs@ZX?k~Jpj?)ygk1Nia!S;&epz?^H%aH>6HcPzr5f8XQ
zd?G~i=1QwEjmbZu<99G2ju3L8E5e*HG5#~;et+ZLyhP2m)oKhRb#Fg&_^;AAKS+}M
z@==1wIm62d9x2F<(N4x7(v%CJwBJpfXu-0V!64$?eES2B(!!#YJ@NXPn?82Y6F2=}
zT1%c9lBp$?`>rA)zzD{T$ajfn62|A@M^)=5`s2%>^3TSeXubE$@uN@p<G+>DdW6h-
zf?Q1q5v=Los)MN<v{}Ohs<pmG)TIRQzh=ng5km|4Wlna6IP{y5R*mO`6ipc1E%w3I
zihe_*P<la<q~H+{w@IzQ7Kp87UmIrCQ0(JU2&Gkn43fDJ9vtOU^JQf9xF|o)em<^(
z%A>Cpp7g@EKnqSzm;se$mQ2Z9S(6xT+FCvB49!!I8lVJ)?S+35#?%;Cu5`GnKvC{F
z4R1luDY`_}P=?gu5ygb>l$bO*<dFR$32LB(N}144o|eoao>rsM<Og;i>OAiFJVZU6
z#`=EJQUQLmYWMXenS2TsBzC=tN{2~?i7258r*}xR8$HJF$Ycajs6ueAB<HBuiO;R=
zh(vy~Y<qQ|rsNaD>FZsv$*0GT9Z}yObxbi(N>wzAzqN764QdT;JdZmi<tCNjztg!>
z>$bhEjL^TplQQh`e%GMhdi!1!Xz7&^S9|BL<5H4LN=MqVl_yXR?u_sc@0`7eyi^um
zqR?3u#X)GDNH<acFk+3jJmsJTNpFVZ!VW8{yCwa1`p-Y~$PjdN9ZK(0qeB%+$YX4&
znc|56JsIYq9=v^fUMvWv-r>!wlg5)}e_{Ww@03!{Vs@TKn0Ok~q?R*&pq=KM_H3H+
zG;4xco4uU<<|{H#xx#f@PT%5oaBIMU*#PcFHoGtSt~Vt2V}*BqMDhAFF^<_C6}HIe
zoF^`xxCVY2%Y|xE^__;>kmC-54|BDb0dW6A<y-rNr$a%MR-B%n>xQnZM++j~d9oec
zIg0DG4%!Hb+{x!+4+=7!AU*w>!1`hMDLBIR6s7~%!{Syh=^h~l6LfL#?Z>#Er!<|(
zETpfZy`=6<s?;REo8|ym;JSx;h)M$>l!BYbrrtZwpZshNin5m$1xXSS*$imy)<<hI
zmx$#4UOR<Ym+fJFLPp;oc2_t)ZkH}(mBb%@m>sGaKcd^&5rr#rOFyA;9RA$!kZYLO
zy0>U*sf;>Un~#@3_o~!<sl=Q_VO8bKUzS-PhXG2JlPcnSAH4><>~}r07sPcCniPM?
zsls96sppXR^nfNXSc-x5;AoSM--32!U-14e2Y-HasT(h@ZkGhMg{w#@qcU?y@>=Gj
z30G}a|K|d3!Jh&aDiV)c;)O{&Ud9UgdQ<h`8*$UrB=I%|UDAnw5|At8nT~IAi4zP#
z1cgO$OLI}j5ojA(H&d4GZbP|u(GNU-R<KLcD$3k%-%eYeFsPK6B!`sQYie!h(Ad8^
z-;t9eY4fHu48j6*CxrdT<a59kmHosK0pezGu8;y9>s4jT6xq_TbS#$Hw@p}1s5E9%
zwYw=P)LRs5n}ikB@ei@24-G?Oj*A>e>nUSq1PZykM$jrqb*}=QtlMQJhw@mWcu!O0
zNARCY+%ows%7e=Rp-~|_-t>Hg6|#5%=d^n?;K*AX=@j5BoG~vg6>NZmj|wzd7LiGj
zrFNp{`u=>^^ixv=iDC38@y}Z<vI8AU2zkeMnr&S6BX-XmvZvX)ACD<2g2@(<Il!*(
zdFGAgQv7InmxdgBjc-m7shruU{SB)?!zQ)q@lZ3R@A+ENheTVBLakKhb~Pn(hE?yi
zI@Xyu#Zp{!X~YLtn#xuR7SC8&aTl5QStV`>Z!JCh0Y86bRMGpJZiJZxrz-ZGs#E<!
z*P*i}zL7dD%yWLG{x^g8xdu337@ju^c@a!95@C%_D0f~fZ$8?nj1C?5SzGPeyIAJb
zo8z&}3~w=g|LGx@)I#gK%OB?@qGI9+biV|`mUL#)M(=3T-!tA(DRa5Jt)FtYZhpP`
zhj#!K1wmuOaRniNW6YOZ;$xou3S%~R$s4PEzl-Dkvcz@=b$mxynu)e7S5XE1IaA=u
zBh(z}LWkSF&iULI+nP78H6oVMN~@cjDjsc?IiGIR`Fvw)gfHJ^v&7wuaY$KwWZQPC
z1*JUeggYo)R31k*bNEe7YK%E=l_&Qln!Y#^9x;q0e^;Y_?;Ws7vG}Am&1;cwfP+PC
za&w>$G0&5nE-jfqPAmXVz`c?|$(iAIeu33rplNI;ncB(k=M^|a5%oP?$o-B7A0|y~
zp{Qk!Q2fvsX3k01i5lP@I<h>A{b8u$*W{&TqaXBb>N&+;F4rqIlcj}y5d?|&QeG}@
zB5O0HWR%O7OYdq**5zL;LUcgyK}#Rb?xg&Idwd>?6Ze!JWbURSv+50zG0x(b3PM+G
z0_f&E;_##cv^kJCJM-+GL?M-q)R#v_(>URwDW2X@@%JCzX&|)Tej6e~UbnouBh<68
zqSq(>4#Iv}N(urr4s>b|cMUO}S(CM6(|!(Nk91P|ARx7~nw>eJ5J~7kjb$+n%@~O9
zkl!Bdu1PBOyDCzhPFBgA#>rMs4c;JnUy3fb=iZn;+_J)}0GMP0{Mlm?rZ=t>vI_zt
z9soNO2}{Um+&6UC3<vST7r$XGZQ`5Z(69KAEA9uJe3pg-T7?kuVZg3K%~mZrhPD|`
z@i+Hpu9!Y+8YW3~%0*Q_$sBAE{l(_<JLcQhayJ*^Z0Crx;k<D<p^^N@PNdN`-9%_g
z(eA{EJ}nwO?xyXUlQ1W~qpwegvYUnna#~Z*D&$u!x<J!7Q_cwx<Mh@**7y?FU%#vw
zbc4w|Sxqvw;bXH41SXGnKInvVdQ8<XubgVM8C(q~ez_oe&!R1o&+sEDBEif~?n=OW
zBgLfqNo=3}LYJ(6CfQ?g2G*GH0+u24(Lt)zRhVNLtWxX?MCSA<t_Wq1uk{o|ZT96G
z2k9<{7lQNap);$$W|Ua+HHByND4AW1@F$7Vn!SVXkfR+RI0ocXMY7g(@;j&VeKc@9
zllGZStO;}eG}3y~=e*p-4qV@kws)>j{OETM3yPRrBx&dz8^)e%oPS$IE*H>?t|QES
zC#|0tlF}O9Z-rt^wLixVPC1V>sdeRiFSn!oOHhF7XOQ3RV+x_pNO=W~*Uu>xI+JSE
z2$DBjGlO`e=poos6ZhkG6Flfx3q)>Z$vO~B#cSB$k!hI3YO~piUgc>#p_-2wEqP6;
z9?nWY&;2w5x+TD`*!{tC@vHW2HFW#8A|lh3pxIx5jGlPTD(`}MNOdVnMQS(E<bLY2
zT4k-0Cr0PoCGsYdoWJ>{y%e)}HnyvAOaSyjP8%82XS$8UA%@gZx13PV<U_L@UQ!OP
zgKO@-PVfqv*5Axbp>kgKe7tNJEo2IPqVglWNk6pS@7IE2XZQ)vekd)+)Hqt<3R_YA
zQuLlL^}DB9p5PV=(u2VuZx6hX>O*%=9^I15)3Dj+CHJO{%+#*H49wy*K`)X5lQ$xZ
zy&veOO?`O$dGXA^p--?x?0w?AfSg6q2rNkbp8Rv?5~Rd4oH=?up&d)&fzV^#K*!{{
zBrrYx0|R%t2KM<-fkaMNhP@-2@9~c(!)t@A)5f1>>0JXw9)sLS7xP$RRgtQ?0;SPH
zNJs;&fTD-;?QdHdk~BnLKr!z;ey7nh;QuIUdT?8LD#}`9>5TfrU8f^f1K$KfwyNT{
z3mGSST9pJv_v~Iu3%XsbBMqh5<pdPug*2CW2;673(?Z*l6n7XJz5RaWqG!GuR=d6c
z9UDG0EC8j%bsIU-aomFb28)<0tm>;3)n&!MHhDp0h-bK`K3&DSR%}6?t0CQ+qpZ0-
z9&v|G{TQIUl|2{xDBDVaJpKdzxsO<tl(x9iZ(3V?w>+FiB#LjBmej_+uw~kF{T0jY
zB|)ku;xkl*J<pZAh^E}&QE27-k32u$N6|HYoi=GTgA(T)A8F`^i6o@l0>t}$9&Ku8
zqv*e-d(kGAIDYFVVp~ZMXW8keNbSs!n)coD5H;TPy*PbPU3Mo^9wIySQFID`olK+8
zpVGGX%_5gx9*%bV8@IKG8lgLfEeV5jp+fQrEfI4Ca@O#$g>$Y;AQ$>$to>{h4%<A4
zl!=4Iu{JZ!WcL)w22cIvcgMMS0!D82=SYj<y&a(!_xA>hSX@IgnV!pm6yJN}a%ZY%
zpZ7!~bQ7&J4adRxGA|53w2$oc2d*ZDUr1`vjdS4EGxk95PEDvEZ|F_>bOQPzR(XPG
zj}w^BYZVhLpk9)VS{_=y&f+QI&mZ>0{7)C$Y`5H1C}?6!GpwSf4Ib(W*p@dIz?vgH
z-+K)kczfi}kcpGr<@ZF-;B`95`O)+9#1+IJ@vq*S4GCC1lZ*N}S4ic6!)@5-lU(HJ
z%fC$Xb_-eWv2;r8|M}23Y3Y_iBgNW)6CiC(?>JN}B`}9(5LX?&_Uu8Al}H68w7Hw3
z7Pl>jG^u^lIhdbvdh>Ie@CN_7rig`Yg`wzPaM9M0GFF_ksZ;=+zb$+FS?kDXF*6Ro
zRpw9e{>|R3O^N9j6_=dgsAF9%hq%_a_WUP43H{>M8YY@`bd#A82|0y^6tup9SHSO^
zlO%6kO2mB`G|=>D+g`!KLzP6!u3OoV7kF>o_Kz&I;uLOuT^L~zCr$+>a8e%!2u)C^
zwI<1Y6jtU4>{i(_ManRi8xh&m`+}Ay8!z+(s8PS`6d#H`22}}D{)(3Hk<=<s^vTN7
zjvIKHSzK9Ec@E8#dwlUgh*<4{n^R$O_d+MiFo@*k<161}H2?mxLy}ls0%O95TBL)X
z^s^=XfJ`{?1`WBE<xjj={jAsCbQube3|#e&VutpUDG3@Jf`_8=mn43Sp<9e?eJrWS
zX#D*I^A#4cA~0~+oLaE&>O)TsFOA#AsvvfKW9<v0$)5!;W}cCi#8H&)<qoY_2$vem
ztRIqHASW7C`Jz)(C8d;S2q>2f4KmW=>-e9Z?~uQZ$)&p20L(CZHO`8DbUZNk=GLm%
z+~ZW&a3(ASq%l5xkcJit1Pg#5a8@uJApi$~S)m}H02B&ubjqou#*<c)Q`3-5Wo&T7
zh9Xg^!EMy3<IP00a0rSO0Y_ryML<><5Q6#qcXk9!ebWHC1A{{UA%{X>n0Jg7MvmKv
zz=nYksXfht7<<<L<;B#<-GuX=?VtW0Xv=A-g1|tapq#6Vr<9bdw-Jz)9}I-DB2bVF
z^+14H>iH^VMqMC)lu=GlUQkI;Sx`+-Lr`1LT+l+$($(47T+mw3He)Ujz)EHBE$Aue
zY3FWjE$I2wRq%<Rm!MAuDH;%gMgWmwV*fP*^Uf*N_wm&J_*%@K)o-|BWW>4NJ7HT^
z01Nzzidq&R`JBHgPO1=l{GNSwiQ;^d>SUa4`N(vc_B^|4q-P2LELi6`j$o*kL<z5K
zt#3dSfmrS9+}f#Te_{TH{eVB6tusbkf7rRUzAYdAdVO$tQ~|n8g-(3u=d>O(+k8U%
zA)EI1u?jcmeQ0`OTUg<b!t;7Nth=goQ^4;>Aqt&4giNrDrF9*g#IvoPVRriG?gs8Z
zrW`pGhvwGGEjj2r2L7ze#}wJsv-^d6ma616I-GqKt$H%V_+x)L^I6`}<TsxaTE0$o
z&D~1UX*mbH=IEafsO8ZE+S!!`(^?Mj=D2yeky1U4lgg(Ry3?`K3=aIw2{A>STIw3f
zX-PltJc+kZIHxM0(urzKM9|&a8e1&}P1AkP{6ptR$wzY<th+*&LzsP680j+EHnsjK
zPB4c8vU(^3thZWQDG^P*Nd5TcM6aft^A}5xzoJ2CA)O$(Hmw_aO*YWcu2R96I7GGV
zjJ}q-ggd^ziOv?sT7s|n3D_I9eQ<uU^+wleR>C9vQT}X><W|BWt(A>I2VKprigf28
z#}wv8)8|1gg`cZ_344bBl+qTvWc8gq=)CK}ohuF<8{@qn`pNA?BJB`3N;(jeH#6!3
zaFZG&e7$;(WKcgxA0e*j_?fybX;z~bsSLemt*lf*i|aYk{p}j(U!VR4KE6eSZ=7dn
zq^d&u^}~y??ODr(D0p%Fx36EA=XQ9iteOZo{53sCv?3Or=-B}k9leBOx`)4g@|LO8
zS{R^+?59`C4Y-m8lHpGGLhLDp6@7Rmus4tvz!hFELzBS-v{MbUBuxdW5bS+u!@P*A
zbm^ysS7WW>Vmv+>De#>*L%m@OF-2q%tMQ{N^YgwwZPyi~_@D7{#`|u>cCMg3*h^ol
zM-if|pwDSa<*`Tg1qHV%=R|N?ZRh>yjE_l?Zu8J=%?r0?W89?=X=3Vi-RU7^?)q%;
zg)7kZelKTNv|^L9r&DO4B+at~4#lr!nnJF2rS}{5fO;412{MGP>!agR$t40Go5_2u
zW7!+&n76;sSngr>j|4d)l-6vmmbb@B`N<kh5(`F)K0y|ZAMwp}h@^`Ssv6;{#dZyv
zJLxphG_!d-zdZRp$IJ!y$wZPPmcm@R6UC2ML_NfQp*eDO56Z&dw8b#1;fVvj*_0Qu
zs#hV#Qv<iOwYg=JsF2X&=TDElwwoER#^c9iHs<!CsR@K)n91-20fRk4$#=YPCnSXi
zar+AxK0XvB@M@;_g1Ft<n{Zy>rmdbL*|B3We9XJLJAE=A=t=+i`ycS*SLM4ZpWhLP
z2iLmmFr(j5G49#mhgicSV|zBb&Aql`;}}AtpM8Vck(Q`yx8#|AI>HMv7CGZPgSXoF
zo_Ty)w)sut=kZ7N6xFWxbh}r2oMKw-C}rgn@BO>RX_rUZuen!g&tHwdw9}>G%2Im}
zbXaX<oN#NS@q+vAs5m9sqhRx3Ynufn;ZV&`X)cAHsNS`J{R)7Rt=LO=LkCs+9DBA&
z9EKJam}3Sfc;YC@;y#$;o_E_Cjy)E>rPNxcYYYD-r2CjESH@PjO3i>)#<I-GNrSMT
z(nwJH?e^1d)u}jYvZ!H6zea1}K4<K=t*Ou6BxsE<Y3&gz^B)%(D*W~q@ZZkltP<gZ
zA_l9`g#5(n{`ghAH3}y#(fhuycP~O4ofxv)DRu7~rH_0LsJmS1$^XTL&CGS1#Qmh7
zwR>ixkT0!H5J<zjW_^Tmiy4{Vd?D#LL6`Fk+^FosF4QRAXy!ij4Jw>WJRj6|mwl^`
z6_tHvwya51hgC;Pjl*`izdmOsOPKCGFrIxMeMC4uVXkBmQ4UD69g%&-zNm|WnEHqp
z)*GoU%u-rOzZ^Os2TNHOFA63PrrQfH&-y-je0aJ%ytDSWTNl_w>IpUU+et1aShfrJ
z`pB*w(Xhq46mZlot~7h*Xcxyl{&9Ct_Hdo;!1;cGZ-SA)YMw<?f#=3ZP2)DQeb(>^
zn#d4W>U%=Uk6-wfViL~yPLV5H$IcQ?DhjGoXVV=oT);G$fI(+|d6)C`ST0k8Uk=B+
zYxA8F-P%U_bv4f>k;!*rY_QFjk8`UtxLoajZ+Fy@FY}c@h<z~ko-(8+s?aU1*<JzI
zOBzO}Kximw6w6~U#vm7ckEbt5^P!zA1G-lwn3bFTLy061HWirE6AP#!^IqI9D|;lZ
zoocc^iE8q`r%$yv*>*xe06A;qJ<f#N;XTkaeLQ@tl?WkYr1W7`=owW86>Ua_{Miqd
zi-OiI1y{2%+tvNIv68wHT>3m7Fb28e=P<`jVstJ97fndk`cS+qSF(ru5n<PdBec0~
zrd+*k&@xrR)xA`*KUn?)8+qNyKf?B#8tsT!o}K~n;#Q?p+#c^T*oVZKA2rvv`DRi-
zZ(+RC&tp)jh>Er&S0YmoKHZRY(IGvmzNPz;x&kZE{bJC7>GldI|77ufJ@rJ3jD-zS
zQZcLpo-YcOv3ofSsB*vB7lWEXr{icGmAO~;hT-nz-qL*UC9|}2d74rNs~#lZ{W;C@
zN<^Q3!54Zm-le8uW>)|T7yZ6fRlEFBjlRd5d3UVUhAmvKRKJXW#Q#Bn{aWizYwGJp
zWW2cyqRA+LjUtwg1adV#`<NKJ@FI9Zz$^4ovFr#5eoqYlPm>bDO39aw9y{e|YaE!h
ziUPR^Dt(goqSW@X{JXev8*jVM*3fg72Ye3%o&XC^R@U6~$<5#BfVNSlO)>PQq-}-c
z!Ha9aj=NXdnem%`K0Si<KScf@as+!nhk!d?eCsL8Z*yA=%RsW=)3TTx?wOXU8P(Ov
zzmz#dwNLJL*zohT++%EF{PtD~ZD|vnH@ftSjh~F8_?MWy_8Mr)=ajH%CZ-mBcrtQ;
zg*IRj@cP*HGAMwen>JKWN<*esZ7G3riFv4jv<a52#bVLCnH+^1vJ+DBjWR^z8E}!A
zmL^9&GsIfL8(W=stw>#zk*%{@r{R6(++yPWMI46ri}9zlAx3X@UTvLaqf@?6+ALol
zP!F&ng?fxb$lv9*Z@kmXH@bZ>w4thcZfurzi16o!YWEX?ckg_b`M6}<bP+y%tb>MY
zTeL9Veno;8OGt#~)!8m>;L<d-b_XVI|F{enP929M$>sODo?wepcSdq~q&k=uE>nC{
zda-Nn)cw^>ue~b7hZNVD2E9$`A1=0A-G=-5Rx>T0j^xSUIR!WBS9$d>bK#(GHKP@u
z?vd)~+woQpzpu6z27crb(Q2aI`;b~DJqpedbWf(mnKyjEyZ3R17e|m#O!g13JwrnD
zAy~EZcP=eMorC?VE7#G>3M?j%rK_(}k4ENAWMj>iS$Bo0_0*TXbeN-e!FSXz6j#}D
zS8}-;mQW7nhS+a&|5%t)hF(bIm@JNly$wb3QCnvnZ*b#p>L?o;I$#6Vs{MUbcbX1c
z=00Ru%5fRqX3AQYahe-~oPVV+lE_4Bd0Gu~7>I}bxmxASL$>W*%6=z#=emA>?miQt
z$;$iyME}4zATrdny=@$wCd=OLDRb%(bO>}rWY9%_t8Cd+jF#UW_U<sZ{BZiJ&dqWO
z+48L_>}XrmCh<tg<<!<EV{#m_z1Q~i8DoJO5PL+VwmY%j+KK1LkvgcEQ8|vl!2tV+
z?RmG|$M&i$L6j29<gH445{t2lY+|+sye2rsuFxWuR)Y$qp}<@8WfWp0X|Dab@GaQs
zwD&IIi&p3TrKOg+LJyjxvPvpWSmm6b<V)tE>a!f>J>?zcU5JpXT4-p~#p0?q;x##B
z-Mu$1J<DG)MyJ;5N9n=HY(AbeY9;Y4$%y8mg8I30VlS)C>=k!hQ-Kcavvj6M5jbCN
z|6YXr+3fg(p1J&kb{a8~tGOs-P8XgKYT`6#W@*3*_|v}9VaIQH7HIm7EwR>)<kvv#
z6jrBn=qz&ZUE(?bY`0xYDo<i;@3dVZ5@e{EQO4Ql1Y?7QXr(Lho^WFW>dIgJ`8@M|
zaShj)>5K`{oV*abeDUs+zUu{@youW_+?CJ`I`=zkpS~GAN6Q=K)4b|Qw^8|A$Q)w!
z1n$CQNaz7DbToK<k4L{4%Bw;7{&2_$lJLymNdzG8IKn^FBU&;$?C;;%Bxm*UzWZ~;
zdjvaYmI_|4>^N3TJY1Qu9y^%qsk6z`k04JfFMC0!Aq{I=<*WA*Ux{oD=zjtA55`kX
zrJV8W)+cw(SI}FeU94*sx_srbjjU%ncUnmW%ZG81EoF4o6JzGYFx|MPZpuSU^r|(W
zh&v=>B(5B#Ru52-0<&Z3OigDq&6kG4SGfdhl|lk;WG6HduFq*~UG(-;hi2moB)e6)
zJyvO-h>NhJEU@!f6{9aN#KZQZ`&WQp-G9vVnu{wafzj+6l`krSx>u)O;tpDVBygcl
z{l)5ui{vYvzmh6_9i&F#I^lc~3VER~wH3u4?sAMTZJK;$yzB-ZT)rFNb97o-S7Y#&
z&krX5jBO-YE!mnrCPt;=5fRuheh^1GtpFg%@_?3Vk9#gJh+V-cnZoa?YUTWhTwG}G
z>BUv<?lxLKiY=e32<EZsIHvgCos4c9u5J=w68NHjG${aYhyReAj#QOQhNV3bfj$wq
z9dGs<;;E~%>>+e`JH*y6#mp?f%R4?r^Q*O2Iv@+DU8>|GioZ0@NF#wasxqW^LA<5w
zYQ_QfF2CM4V2aD{xt3(?o0d`oz3iS$9D_|`)O&QqnAk%!zV_Lhx0Y{=u0}+-=0shZ
zb5SRIsjc}t2FIH<pHDVi3{sQ5h!{GTB7D=;oxp4}{VEJ|K|>@z4;su3*sSJ#R?!?&
zQ%G5M5cL;U6x9z~AM5z|Kr>4TUBR;OTpQw5t^F=>Wz|<oG75EOn?pn`(?1y*sGdAu
zy&U8S`M{S`av1(h&(h6JSE761-edG)<ob@A|5*xQqUJOj`xosBYwKJ*00|;QLIt2G
zAOZ=^V0Z)ICxF2OASe_Fn4$Itz()Xu2tW}qFft?L4FF6C1!8o;U<fLs>kUAV5DphW
zfguneD&zYb0E`ff!u$vYp`fjhZU7p<4mZbqF^2;AEszikeh|poiXVu%_#qZRkhujE
z2?yGsGG=-JuLS=unp~{j&Q2~KLf+1gGu(OrG#RA*0D_FgUH}~_m>&$+0l|boP$4KJ
z1JDN$xF!<m1H}B_mh-g_AkX=KT8>~wVh@1r|8&>ZyncWp79ki62f;v4%n}dZ0_gwk
zE9E;tBpQmqj5GdTtS+oXf8RkMI2Z-~PZ<ybgMe?yFloUIN&a5{V+%q+FvF66mtkz7
zV8{&_{O_N0fI#&B7-JL>K+J^YnlTc1%?U;ig&CY&(}RORn0d{A+QNarYrz2_a5xe(
z<@uK$#y=1v1S1gtCj6%i^1sNS|6%-3Js9f7qTxu$HMBq&SYg)}h_TP083ItDAvZ#V
zqc8)hzxV$awm>Kxb^~u94ElFa^`Ckewd*nz0uK52u>TrBVW9u=f&L#SC^+aw*iZ-x
zcHI~WL189q*BnD&$m>ubkVwS!u%Tese-_=}B)}nX)O9DAo`+pW0gfrp>rVcfUXK`p
z0D*242?Bg02M`1piM}2Q1mpR-F%W`;UDpGm5Re<ufe^6k#RLb!P}lDV1wldo)fO3Q
z!vG>Q5`;<iHAF#R82p+HhJf8H4G{3g+F)?#O+bMdD!6_>5DfNr9e<PX-+c^({%x{r
zikQLYO<q7ikk=QD`Lo@P(ttoA$m@Y%z=Qo;*8b6nKoF*QuRDfdBEF711OZ3flp$~M
z2Nc6+*RugdKyGpc0*$)KTu30|I$RJW_y&X!Bm{O-4|<aqFcoxtF%T%GIQ}AyiT_{l
zV^DxzhZPLO5c#!~U_gc5xFHg818OLSkp2zozeNVZga-e2+kfDXVUz2H3Iakv(CeKE
zL8AVb#oVL`2o&*mT>kg^S8$j>ZY&xM1)^_2jX~ym?m!p`;(8}R{vIQ)Il<7=%^YJg
zat#H{Qh=y`qWW(n2u6WWH+C${k>h$wASej@rXCD<qcBnM>&y*=px}uAu>Ffa1hY?H
zH^ywnH;D{W*4JUhZ16V<6Nv!-eWvjr@Iz3TM-JCyP|WU*zAi*SU^jD&Lfzm6%(3kT
zFJKODH>w|s!r*$%F${$I@9iD^uL8l;<qhV7A#V0I42g;P+701A<n;o^a31PL+rgpW
zYs7`YA46vF>#!nF;J=T5{sTfJ=Dc}5O-KX+`S0!Y*8r1t_;o!D`qvy|S`iF{1JVEK
z1k-jf;I-UgSRQeGC&u(K>Ux)8=o@uo4}yY0H}*6r<`DhgK4AZK{==LLfHx`~iok5e
z*A@tZ!r|bI*$IHC8A28em65@mtU*weEEFP*p?jc=G)NkXl$4W`g@VLH{=XU~L}Fq@
a9-ijzp5E@(Hbnn8E<uPmIAqo3i2fgr1X+&&
diff --git a/src/plugins/e-acsl/doc/memory_model/article.tex b/src/plugins/e-acsl/doc/memory_model/article.tex
index d6014bcecae..4c206402d7a 100644
--- a/src/plugins/e-acsl/doc/memory_model/article.tex
+++ b/src/plugins/e-acsl/doc/memory_model/article.tex
@@ -720,7 +720,7 @@ least one test case provoking a runtime error and this error has been found by
\hline
$Bsearch$ & 28 & 63s & 20 & 41 & 41 \\
\hline
- $Bsort$ & 37 & 273s & 153 & 45 & 47 \\
+ $Bsort$ & 37 & 273s & 153 & 47 & 45 \\
\hline
$Merge$ & 55 & 100s & 19 & 58 & 58 \\
\hline
@@ -728,6 +728,8 @@ least one test case provoking a runtime error and this error has been found by
\hline
$MultiplyMatrix$ & 44 & 146s & 9 & 44 & 44 \\
\hline
+ $get\_sub$ & 165 & 993s & 364 & 53 & 50 \\
+ \hline
\end{tabular}
\caption{Experimental results}
\label{fig:exp}
diff --git a/src/plugins/e-acsl/doc/memory_model/experiments/get_sub/Replace.c b/src/plugins/e-acsl/doc/memory_model/experiments/get_sub/Replace.c
index d8eadf8c6d5..df8c2cc629b 100644
--- a/src/plugins/e-acsl/doc/memory_model/experiments/get_sub/Replace.c
+++ b/src/plugins/e-acsl/doc/memory_model/experiments/get_sub/Replace.c
@@ -2,14 +2,16 @@
-# include <stdio.h>
-#include <stdlib.h>
+#include "stdio.h"
+#include "stdlib.h"
+
+/*
#include <ctype.h>
typedef char bool;
# define false 0
# define true 1
-/*# define NULL 0*/
+# define NULL 0
# define MAXSTR 100
# define MAXPAT MAXSTR
@@ -35,7 +37,7 @@ typedef char bool;
typedef char character;
typedef char string[MAXSTR];
-
+*/
@@ -43,30 +45,34 @@ typedef char string[MAXSTR];
@ behavior b1:
@ assumes *j >= maxset;
@ assigns \nothing;
- @ ensures \result == false;
+ @ ensures \result == 0;
@ behavior b2:
@ assumes *j < maxset;
- @ requires \valid(outset+(0..maxset-1));
@ requires \valid(j);
+ @ requires \valid(outset+(*j));
@ assigns *j, outset[*j];
- @ ensures j == \old(j)+1;
- @ ensures outset[*j] == c;
- @ ensures \result == true;
+ @ ensures *j == \old(*j)+1;
+ @ ensures outset[*j-1] == c;
+ @ ensures \result == 1;
@ complete behaviors;
@ disjoint behaviors;
@*/
int addstr(char c, char *outset, int *j, int maxset){
- bool result;
+ char result;
/* b1 */
if (*j >= maxset){
- result = false;
+ //@ assert *j >= maxset;
+ result = 0;
}
/* b2 */
else {
- outset[*j] = c;
+ //@ assert *j < maxset;
+ outset[*j] = c;
+ //@ ghost int tmp = *j;
*j = *j + 1;
- result = true;
+ //@ assert *j == tmp + 1;
+ result = 1;
}
return result;
}
@@ -75,35 +81,38 @@ int addstr(char c, char *outset, int *j, int maxset){
/*@ requires \valid_read(i);
@ requires \valid_read(s+(*i));
@ behavior b1:
- @ assumes s[*i] != ESCAPE;
+ @ assumes s[*i] != '@';
@ assigns \nothing;
@ ensures \result == s[*i];
@ behavior b2:
- @ assumes s[*i] == ESCAPE;
- @ assumes s[*i+1] == ENDSTR;
+ @ assumes s[*i] == '@';
+ @ assumes s[*i+1] == '\0';
@ requires \valid_read(s+(*i+1));
@ assigns \nothing;
- @ ensures \result == ESCAPE;
+ @ ensures \result == '@';
@ behavior b3:
- @ assumes s[*i] == ESCAPE;
+ @ assumes s[*i] == '@';
@ assumes s[*i+1] == 'n';
@ requires \valid_read(s+(*i+1));
@ assigns *i;
- @ ensures \result == NEWLINE;
+ @ ensures *i == \old(*i)+1;
+ @ ensures \result == 10;
@ behavior b4:
- @ assumes s[*i] == ESCAPE;
+ @ assumes s[*i] == '@';
@ assumes s[*i+1] == 't';
@ requires \valid_read(s+(*i+1));
@ assigns *i;
- @ ensures \result == TAB;
+ @ ensures *i == \old(*i)+1;
+ @ ensures \result == 9;
@ behavior b5:
- @ assumes s[*i] == ESCAPE;
- @ assumes s[*i+1] != ENDSTR;
+ @ assumes s[*i] == '@';
+ @ assumes s[*i+1] != '\0';
@ assumes s[*i+1] != 'n';
@ assumes s[*i+1] != 't';
@ requires \valid_read(s+(*i+1));
@ assigns *i;
- @ ensures \result == s[*i+1];
+ @ ensures *i == \old(*i)+1;
+ @ ensures \result == s[*i];
@ complete behaviors;
@ disjoint behaviors;
@*/
@@ -111,27 +120,37 @@ char esc(char *s, int *i){
char result;
/* b1 */
- if (s[*i] != ESCAPE){
+ if (s[*i] != '@'){
+ //@ assert s[*i] != '@';
result = s[*i];
}
else{
+ //@ assert s[*i] == '@';
/* b2 */
- if(s[*i + 1] == ENDSTR){
- result = ESCAPE;
+ if(s[*i + 1] == '\0'){
+ //@ assert s[*i+1] == '\0';
+ result = '@';
}
else{
+ //@ assert s[*i+1] != '\0';
+ //@ ghost int tmp = *i;
*i = *i + 1;
+ //@ assert *i == tmp + 1;
/* b3 */
if(s[*i] == 'n'){
- result = NEWLINE;
+ //@ assert s[*i] == 'n';
+ result = 10;
}
else{
+ //@ assert s[*i] != 'n';
/* b4 */
if(s[*i] == 't'){
- result = TAB;
+ //@ assert s[*i] == 't';
+ result = 9;
}
/* b5 */
else{
+ //@ assert s[*i] != 't';
result = s[*i];
}
}
@@ -141,57 +160,49 @@ char esc(char *s, int *i){
}
-/*@ requires \exists int i;
- 0 < i && arg[i] == ENDSTR && \valid_read(arg+(0..i-1));
- @ requires \exists int i;
- 0 < i && sub[i] == ENDSTR && \valid(sub+(0..i-1));
- @ behavior b2:
- @ assumes \exists int i;
- 0 < i && sub[i] == ENDSTR && \valid(sub+(0..i-1)) && i >= MAXPAT;
- @ ensures \result == 0;
- @ behavior b3:
- @ assumes \exists int i;
- 0 < i && sub[i] == ENDSTR && \valid(sub+(0..i-1)) && i < MAXPAT;
- @ ensures \result >= 0;
- @ complete behaviors;
- @ disjoint behaviors;
- @*/
-int makesub(char* arg, int from, character delim, char* sub){
+int makesub(char* arg, int from, char delim, char* sub){
int result;
int i, j;
- bool junk;
- character escjunk;
+ char junk;
+ char escjunk;
j = 0;
i = from;
- while ((arg[i] != delim) && (arg[i] != ENDSTR)) {
+ while ((arg[i] != delim) && (arg[i] != '\0')) {
//@ assert arg[i] != delim;
- //@ assert arg[i] != ENDSTR;
+ //@ assert arg[i] != '\0';
if ((arg[i] == (unsigned)('&'))){
- junk = addstr(DITTO, sub, &j, MAXPAT);
+ //@ assert arg[i] == '&';
+ junk = addstr(-1, sub, &j, 100);
}
else {
+ //@ assert arg[i] != '&';
escjunk = esc(arg, &i);
- junk = addstr(escjunk, sub, &j, MAXPAT);
+ junk = addstr(escjunk, sub, &j, 100);
}
+ //@ ghost int tmp = i;
i = i + 1;
+ //@ assert i == tmp + 1;
}
- //@ assert arg[i] == delim || arg[i] == ENDSTR;
+ //@ assert arg[i] == delim || arg[i] == '\0';
/* b1 */
if (arg[i] != delim){
+ //@ assert arg[i] != delim;
// unreachable
result = 0;
}else {
//@ assert arg[i] == delim;
- junk = addstr(ENDSTR, &(*sub), &j, MAXPAT);
+ junk = addstr('\0', &(*sub), &j, 100);
/* b2 */
if (!junk){
+ //@ assert !junk;
result = 0;
}
/* b3 */
else{
+ //@ assert junk;
result = i;
}
}
@@ -199,17 +210,46 @@ int makesub(char* arg, int from, character delim, char* sub){
}
-/*@ requires \exists int i; 0 < i && arg[i] == ENDSTR && \valid(arg+(0..i-1));
- @ requires \exists int i; 0 < i && sub[i] == ENDSTR && \valid(sub+(0..i-1));
- @*/
-bool getsub(char* arg, char* sub){
+char getsub(char* arg, char* sub){
int makeres;
- makeres = makesub(arg, 0, ENDSTR, sub);
+ makeres = makesub(arg, 0, '\0', sub);
+ //@ ghost char* tmp_arg = arg;
+ //@ ghost char* tmp_sub = sub;
+ //@ ghost int verdict = 1;
+ /*@ ghost while (*tmp_arg != 0) {
+ if(*tmp_arg == '&') {
+ if(*tmp_sub != -1){verdict=0;break;}
+ tmp_arg++; tmp_sub++;
+ }
+ else if(*tmp_arg == '@' && *(tmp_arg+1) == '\0') {
+ if(*tmp_sub != '@') {verdict=0;break;}
+ tmp_arg++; tmp_sub++;
+ }
+ else if(*tmp_arg == '@' && *(tmp_arg+1) == 'n') {
+ if(*tmp_sub != 10) {verdict=0;break;}
+ tmp_arg += 2; tmp_sub++;
+ }
+ else if(*tmp_arg == '@' && *(tmp_arg+1) == 't') {
+ if(*tmp_sub != 9) {verdict=0;break;}
+ tmp_arg += 2; tmp_sub++;
+ }
+ else if(*tmp_arg == '@') {
+ if(*tmp_sub != *(tmp_arg+1)) {verdict=0;break;}
+ tmp_arg += 2; tmp_sub++;
+ }
+ else {
+ if(*tmp_sub != *tmp_arg) {verdict=0;break;}
+ tmp_arg++; tmp_sub++;
+ }
+ } */
+
+ //@ assert verdict == 1;
if(makeres > 0){
+ //@ assert makeres > 0;
return(1);
}
else{
+ //@ assert makeres <= 0;
return(0);
}
}
-
diff --git a/src/plugins/e-acsl/doc/memory_model/experiments/get_sub/oracle_getsub.c b/src/plugins/e-acsl/doc/memory_model/experiments/get_sub/oracle_getsub.c
new file mode 100644
index 00000000000..5874b006dad
--- /dev/null
+++ b/src/plugins/e-acsl/doc/memory_model/experiments/get_sub/oracle_getsub.c
@@ -0,0 +1,36 @@
+
+#include "string.h"
+
+void oracle_getsub(char* Pre_arg, char* arg, char* Pre_sub, char* sub, int r) {
+ char* tmp_arg = Pre_arg;
+ char* tmp_sub = sub;
+ while(*tmp_arg != 0) {
+ if(*tmp_arg == '&') {
+ if(*tmp_sub != -1) {pathcrawler_verdict_failure();return;}
+ tmp_arg++; tmp_sub++;
+ }
+ else if(*tmp_arg == '@' && *(tmp_arg+1) == '\0') {
+ if(*tmp_sub != '@') {pathcrawler_verdict_failure();return;}
+ tmp_arg++; tmp_sub++;
+ }
+ else if(*tmp_arg == '@' && *(tmp_arg+1) == 'n') {
+ if(*tmp_sub != 10) {pathcrawler_verdict_failure();return;}
+ tmp_arg += 2; tmp_sub++;
+ }
+ else if(*tmp_arg == '@' && *(tmp_arg+1) == 't') {
+ if(*tmp_sub != 9) {pathcrawler_verdict_failure();return;}
+ tmp_arg += 2; tmp_sub++;
+ }
+ else if(*tmp_arg == '@') {
+ if(*tmp_sub != *(tmp_arg+1)) {pathcrawler_verdict_failure();return;}
+ tmp_arg += 2; tmp_sub++;
+ }
+ else {
+ if(*tmp_sub != *tmp_arg) {pathcrawler_verdict_failure();return;}
+ tmp_arg++; tmp_sub++;
+ }
+ }
+
+ pathcrawler_verdict_success();
+ return;
+}
diff --git a/src/plugins/e-acsl/doc/memory_model/experiments/get_sub/test_parameters_getsub.pl b/src/plugins/e-acsl/doc/memory_model/experiments/get_sub/test_parameters_getsub.pl
index 52766e82aeb..a1e94895895 100644
--- a/src/plugins/e-acsl/doc/memory_model/experiments/get_sub/test_parameters_getsub.pl
+++ b/src/plugins/e-acsl/doc/memory_model/experiments/get_sub/test_parameters_getsub.pl
@@ -17,15 +17,15 @@ dom('getsub',cont('sub__getsub',_),[],int([-128..127])).
% dom('yourFunName',cont('yourArray',_),[],int([min..max])).
create_input_vals('getsub',Ins):-
- create_input_val(dim('sub__getsub'),int([5..5]),Ins),
- create_input_val(dim('arg__getsub'),int([7..7]),Ins),
+ create_input_val(dim('sub__getsub'),int([6..6]),Ins),
+ create_input_val(dim('arg__getsub'),int([6..6]),Ins),
true.
% add new variable domain e.g.:
% create_input_val(yourVarName,int([min..max]),Ins),
-unquantif_preconds('getsub',[cond(egal,cont('sub__getsub',4),0,pre),
- cond(egal,cont('arg__getsub',6),0,pre)]).
+unquantif_preconds('getsub',[cond(egal,cont('sub__getsub',5),0,pre),
+ cond(egal,cont('arg__getsub',5),0,pre)]).
quantif_preconds('getsub',[]).
--
GitLab