From dd6cf3a5c5bd3c4501d4fa9363c5670a2ab7c213 Mon Sep 17 00:00:00 2001
From: Guillaume Petiot <guillaume.petiot@cea.fr>
Date: Fri, 22 Feb 2013 12:12:42 +0000
Subject: [PATCH] [e-acsl] article in progress
---
.../e-acsl/doc/memory_model/article.pdf | Bin 111672 -> 111682 bytes
.../e-acsl/doc/memory_model/article.tex | 10 +--
.../experiments/Bsearch/bsearch.c | 65 +++++++++++++++
.../Bsearch/test_parameters_Bsearch.pl | 29 +++++++
.../memory_model/experiments/Bsort/bsort.c | 50 ++++++++++++
.../Bsort/test_parameters_bsort.pl | 24 ++++++
.../experiments/BubbleSort/bubblesort.c | 44 ++++++++++
.../experiments/BubbleSort/test_parameters.pl | 21 +++++
.../memory_model/experiments/Merge/merge.c | 63 ++++++++++++++
.../Merge/test_parameters_Merge.pl | 77 ++++++++++++++++++
.../memory_model/experiments/fibonacci/fibo.c | 23 ++++++
.../fibonacci/test_parameters_fibo.pl | 19 +++++
12 files changed, 418 insertions(+), 7 deletions(-)
create mode 100644 src/plugins/e-acsl/doc/memory_model/experiments/Bsearch/bsearch.c
create mode 100644 src/plugins/e-acsl/doc/memory_model/experiments/Bsearch/test_parameters_Bsearch.pl
create mode 100644 src/plugins/e-acsl/doc/memory_model/experiments/Bsort/bsort.c
create mode 100644 src/plugins/e-acsl/doc/memory_model/experiments/Bsort/test_parameters_bsort.pl
create mode 100644 src/plugins/e-acsl/doc/memory_model/experiments/BubbleSort/bubblesort.c
create mode 100644 src/plugins/e-acsl/doc/memory_model/experiments/BubbleSort/test_parameters.pl
create mode 100644 src/plugins/e-acsl/doc/memory_model/experiments/Merge/merge.c
create mode 100644 src/plugins/e-acsl/doc/memory_model/experiments/Merge/test_parameters_Merge.pl
create mode 100644 src/plugins/e-acsl/doc/memory_model/experiments/fibonacci/fibo.c
create mode 100644 src/plugins/e-acsl/doc/memory_model/experiments/fibonacci/test_parameters_fibo.pl
diff --git a/src/plugins/e-acsl/doc/memory_model/article.pdf b/src/plugins/e-acsl/doc/memory_model/article.pdf
index 720206c4d5bcd748d1d07a4975dd6fe038e610aa..b00f251e110513423e61ce008e590bc54554c3cb 100644
GIT binary patch
delta 6887
zcma)8c|28X+ioL-LZ%{Rh|KmH_S$=kWS%1=GL*5*84{_sD3l>(o}xA~&mlCBS!5m?
zk%&S{WvF*`zH`odTKoO|zO(+Z*W-Df`?|0Dy6$_`%rG|2Fvf(?tLdM;5h_VJW{W7W
zWu}j(JtB2xypQtpJI#;0ENIv{lJ+X?LiL7SSmhCBVfO{Uz{QXy=fEiW25J2GySfLx
zPIyhv;~!VP@t!wMu$eq5yt<>RI=~CeJ9pvPGtJS`2W`g{1YWGzUc8X0<tT!mb8eO`
z8&HEi)`E}LOesFD3H|=6pMOX2Fl9Wo5e~XOE})~Wy(m{g-2GlmW`7@(l5WVIIf-ny
z5v1{M=A8s7j$^BD);%3qs~cYIeFu+<Gz&|O%x{(Ji$UHEp9(2CyMC43c8zgQ)Jk{E
z!M0AaQK?e#0h=D`r68;3lSG+=1Bdrl?Ph>iR#F91kQ_S^$JoBHDfi$@;eiLZ=07?$
z+HH0}$xd%>Ah2nFQk;<I>jLY65aY3-DfyFmA2;t4E*uHAQkhl_a0e}uj)u1yF4OVl
zZ+5vjuuP4e#Ys?_BHJ^Onv>~ON7o|{2GcFp*DmVad}ZTG4AM<iI+tr_%JGD<aA&7m
z<YNT-Hs83iFElkmJ8Gw8{Nw0urr!N^7Yv^9*6Wm=qtvO@Y28)q2)ScH?P*Y^wr0k8
zx#_txsmpkzFInh+m#Huu%KX}E6RUNb;VhVZ7+?tIzr90=(h^l4qH*$KU5K_#{0?o$
zqRho><~1tKdo4^|Ef_yPdx}#k>@fto7l!h<{MdFLDJib+QZV44S9{6OX6xM7r!e{?
ztM10->n+r}>k&HHS=wy$smqTt(v=H*la;lMB9B)b&i+!)(4iLR_9}c(?+mL+pdiZ@
z!Sowu+by|LbB|C|SAwSAj`Lagr^D0X>$zI$<tvxtCLpu$p-t44^V%9|>&QZ5K<d<r
z)(1{Dz77HLw?&GM`=F$kco7Tsd52t1wuTvp%a={h>o0K3UTf@MDcP&8t-kITRyGn?
zqSwRT!t+>Qb4TnU{Mk$`>5ho`aR4_>CB9XbI+0s9*7b~X^N<eLj@;m`JcfQrez_+H
zzjFsm?th$C6q<EY&bHnBq^9F~NJV9TnZI(9gJdG-(MX$Z>)Ow4ndJjmxL80{%E8WU
zEH9Q+W$tfxn5x+OGi7V8v*ARUO+%Blm*eE)P*OR&mwv{TcLp};a0H#?32R$slT&gf
z!3Df~Jjjm8uPG6#kW%}`t?-(Lyn&CmMuc(-1Yhx52%45;mwx&lJR(}#pR1zo`Sr=W
zfUANV<0p9D%ylVq=M~CzTt4LzY!T9ut;!CheTjLi`Ew)q0+ZghOg3%li6knJv0ato
zkZrL5DjHO7Y3pUSXN01wg6;{`g{;rpC_WN3BFhMsawt-svq;HD2z8jgiq1t85}8F)
zm4>3alZ_|ObF8c|&av|Gt~8Bt@*E4981dowe!#v{+-x@|acii})UZuS#peZfVUaK%
zyXLo1k2}<IilP>nKXrDKWx&#o`1<Q%b0XZD8z})|Uz^@#`~OtrsxDe96^c0*xW~F*
zQ6w%0v2T7v*&-$Vqw7?MSvf!TYyyKVM=r++221t&a?#+5i@;``r%r4MS0YthSsBHK
z<P@B8>C<nw?b*TbITy(C6}fFX=R9!fidXBd%<R3NHdI_9D%qV+CtdeWI(S%oZIR{v
z)k(DkqFq}p@4{RDtMO{|9QL_sMH}xQrM-z0BXxc?&f7}4b#nErAby*hS(I7RvAU}}
zOwag#%1CLo*6LN>QXXa>D=waGEVJYh4(O=q-Y?l<%2~EyZz15Kl|((O^ZbzbM|Jnh
z1X1-zPA?ILw;gh&$KeSt!uP;ypG-0nc<VcLmpBfI@gK7jG*!rp1)0PL#^f9GncBl2
zFUVF$cFpOOP##pCAGE001WON}c_C&g;;)vFw6`YrYR{U(;X0-pM<5NheIq})Bcux-
zsRzg3F-lrWa!b|zOx3;+Ha0V&pyE6s@z5w;GxS_@$H1u{=5^dI9F`Le{HN^eqMRQ~
zRmr-F*B8eb52Yydu?n%*U1<F5dPBr7E=W)e?>-UTn6Zh{By;5I@D9C#VburEDxMF?
zZU-0oay)!5%q+$+T3!v?dEjUh0<NS69fY>I+DDl3_N|Ta+U>bnI}jT8t-Z`j+&VPA
z$(VIx%RTcJa-2<=#OAur(e5VU%lEtuR4bl<cN_F?M;Cyt+^U@Wb<E5kb5EYP6b&~h
z(F(SCA#Bn9g)+r1Y`nJYpm)=wapi;6rajTE>$|_o>PFr&7jZ52)vccr?>E_3DCadM
zx-2)xSxPuQ`)n_rck%o0O?eCkV-cNnMJ%LCA`y~OdO1TQj@f{j=anqIOQn<HY_E8K
zq}8{wNT1CYyO6WFDy8(6-D?$&6Yc_gOukVCi*Y+jzwVl(2rS3xDJ&H+B}mP~8**iR
zGop|3iyJ-Tm-iGE+l}_vz4FZ97}eb<GBz+)T@OHvSZtk#H8^7Ycr-LhzJ9y7FY|Ih
zC;$5l_xNfO3*B~lrO<}Lgy(yvUKH#wC=AXI&$2goa?s;kgn}tAvQf<A?%BZhP%~j5
z$m)V@jKA>quas>6XVF(yvu}KrG}J6$jPw`zc0|Zh=b-+yaZG#RiN&GwCr+mttc`js
z;Odl*3at1K-?;srqk<%%e)meDpTEn|SdEH7L8mSH`9rl0$i0HN4L?b~R;9dDHLr$E
zMog`fOV*sPvZndOt~A7rmb>xM<+1xnvzlZqT9s~(Nl&$)SREr)?BNA^Tk&bjD%Y~@
zRVe&HR~henHw{x|?#s`o*9dRq(O<RU>}AN(8o#c;PlCsKWt3D?nKWs-M(rmRN@>lF
z_6YJst{pV|@!@nQc+Qcx>ymAcuf4u=j7)X@sP-|0?9CuCNo_i#LTzzzlOog&N`=k_
z*(zif=dajNp6ez51d4WP7v-HBiMKm(@xW(Z>%^<-l}9uJj)sDM{1+D!&rlofV`2^+
zd7v&ZFY2G7t1dFr^Wf*flG!%mXiLpzjYIoy5F8J!iymXW7qYX&J-lV(^SQuT)<L(b
zVK{2sr}*59&Nq55BxPC>?=9O+_-1_H%eGZ%IM2DH>}kJlrr#Z7gRq>%uVNYD43UlF
zN+uBv!pqNQ=X+gaL=(<;XQ`IMI*K2MH08|f%iJcXaFb~g$;j!&Z(`Z63Pbnvh@PSg
znNCo+=`a=By+x8TPsyBIJJGJ;U*17qw7bKBv=Fr=dh}S8+29@NrwTWE7Z!EoTQlCj
z+_`gxul1#ji@crML*(|0Ac<4?dKLtox{e}3QO#D<H>q5CBjtAVQHJjLkg}eLX!}iX
zzRE9qI~ps6n<pBzG)*&v<*I*~;@tXi-~EfC()L!+lp^5O7VF2d6UQAJ!{Wr-D0znK
zr91B?Uzb+dZ)V?roOr<E&R!YI#tKl5O>%u36lDvG0;eY>*VVXwxHl#(kfv@Tm8|8b
z<HL{poh;{R+x;n__^~;?YqF?GK>WQOhi=iC(&I8MZ^{wQxb<6mrJpo8^3sgS%fR)Z
z1v{npOi0J4g(k1yq$MBsVBedTx44<K)Yt+HGfhlvxffqkj%#PG4({?lFz=S1LTNjk
z(y1%9`I}MeEENvdzYFU5fP0JHFXha65`PqHUYayu*<R~$OZN_L;cilujJbo}KA-em
zc&lr=QzL#S!xtMWD;OTWZvHYR>Ky2iy#3xo>BNh?UPt_&@^4qNmP{&dE6IItIGAZZ
zXvw^M=F+QsElK%7h7}KI9!`GBX}Gh8Qrlfnbmo+HN{`6w`8-aY8Q=UUs#s7E`Ez&k
zt9Ksyk=G?MeR5rArZ=|<o1KBj>3xn62-n&@@KP;ZVFe6JkuHuoA;nt;A0%YZOH@@c
zkLQCi_G4w-{mxze$y3}G1qES~SDu{br(2GH;`!ZVF71wcuk`cyrGdJqL<TL+35st7
zM{uv>gKNAaT=#$W@b~YodVWb44yeE%w;mYrUhGk!R_hm6*Vwl`2(LMv$2VBhrdaZc
z<@)|_POWzny0(;>2igT`@>y)pNm1@kLiU6!rXE!+Hie|W951Z*7B+F2_b|(<>5%+#
zV77N45pHgNy8e|Z+|;vHYPu;Gn9ZjI#OUkou4B->$zyij_45|S)gHY}kD%A@>BGw|
z1GYdu|J=6qnDRU6+v0ie`CG)gRcCIfhmMGk^xl<{nHI8=OEumqk!ep?J0M_UkbLNd
zP_MODzo3gCYa+wK1>D5&E{^htzVElX=dWqVB)AC5J@Sx~`0RJK=GokZ#lgIyLP}~u
zcnbR<-Y67-J{{XxQ=%azTrgX^WVPk_TWwh=Prf}Z>4}dKBZ*K@RMo}RYHr=Wf8DU~
z#@z7S>r7x%?&qZrcKxtbQPcVwuhqI(!)qoEB@;76t3+kxA(_nt{N>zXr_tG_w5+ph
zIiK#<H=KA&sx?8{j@|ZQ_LkWa`Qwm~TKC*1@5m=P;|HfD3LbcPe6OS)NFjZz8SNK7
z9BI4SNuT`kp`!BIz8`DK8(J+Bjvfv^zTS?u?kwmpPdgVD5D>x({rUkR0I}lowp4S<
z85Irah;(S<WEZoP7n!b=V@CSw_#!Os8EP6(CmttkEu|+No!n;W1&?{}nhv&b-|J4|
zzg|6Ys!;H?c47QGb4#zM@GUR6FGc9wf~A5&pNmnE&%?#o*zpzn9n69!bh+=yedvx&
zc+n=I$n%BO=|ioCRySkC%`adF>(rD4g)F!(MV1a#9qeL`F%)s1=gb9y3$Bip5~e*u
z`93(jpxZ5~!MAC~C#xvQiPy7vK)Vx2269aLkX=#DD5$<|r}y@)qW>j1@jfH*JD2IN
zDupLkW>ZCFHzL*FITHkbcrI6dcHdTiG`YR!4X$V=L((pqD@j47S=v%Qz=hJzlonIf
zP`LMD<R?03vTmU5Psjj;^9H5EnM_CaJ8r$U%UPhRWuj{_|EzTg-!sm86G_Q+JX)gf
z$27N6mpeK`slZw3Xw3m!wEDp5=v<!Gr_Xn4iAq@sZiIH|5A^kN9wGGy9<9}_?W%KG
zZRbu=F_H?Lu>OAiR(*bAEycY@Fyv9QzjDB&)^2lGN;iFVcHFb0g;R9N-*t=i+@wR-
zo%aXpIz<No4ko$JO9!JrEao#!FE+m2^d@eE$7F6KGLJLWeq#4XnyBBC!~2oRQ%$>H
zYd0b9!mYh3w}nzUElGoculveuMQ4S~M+GmuZB$rmf4ARCgQCWlIF+T%iBRI_)@=H+
zwJ*Mv|2ZEV6;UF4=G7G|Nm63RZEvT0@M=;)IM6ZZ+ARH5aL=%7-fURDP_sR3QmE`Q
z#aR2LF7+p4c1x{%>@nwEbO;pU?_BNgj8jn9i`d!|9AP^rSvvxN$O3?)gDf6>WC<h^
z$%$l#5Fj#`I7G$Wm;X0A_X+vCyLtF1_`9D@^rGT;6SwBzm=m98;RIMfQ-GiVfC>OP
z5toev{`sz$jl1^mfV|JfX^H<UAo7XVsW{Ppb!+vl9Go5<69^Ch5Jk6`ixc?!WqTej
zoPrR9esO{q@(^PA^%uaChyeWi8Xf{5JPEso#}km>*8n^W0;s=#J%8PYo`vybnl%JZ
z{9}#s&y5I~_Art3e;fa~k3_~}F9h*q3>Y*pnT$ye4}l2rx8x`&R0sqSh~`4*f2_g3
zAO7PkfkXouBmo$<P-XxSn+SRwNaQQPaZ`SS^vA7a5DOg!NB|ZknMj5(k?<(nFcuLR
zAV64pU_65SSr^LR#UkVJL~LM)Ou&N}dWa;1gk6Kk0EjI#5kg>^T9E)ua%d3<Bm|+k
zkVwK~!4MDv2^$0g$q1HP2m(+IqE!A<i4aJ`0)#4pM8R&vgAg_d9wK5;qgRs=Jhmhd
z5u#Zmpbxf85JD#W6$AX!dw2qbM`*NwkZ9;9fQg(XI4;z@WbC~J0H!4p0kAg5!)O7q
z<U#~8ja6Y7q=f`Q$S*nlGSA=Afgp$m41}r?t3{MF5St^4nHDrez`6*J#{DOezv83z
zg^09$gMiRT0tN}Rnnfo7jZ9EyU_nDLNRtQzQy?0rK`>0)4`2d~bJ0T61V&jPVdVsn
z2((QMMxa0Tq51!pewawaqDH$hR*R@B@GzEs_!s{e50D86tv+D#Z|(gL{vntQV^O2i
z0*?&>kWdw3f`A|`gJ`3qaX1;R9X2_LfTs{>S_T16!Ul#=#r==KG=c*WGMT205CAew
zas=>CW_}x9C~RzYL_Dp6QN7aGj*J!=bCv|+X*xSZfPSC2zxanp#J}43-&#OOFztjS
zps+DPpkIv%vj&4CTIaw7nqdeN0fd4@O#p~Av=TsCfCLEsbN>HVz-Wv7r?-DO8~wl_
z(O8>62LBT9f9DoLB0*Sz5YgU))dG=>2e2%leUN5Gk?|0M?F(d7!N0GWq7winKv>bB
zjh%$0l}rM$bw{lTk+A?F<d4p7LPUta$NE)i<gdj4t~88Ngxv>&FjmI^o`@$UrdHq%
z94CU1I{K=qhKJNhct{0MS4D@kimDnyBqK1QdO-32-C@mg-~fw{udTPQzqg|k3;M-~
Oeyy;GiD?*Wvit{oM)U;$
delta 6457
zcma)8c|25o`)(x5SPP|4D9Kjm%$YNr5ZNh9*@-YJYh<S;Ep{GD(@-J?*(Gb16ta}c
zV91iCR7$d?RN_57@B4c{&olFWKELPuGv|EIJ=gcXuj{(M_i35ts+;CYy1cP9Q#UzM
zfszAANOAQ%_j>M_@z!KnS5=iDATh_B;P-s)^Zdccg^I&tidT|qf*RCT9<5Y0wbLfV
z(q@-ljh%+X>9q%f!ovB~6^zOkDuvJUkBk^+7#E!wU#c|2c^+7#J=d*0pXRu0+AN)?
z@r$;vk<mw)9ku5liS8!~0lo7-zG-hfJReF4JGNC|;>}lG%$6;UPrtMuKGJe;H>HP;
z-B+Jz{={uacSZDgzxgIDBaMvp1kXua-OZ_ty>__-?M*kEG-U<OoV$>KTM6yRS`n`C
znP;4y<LABNLF7i)bTB*kLb1YUEf$6Z_=E%c6HB>K2~EG;qVf|8)AWaOt8gJVouprn
z9c=Rpf?PB;M}}HASoU!}6x=J<DY4?dZTa@K8u;f^o1(Ca6k$tGP4lGtrYCN8Z*@bf
zX<WF$YhS?AuUMKogW5;wj_<mSt2=e8#%eYG&?Sy}V}}7Fzow=E?+sL3*ca2s1-Cb?
zH^sT#1vy5#Co1_yvc$dj%i>SGEaD9GSC1YWn)L{+nK%;5{5c{utVVikwo~-kj;n%e
z+ts-8;$7_ARi&MMXX0NtKRFfh-BloT*DM?&YFKh~FQgcG$aJ?TozhX~JL|+qAO9?!
zVkO6Ao-HPMg0aQh6zq~yw7rh{1(jdiX}NMo{C&{OD6eW{e36xcPvudOwuec0l%MsD
zs;cK-fe+rUlk|n@&%43GYoakHozAU&t6Vxo-M{pnCw9RDS5$T4`k|0$zajjk&_eH%
z?&XJ1X49cwLuU_Xk!p%z=gy?Y@Sn1L<*DtG$-9=L^#?MO%){H!j2%w>nL>rpspIb)
z2tKK!YXxeTCbdFZa~r95KDl!BN$BpGiMYiNUy>2O6`zz8`^N_<SqHP=;Wg?No|v@p
z&%oBOxd7fDkLoyr>4!pkdEW_sIjs|td|q|$!|*Tpt9qOG1FRapQ*0I$&TwqBxJ#ru
zk#t(g;`_3+05W%4B{S)GublGsneKvk%Gv9Iq^)z@smgCLwqkVJMh#4mc#BbH%au!f
z*&4UW+*dyb%jlPJN_<xyYIfV`KAaj{qL6l9smxRIrEtgF!;*ccY?k&OlYf?T2yJa8
z-XePAY4L>O>sFOJ$|96-v(xY7t(xWcdY@ISZn#4h?qeqU#FYpZ4Vqhj57&IUyS}eL
zQ`_fT>-+S!#5J$GvGdFCcEujI+(y>I!mTBmZ_Fp7#Gi+D`q9@fJbG|hj@y)LPb}fx
z>FzsMdUn~I8ED`)5%J>i!?vV7il?hMsdRpp)@a!FVvgsyARmu1Cq=0C($lB1(HLg!
z?xKX}axHb;J7;v?8yEVj^Mr+6UcSo57v?-0jV{&n{X~oo&#EAcDE*Oklk4z-MUV19
z+Lt*Y8RsZ5=jtaC5!9$|JBjhlQ?y&>tX-X`N`vY<%i>JMmuDU;-M<rXBKF%0=-f!X
z5FbZj?KcMeY`4}KcgT{mdh_<Z*W>Z|o^r)t=qUqXt_U<r_pVNxlBz6WX4|o(HqUk^
z8CQN=J78Z$AOk!sHO;TH_E7q^UV==X2ydRP30+V*UiIAu6}jX&A#=Oj^ZJ)t!>_e+
z#$tw|6sGnj3fYWB%gop|(y&{UqPV2nO^J3tnG|BHg3;OQb9v?ziGwdz=SWVHFH3fm
zMpp-lfCV4tr!<y#1WD<v?|Hd1@yLy|YlanV4KnR}1Qgyra5mLx`})UKTz?{<H<wa(
z%Xl<qn8!mm`oc4h5#eh}4G%9cqC1#Va|%yPB5ZBv_bWX<OrV~QZX*@=o6D00jSH$B
zuUH8A$#68+j$&}-@|32py^9u6Zm83iWi$0gHQMu$%AmnnGbsC8S5BaiY_VIS_|d!T
z3R|tLDKVT%I@!P*a0r(?t(W{mu$oa3aH+S=EIgZ(z`q<zEo7`#1S<4P*R)-Rd)fmf
z`Yu{{+6@>7J1FFpzyZ124($y5dF8{Ptlp=6C{;tJu__XpLg5guJT7;_MY;3@-?I7(
zKf7A}&PJn~^^E20%6#lg!-L)P_jAa*U7C4$uy5|-YV^r6P32xPUuEtadFjVwNj@d_
zlC2Gtt9!Cc<H#9@KLkXZ-)+d4HI~$}RvO%cRW*8tO(XXETD(hZ+2<_Zh2~3h&hYWz
ztoX33-&3qQWll-ST$Rywr(}8>^d5Qn;1=IR>q6T2n+G~E3=t#OXVjxH2HqHrfR>M2
z?x^AB?(Ia`Em7BuWu@O2WtwCd_T)CzDfbjz6xnw#E$5!AdxC@I4wq$1{d!Rz)x^$u
zugMo(VI_C{?%4L8vUMuvol)T0$%z`MSpctU3{UR3hzff_0Us>fNXZo$4|OVRIodbZ
zYrf<BloiurrPObY&a_aLu>JINRz%jWu-T%>#xPpr1(%_W@@zd1M{ik9!SwRZ@j1?G
zfRD}LUzMecTlF*#x!vvn(wHefFE@sX(PJ!3#ghF?&WLv&@iB{fa?iNgLubSexLlqr
z2TK>0Z`yJ|oAUaB=-g0+X)|_F{cYE2=Ecn>oXu!gCEn;Edo(UYLA(*(B|hrbccEq^
z?BVAZ%t*Dd0M`Oio3bF9aYm+CDs!0W%J2+`vf)TAs`kEnWLA;f?C|8VugS-EruM*w
z{znVJ;Z|+<!tXi;CjoMe^2pUgA6rMCwDij#+-Ahv`JD1hIc4D4rzjocFChQ>@FeFC
z);(EVPC1%ok_*d(r_60%kB%m-^+#xzN1x{CrO)cU6S)?<|EH&<y=}K|(J#gsNlPky
z*>gG(-G2VI{CZ#=d3zHk?%hM+bUm1l)xU1X^xUIzQ<BJWZNcny{cSTB7)QPF%3ZA0
z{~;h{YGpwQ13%|=ucuiF<_;WJ`(y|L8oNTZ2g$OVy)4YesM+ziB6qElUlq)Y@5w!8
zabSV#Cr@VnmSk~~|C~mT2Wjz04d|_z+;`OVNV>>+^nli^Q@e*mj;}`3*ohxn@XcBH
z$eXVj#V5Y`t(XU);}*!XjcJ5e?*q0(MrO|RHx6Dm?(VxCm}7n<Du4c)Tvjw^e9MU1
zxwuD@ue17w=!4RF%HJ~#uDYH{2_7v?urFzM9%}E}*iJOVcuh<!7#TL(2m~qW_Hc4N
zQwi8Jq@VhnSAp_${ZPlZM=5dhu2gPYwQF5x$0S4~E2}+Ai*&5g0%Ymqlc^^XHJD8h
zrsqInlTH7Lw#aZVtp=1?&vDv4_mn`YorkTjL_rH)-n@eRm}^JYuoIU{_BN@G4J~ty
zZhmBQwP<UaX?xo{&Zs)=<*CgApXKjg*sbJZ4^15eeLGVF(c4jysYz(Jt@q47?rj`V
z-Z0&tXg6QF`0G)q*znHiRDM2?lC!|O`f+n)tM2xt1<|!^-gVr`?jT7&1Bu~HHg$$=
z2O6Luw5w2vk(E<PM0I!a{l+J@{PHHKqKFMWDh9M0q?!+9b<Zmc6@7{?*X6^vOQM>m
z>ov*WgI*IfyI1bxG}XIQOkyw7Wg;8pdkPBybntxhfjy?b+yxKr3dC6)p-k<2M$Sv&
z2rqc^#cYRm{;~8t;`S8F<>0>MS_z63{o%siO}q|x6FJ7kZ^w-7wkqGtOTB+oP<+3R
zoS$a{q`l%aY{TI=|2lLwxk|0pIL3CIYNQcYr+Cm!ASSa+)YxXq>iF^<chi!ODp$VO
zKb*65F}8Sk$Hvir+&84pi6KOBIOXmkwIgM3RVT^OU3)9(miwD%PGKNw?EcEn(S(?V
z&71rM0|Z_*ZXmW5CAx(<l@;adf<pqjkL$jlrAlX-m3I60z}fYKi{~~x9@u))&VtL&
zSoOLysWgOCnIY>Duza@hY?{eorw4v3Dirry$Es99uQp&ZLuub5C-!M&P`o#50rfq_
zrz6yoe+rd?vnQWQ6=<j8`IeYE2`bz|QrOU^Q=xIHk)v_Ze6&!rgt+b{#bd#vkMOGM
z)t*N$Zkmlj?Qn24NONB^b{P(rUi8clwl8$E{Mc+A@>VOq|K+O^eP8OakLP>og$K^W
z#-)Fs6A~^Q^S9`ZF>~p)SW=Nr*WcN|X_!LITN#)Z;s26NJM?P9BPO@73$IIy^Kp1U
zYDI>uqbjAS;=Z7jdP+cw@+|#mvNXfNw@=Dl>Zu~{*iVkOa-y{B`49aP!^gkHSt~P1
z_7`5+n@-PuKAZL7{5-R;wB%-S^bH{<U>b>oFs1yXgE=WlO#fHGWt^Y=a<6YIJkXVq
z)_TsAivSmw);tsGuy*KDT{Y>^|FKLWoaW!4c)oFQV_)_fkJth44A-^KQ>m{-hl&ZI
z#cR)A`~e$j3h>K(thNaxf$|?-Jt$mN@ByreiJz|t+_RjPyd-JFLD%R^TB<ir^nK|s
z(J4u;9(<;f71*yQ!o3S0M%oh#8dE}~`$lN*Pp!96*10=_+9y*_2}+@Gl~)CCT2sol
z2U72g9iCip<D}L}Mo8=?7>!2W0YjkNCnIn+{|9p$Ti<T&u~<6e`kRSB<1D&YD<im3
zOwVO@gPwD#ddG0AOa4MUJ$ZnW5jNh-NVdG}erxG!R>o+}uGT}-8;<1&2b>AYtoo#@
zJ6TxZ2zU&tko<6I)DoK632Aw~F3PVcTe(w@O$+L`qZSQv6Vxt=?e(8Mr|tD}$2oj!
zT;M%#lu6mkL>U`JJ*E8g$95px>u3Dc)^X%4cB{{0hQ8`U-yx=@Bouc_GNH<P@2{P0
z#=}S!*DvViELGhQT(1qW{ej~iEADokp1)}M<%KBN!D}pa{WZ0ecCdPC<57zKh?C_O
zN8ON!D#^U2*ebEZ+4Be!Rgw|*GDQt3RRVS{3vR*8hO$R-@1qeWx?jc8H&fr79Sj|e
zq=P|9iMsu$#HVA`uhY_1-<;OIT1+1|O^>l9k#f+dLgx&v3~EEHj%cK7K|F?JlSZX=
zMyl1ad96Ub%Y3c)oV?E}rE{al?2C|znrn;SW2yGikYiUsjMw8N4KF>@uI|lkVjMF{
zU88rIiL>)X-0$Xty~Z79B9!t6Dz+cnjq7M@bvu{%Qb2F^WjuXz*u~wOM>2K?K4y@_
z6Lmc&kIzLIbwnoQUUnh}eWCKre3H+aJ1h1}z`;HxRrlqpMcG`K0nI`7JGFVWk`K54
zK~4YpZGL$Z_KHzY(wV)}E@iUq`>e{v%1493?aTA>cNJX{{exj#u~v{QF+DKny(W<t
zS}#iWc0K3sM?UF=M(%u^-O)shG$8%^1`EU3%a_j7UOIy!k@h$P&Nw{A)kVb_i*-=}
zL9(j~fLtnMz!d^8M4~eWPoz!IQTP8@WK%9m8x0-@VG=+ffdm>~9t!;Hvu++L_Mahr
z$wTS=vq;B$l-xgxtS!h#8F6rfAPf+Y+<p|GB>wv#S%`{OfMMz1#RJmb(&*p6AV9za
z*uSp<5QrhtHdmlTP*~bzAxcCI0NElSB9UzkCgR!Fa0D7ygh1fgUl9lZYd8iV;8@o{
zB7qk18v@6cCk6vUtl=2wf2?6~GzJ2pfM+WNLjVYWhX4UA2+{<KQTq<EgA+j(0+C<>
zz#2!y6EQU3Vw4C4V%-n{z_6Bx1#mDcn?wLv{Ci>mM8y8~`0wlg^aJn&#M~@v5D^6b
zjVJh*KnMrXHkTkgvXuZ6a4;JN9#3T5AI8CW+R5J#Fq@hXKx9)B!myPJK^T};@f!le
zS}_3OF{}y$L>$1L8RAY<DMBumML7V%Aq=sQ0Yd=H3Jc*7fmq`(SR$*A5Dq4=?g4|?
z|B&?;av>ZD)3TAA*vW-p0$ZzKu^9H8APA-{{4R@aO9)Y()kg?37}j(_EDpyShoG_=
z9DpDkJ9QAA@bCZrwJbz&T5=gu7Q4rgl-LBv0x;YDSdd7Y{0+g@3J?~{-j7(At(zbK
z2hzZDlqiK&Gmroi*|f#769ZxKY{XzO0IS|0(pV5H9v0F2KMgDJ->xIVNJ@-yL@f5B
z5wQ`gFc5%e%M&CZo?-DI1_NPPNyUQ5d}4_sVlmkNAr^q8`QAl|h~ZglK$;V#$^3rB
zMgs<i9Iua%S84>dtYHjWh7bsXtQ~>D1Hhl-LJh-O5JV)fH6#H8U|1oLGaE}giA)?d
zwu2Byz_QN?7zSCr03k!4R`DkU>*0h&J_uNgL#)TP6%68G8tUHv$^wQUw&4cDNNOy~
zz&HYdX7(F`%}B@_3~P7bu>jlj#Un>QE&ERhRxc0%q?=iGBqB|~wuT&0w1wXgcveM-
z1Y~Ib9RjgEL}0TF4ojqIRw58MR&<DfV=E5ne6}nQlM-mj2m}gG%d14GJL(d(wQzV%
zZAeQKCh7p1I9(j5i`Ui$h}yaY<Xc4j;Qt%pfL2#WpYuQI=O64xc0(hdFUUYe%gO1O
H=%W7x<CT}l
diff --git a/src/plugins/e-acsl/doc/memory_model/article.tex b/src/plugins/e-acsl/doc/memory_model/article.tex
index 67e401ee44a..3f635e815f5 100644
--- a/src/plugins/e-acsl/doc/memory_model/article.tex
+++ b/src/plugins/e-acsl/doc/memory_model/article.tex
@@ -692,18 +692,14 @@ $ptr$ are initialized, 0 otherwise.
\begin{tabular}{|c|c|c|c|c|c|c|}
\hline
& alarms & time & test cases & mutants & mutants killed \\
- %\hline
- %$p_1$ & 5 & 22s & 27 & 2 & 2 \\ % sorted
- %\hline
- %$p_2$ & 19 & 34s & 31 & 6 & 6 \\ % f
\hline
$fibonacci$ & 31 & 54s & 38 & 20 & 20 \\
\hline
- $Bsearch$ & 25 & 65s & 20 & 43 & 43 \\
+ $Bsearch$ & 28 & 63s & 20 & 41 & 41 \\
\hline
- $Bsort$ & 32 & 200s & 153 & 50 & 50 \\
+ $Bsort$ & 37 & 273s & 153 & 45 & 47 \\
\hline
- $Merge$ & 52 & 106s & 19 & 63 & 63 \\
+ $Merge$ & 55 & 100s & 19 & 58 & 58 \\
\hline
$BubbleSort$ & 31 & 963s & 873 & 44 & 44 \\
\hline
diff --git a/src/plugins/e-acsl/doc/memory_model/experiments/Bsearch/bsearch.c b/src/plugins/e-acsl/doc/memory_model/experiments/Bsearch/bsearch.c
new file mode 100644
index 00000000000..12938539bbf
--- /dev/null
+++ b/src/plugins/e-acsl/doc/memory_model/experiments/Bsearch/bsearch.c
@@ -0,0 +1,65 @@
+/* run.config
+ COMMENT: BsearchPrecond
+ OPT: -pc -pc-trace -pc-tests -kernel-debug 0 -verbose 0 -pc-deter -pc-trace-preconds -pc-trace-simpred -pc-trace-result -main Bsearch
+*/
+/* Binary search of a given element in a given ordered array
+ returning 1 if the element is present and 0 if not.
+ This example is like Bsearch
+ but gives an example of
+ a precondition coded in C */
+
+/*@ ensures (\exists int i; 0 <= i < 10 && A[i] == elem) <==> \result;
+ @*/
+int Bsearch( int A[10], int elem)
+{
+ int low, high, mid, found ;
+
+ low = 0 ;
+ high = 9 ;
+ found = 0 ;
+ while( ( high > low ) )
+ {
+ //@ assert high > low;
+ mid = (low + high) / 2 ;
+ //@ assert mid == (low+high) / 2;
+ if( elem == A[mid] ) {
+ //@ assert elem == A[mid];
+ found = 1;
+ //@ assert found == 1;
+ }
+ if( elem > A[mid] ) {
+ //@ assert elem > A[mid];
+ low = mid + 1 ;
+ //@ assert low == mid + 1;
+ }
+ else {
+ //@ assert elem <= A[mid];
+ high = mid - 1;
+ //@ assert high == mid - 1;
+ }
+ }
+ //@ assert high <= low;
+ mid = (low + high) / 2 ;
+ //@ assert mid == (low+high) / 2;
+
+ if( ( found != 1) && ( elem == A[mid]) ) {
+ //@ assert found != 1 && elem == A[mid];
+ found = 1;
+ //@ assert found == 1;
+ }
+
+ return found ;
+}
+
+/* C precondition of function Bsearch
+ This must have the name of the tested function suffixed with _precond
+ and have the same number of arguments with the same types.
+ It must return 1 if the parameter values satisfy the precondition and 0 if not */
+int Bsearch_precond( int A[10], int elem) {
+ int i;
+ for (i = 0; i < 9; i++){
+ if (A[i]>A[i+1])
+ return 0 ; /* not ordered by increasing value */
+ }
+ return 1;
+}
diff --git a/src/plugins/e-acsl/doc/memory_model/experiments/Bsearch/test_parameters_Bsearch.pl b/src/plugins/e-acsl/doc/memory_model/experiments/Bsearch/test_parameters_Bsearch.pl
new file mode 100644
index 00000000000..a06b2298d3a
--- /dev/null
+++ b/src/plugins/e-acsl/doc/memory_model/experiments/Bsearch/test_parameters_Bsearch.pl
@@ -0,0 +1,29 @@
+:- module(test_parameters).
+
+:- import create_input_val/3 from substitution.
+
+:- export dom/4.
+:- export create_input_vals/2.
+:- export unquantif_preconds/2.
+:- export quantif_preconds/2.
+:- export strategy/2.
+:- export precondition_of/2.
+
+dom('Bsearch',cont('A',_),[],int([0..100])).
+dom('pathcrawler__Bsearch_precond',A,B,C):-
+ dom('Bsearch',A,B,C).
+
+create_input_vals('Bsearch',Ins):-
+ create_input_val('elem',int([0..100]),Ins),
+ create_input_val(dim('A'),int([10]),Ins),
+ true.
+create_input_vals('Bsearch',Ins):-
+ create_input_vals('pathcrawler__Bsearch_precond',Ins).
+
+unquantif_preconds('Bsearch',[]).
+quantif_preconds('Bsearch',[]).
+
+strategy('Bsearch',[]).
+strategy('pathcrawler__Bsearch_precond',[]).
+
+precondition_of('Bsearch','pathcrawler__Bsearch_precond').
diff --git a/src/plugins/e-acsl/doc/memory_model/experiments/Bsort/bsort.c b/src/plugins/e-acsl/doc/memory_model/experiments/Bsort/bsort.c
new file mode 100644
index 00000000000..007fede5caf
--- /dev/null
+++ b/src/plugins/e-acsl/doc/memory_model/experiments/Bsort/bsort.c
@@ -0,0 +1,50 @@
+/* run.config
+ COMMENT: Bsort
+ OPT: -pc -pc-trace -pc-tests -kernel-debug 0 -verbose 0 -pc-deter -pc-trace-preconds -pc-trace-simpred -pc-trace-result -main bsort
+*/
+/* Bubble sort of a given array 'table' of a given length 'l' in descending order. This example is interesting because of its
+ - variable dimension input array
+ - loop with a variable number of iterations,
+ which is limited by limiting the array dimension
+ - oracle which does not sort but checks the result is ordered */
+
+/*@ ensures \forall int k; 0 <= k < l-1 ==> table[k] >= table[k+1];
+ @*/
+void bsort (int * table, int l)
+{
+ int i, temp, nb;
+ char fini;
+ fini = 0;
+ nb = 0;
+ //@ assert l >= 0;
+ //@ assert fini == 0;
+ //@ assert nb == 0;
+ while ( !fini && (nb < l-1)){
+ //@ assert fini == 0;
+ //@ assert nb < l-1;
+ fini = 1;
+ //@ assert fini == 1;
+ for (i=0 ; i<l-1 ; ) {
+ //@ assert 0 <= i < l-1;
+ if (table[i] < table[i+1]){
+ //@ assert table[i] < table[i+1];
+ fini = 0;
+ //@ assert fini == 0;
+ temp = table[i];
+ //@ assert temp == table[i];
+ table[i] = table[i + 1];
+ //@ assert table[i] == table[i+1];
+ table[i + 1] = temp;
+ //@ assert table[i+1] == temp;
+ }
+ //@ ghost int old_i = i;
+ i++;
+ //@ assert old_i + 1 == i;
+ }
+ //@ assert i >= l-1;
+ //@ ghost int old_nb = nb;
+ nb++;
+ //@ assert old_nb + 1 == nb;
+ }
+ //@ assert fini == 1 || nb >= l-1;
+}
diff --git a/src/plugins/e-acsl/doc/memory_model/experiments/Bsort/test_parameters_bsort.pl b/src/plugins/e-acsl/doc/memory_model/experiments/Bsort/test_parameters_bsort.pl
new file mode 100644
index 00000000000..ad41d5bb9f4
--- /dev/null
+++ b/src/plugins/e-acsl/doc/memory_model/experiments/Bsort/test_parameters_bsort.pl
@@ -0,0 +1,24 @@
+:- module(test_parameters).
+
+:- import create_input_val/3 from substitution.
+
+:- export dom/4.
+:- export create_input_vals/2.
+:- export unquantif_preconds/2.
+:- export quantif_preconds/2.
+:- export strategy/2.
+:- export precondition_of/2.
+
+dom('bsort',cont('table',_),[],int([-100..100])).
+
+create_input_vals('bsort',Ins):-
+ create_input_val(dim('table'),int([0..5]),Ins),
+ create_input_val('l',int([0..5]),Ins),
+ true.
+
+unquantif_preconds('bsort',[cond(egal,dim('table'),'l',pre)]).
+quantif_preconds('bsort',[]).
+
+strategy('bsort',[]).
+
+precondition_of(0,0).
diff --git a/src/plugins/e-acsl/doc/memory_model/experiments/BubbleSort/bubblesort.c b/src/plugins/e-acsl/doc/memory_model/experiments/BubbleSort/bubblesort.c
new file mode 100644
index 00000000000..415b567a1d4
--- /dev/null
+++ b/src/plugins/e-acsl/doc/memory_model/experiments/BubbleSort/bubblesort.c
@@ -0,0 +1,44 @@
+
+/*@ ensures \forall int i; 0 <= i < length-1 ==> a[i] <= a[i+1];
+ @*/
+void bubble_sort(int* a, int length)
+{
+ int auf = 1;
+ int ab;
+ int fixed_auf = 1;
+
+
+ for (; auf < length; )
+ {
+ //@ assert auf < length;
+ fixed_auf = auf;
+ ab=auf;
+
+ while (0 < ab && a[ab] < a[ab-1])
+ {
+ //@ assert 0 < ab;
+ //@ assert a[ab] < a[ab-1];
+ //@ ghost int old_1 = a[ab];
+ //@ ghost int old_2 = a[ab-1];
+ int temp = a[ab];
+ a[ab] = a[ab-1];
+ a[ab-1] = temp;
+
+ //@ assert old_1 == a[ab-1];
+ //@ assert old_2 == a[ab];
+
+ //@ ghost int old_ab = ab;
+ ab = ab-1;
+ //@ assert old_ab - 1 == ab;
+ }
+ //@ assert 0 >= ab || a[ab] >= a[ab-1];
+
+ //@ ghost int old_auf = auf;
+ auf++;
+ //@ assert old_auf + 1 == auf;
+
+ fixed_auf = auf;
+ }
+ //@ assert auf >= length;
+}
+
diff --git a/src/plugins/e-acsl/doc/memory_model/experiments/BubbleSort/test_parameters.pl b/src/plugins/e-acsl/doc/memory_model/experiments/BubbleSort/test_parameters.pl
new file mode 100644
index 00000000000..0ae92b1c264
--- /dev/null
+++ b/src/plugins/e-acsl/doc/memory_model/experiments/BubbleSort/test_parameters.pl
@@ -0,0 +1,21 @@
+:- module(test_parameters).
+:- import create_input_val/3 from substitution.
+:- export dom/4.
+:- export create_input_vals/2.
+:- export unquantif_preconds/2.
+:- export quantif_preconds/2.
+:- export strategy/2.
+:- export precondition_of/2.
+
+dom('bubble_sort',cont('a',_),[],int([-20..20])).
+
+create_input_vals('bubble_sort',Ins):-
+ create_input_val(dim('a'),int([0..6]),Ins),
+ create_input_val('length',int([0..6]),Ins),
+ true.
+
+unquantif_preconds('bubble_sort',[cond(egal,dim('a'),'length',pre)]).
+
+quantif_preconds('bubble_sort',[]).
+strategy('bubble_sort',[]).
+precondition_of(0,0).
diff --git a/src/plugins/e-acsl/doc/memory_model/experiments/Merge/merge.c b/src/plugins/e-acsl/doc/memory_model/experiments/Merge/merge.c
new file mode 100644
index 00000000000..2787cc569d1
--- /dev/null
+++ b/src/plugins/e-acsl/doc/memory_model/experiments/Merge/merge.c
@@ -0,0 +1,63 @@
+/* run.config
+ OPT: -pc -pc-trace -pc-tests -kernel-debug 0 -verbose 0 -pc-deter -pc-trace-preconds -pc-trace-simpred -pc-trace-result -pc-k-path 2 -main Merge
+*/
+
+
+
+
+/*@ ensures \forall int i; 0 <= i < (l1+l2-1) ==> t3[i] <= t3[i+1];
+ @*/
+void Merge (int t1[], int t2[], int t3[], int l1, int l2) {
+ int i = 0;
+ int j = 0;
+ int k = 0;
+
+ while (i < l1 && j < l2) {
+ //@ assert i < l1;
+ //@ assert j < l2;
+ if (t1[i] < t2[j]) {
+ //@ assert t1[i] < t2[j];
+ t3[k] = t1[i];
+ //@ assert t3[k] == t1[i];
+ //@ ghost int tmp = i;
+ i++;
+ //@ assert tmp + 1 == i;
+ }
+ else {
+ //@ assert t1[i] >= t2[j];
+ t3[k] = t2[j];
+ //@ assert t3[k] == t2[j];
+ //@ ghost int tmp = j;
+ j++;
+ //@ assert tmp + 1 == j;
+ }
+ //@ ghost int tmp = k;
+ k++;
+ //@ assert tmp + 1 == k;
+ }
+ //@ assert i >= l1 || j >= l2;
+ while (i < l1) {
+ //@ assert i < l1;
+ t3[k] = t1[i];
+ //@ assert t3[k] == t1[i];
+ //@ ghost int tmp1 = i;
+ //@ ghost int tmp2 = k;
+ i++;
+ //@ assert tmp1 + 1 == i;
+ k++;
+ //@ assert tmp2 + 1 == k;
+ }
+ //@ assert i >= l1;
+ while (j < l2) {
+ //@ assert j < l2;
+ t3[k] = t2[j];
+ //@ assert t3[k] == t2[j];
+ //@ ghost int tmp1 = j;
+ //@ ghost int tmp2 = k;
+ j++;
+ //@ assert tmp1 + 1 == j;
+ k++;
+ //@ assert tmp2 + 1 == k;
+ }
+ //@ assert j >= l2;
+}
diff --git a/src/plugins/e-acsl/doc/memory_model/experiments/Merge/test_parameters_Merge.pl b/src/plugins/e-acsl/doc/memory_model/experiments/Merge/test_parameters_Merge.pl
new file mode 100644
index 00000000000..44c0551ba13
--- /dev/null
+++ b/src/plugins/e-acsl/doc/memory_model/experiments/Merge/test_parameters_Merge.pl
@@ -0,0 +1,77 @@
+:- module(test_parameters).
+
+:- import create_input_val/3 from substitution.
+
+:- export dom/4.
+:- export create_input_vals/2.
+:- export unquantif_preconds/2.
+:- export quantif_preconds/2.
+:- export strategy/2.
+:- export precondition_of/2.
+
+dom('Merge',cont('t1',_),[],int([-10..10])).
+dom('Merge',cont('t2',_),[],int([-10..10])).
+
+create_input_vals('Merge',Ins):-
+ create_input_val(dim('t1'),int([0..10]),Ins),
+ create_input_val(dim('t2'),int([0..10]),Ins),
+ create_input_val(dim('t3'),int([0..20]),Ins),
+ create_input_val('l1',int([0..10]),Ins),
+ create_input_val('l2',int([0..10]),Ins),
+ true.
+
+unquantif_preconds('Merge',
+ [cond(supegal,dim('t1'),'l1',pre),
+ cond(supegal,dim('t2'),'l2',pre),
+ cond(supegal,dim('t3'),+(int(math),'l1','l2'),pre)]).
+quantif_preconds('Merge',[uq_cond([UQV3],
+ [cond(supegal,UQV3,1,pre)],
+ supegal,
+ cont('t1',UQV3),
+ cont('t1',-(int(math),UQV3,1))),
+ uq_cond([UQV4],
+ [cond(supegal,UQV4,1,pre)],
+ supegal,
+ cont('t2',UQV4),
+ cont('t2',-(int(math),UQV4,1)))]).
+
+strategy('Merge',[kpath(2)]).
+
+precondition_of(0,0).
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
diff --git a/src/plugins/e-acsl/doc/memory_model/experiments/fibonacci/fibo.c b/src/plugins/e-acsl/doc/memory_model/experiments/fibonacci/fibo.c
new file mode 100644
index 00000000000..7d841734de9
--- /dev/null
+++ b/src/plugins/e-acsl/doc/memory_model/experiments/fibonacci/fibo.c
@@ -0,0 +1,23 @@
+
+/*@ requires n >= 3;
+ @ ensures t[0] == 1;
+ @ ensures t[1] == 1;
+ @ ensures \forall int i; 2 <= i < n ==> t[i-2] + t[i-1] == t[i];
+ @*/
+void fibo(int *t, int n) {
+ int i;
+ t[0] = t[1] = 1;
+ //@ assert t[0] == 1;
+ //@ assert t[1] == 1;
+
+ //@ assert n >= 3;
+ for(i = 2; i < n; ) {
+ //@ assert 2 <= i < n;
+ t[i] = t[i-1] + t[i-2];
+ //@ assert t[i] == t[i-1] + t[i-2];
+ //@ ghost int old_i = i;
+ i++;
+ //@ assert old_i + 1 == i;
+ }
+ //@ assert i >= n;
+}
diff --git a/src/plugins/e-acsl/doc/memory_model/experiments/fibonacci/test_parameters_fibo.pl b/src/plugins/e-acsl/doc/memory_model/experiments/fibonacci/test_parameters_fibo.pl
new file mode 100644
index 00000000000..04fefca54bd
--- /dev/null
+++ b/src/plugins/e-acsl/doc/memory_model/experiments/fibonacci/test_parameters_fibo.pl
@@ -0,0 +1,19 @@
+:- module(test_parameters).
+:- import create_input_val/3 from substitution.
+:- export dom/4.
+:- export create_input_vals/2.
+:- export unquantif_preconds/2.
+:- export quantif_preconds/2.
+:- export strategy/2.
+:- export precondition_of/2.
+
+dom('fibo', cont('t',_), [], int([-10..10])).
+create_input_vals('fibo', Ins):-
+ create_input_val('n', int([3..40]),Ins),
+ create_input_val(dim('t'), int([3..40]),Ins),
+ true.
+
+quantif_preconds('fibo',[]).
+unquantif_preconds('fibo',[cond(egal,dim('t'),'n',pre)]).
+strategy('fibo',[]).
+precondition_of(0,0).
--
GitLab