From 342785b6636005cf00391b5d7cabf55334790a59 Mon Sep 17 00:00:00 2001 From: Erwan Jahier <erwan.jahier@univ-grenoble-alpes.fr> Date: Wed, 21 Mar 2018 14:50:49 +0100 Subject: [PATCH] clean-up utils/lustrequiv, and install in the opam bin dir. add and install an alias to lus2lic name lv6. lus2lic --gen-autotest now overrides existing _oracle*.lus and _env*.lut files --- _oasis | 2 +- lustre-v6.install | 7 ++++++- lv6-ref-man/lv6-ref-man.pdf | Bin 324096 -> 324100 bytes src/lv6version.ml | 4 ++-- src/main.ml | 11 +++-------- utils/lustrequiv | 28 +++++++++++++++++----------- utils/lv6 | 1 + 7 files changed, 30 insertions(+), 23 deletions(-) create mode 100755 utils/lv6 diff --git a/_oasis b/_oasis index 95a9e332..d3279d7b 100644 --- a/_oasis +++ b/_oasis @@ -1,6 +1,6 @@ OASISFormat: 0.4 Name: lustre-v6 -Version: 1.732 +Version: 1.733 Synopsis: The Lustre V6 Verimag compiler Description: This package contains: - lus2lic: the (current) name of the compiler (and interpreter via -exec) diff --git a/lustre-v6.install b/lustre-v6.install index 9f2ec7f8..44409390 100644 --- a/lustre-v6.install +++ b/lustre-v6.install @@ -6,4 +6,9 @@ etc: [ doc: [ "lv6-ref-man/lv6-ref-man.pdf" -] \ No newline at end of file +] + +bin: [ + "utils/lv6" + "utils/lustrequiv" +] diff --git a/lv6-ref-man/lv6-ref-man.pdf b/lv6-ref-man/lv6-ref-man.pdf index 40bbb39dc9e046391c145ca85948874871165a56..257468bad6c412ace3d0b5f91ba69184c6718b3d 100644 GIT binary patch delta 3692 zcmah~X*kqx_n#euVQi5xgc(bOv1c2yWtW|3?26Dr628L-LuE<GItr1}2$8L^McQPY zl9GMj`Gx4I=l{R1=f(5ld2!BlKIh!$x<B{1&bbeHiZ_0WHw~Y?CJ&JX!qP0wI~BPT zRuA~EShRIo^lx=Mq|2rx2dq87z77s#ALGkC(FKGw&Kq?OXcet?+=^F73(e~Rw!YxA z)$c=aMuo?rFW@R>G)Iyo(w(2gwe~t_q~xs7n-%Mr!ZUK8vtG^E7UjL5hB<{iWw|VM zw4bX<PePIR<lCX-@$z^jKr{5Ak*x!|I#1y8r7PC%qF<A5xp%hn?w)iu;)xbDxyC%1 z8m)tx^1f`+F>4Su>m)rV{?&&ZDA7yv?|IAoz<zL2%*b%qqE&Rvp;y%`TvE@ZS-SR) z_iDfC&9fKo_$FP#{o0-RfY%$MxLP26gMF@Cz3l6G@vjx)bpc7BSb`HR!G8tvN1*kV zVA%D3Hf4g6l8TC^3L*RB0PN_0VEx7b%z*ohzNWF^DRosNH8o>pRYe1Wfq{~$v7w== zhQ6wjnx=uFu9)`!JmQX2u<#A`zZxK>tgNnbS1Cd|yJ`x?2{5UXsveWLOTV;U@QzY> zyRDkL+$L~~8vCen9s~QN<j4B8<*Wf{4zc3a+CDS517Ahy<{4QeU%YV(<X)D*pchqO zkGuymx~LyelC^6kx-tFX<v*`Rcl~DGg=P7EHn}Nx+$ZCW*`C7NBkV5o$;a?C;*wxB zPcCw2rkh$_57;1klM3)<dZQpU9xd}*%13(J@LosQ@4LJ*s)5+^G#M`8-@hlBH<ngF zs)bc58IE46omB%*5UQQw=qBSDfkE`5RQNqVodB`$Bqo3EC{dzX$t(N3TCAT}BGvuD zXNW7+lDEmUhBL^znoecHbC+opXI%BBikAM7>PRnOHedy$MHLZyVO%4;Bp!Y{r}Q&4 z`R3NMTTGYS7Ls~(bmxb@CFnutOj1FaCTNFS%Xo?JeG4g#DdQz|9u@29^@v(Pd&#vV zRi^1$stG}H4`815X|o#Jy*qy=>pT|X-D#F2{|UpANDV`4S#7fBh`q>WD&^iKB{R`p zDJsCDHV&oeJMdhSHaR8ppu!nU&Y$PxsBMoMd8sG8?;m6@)si-B(bKv2ZHiFM+36Rs z0IlM2lPIe%R+yDkdjE;fGP-(x=-yYE&MmZxj6d}vUQOSQx6wE#KS#H<H?%OPF+8U% zxiheSlsaE&$9A{i^(tP?*bY8p8!f67y$r~{+Ces&7dBpTEG@9QF(`j$fOpGW?XY;~ z$};onZ2n<hijVK_K9L0FN%K4LnmU>zg%-cx*ZuAfys})kH5A28OPp~79}u2_w_Z1+ z`dBs*#E)-<!3Xjoh^^<%{C)Ks%Vg}mYoI;bZ}2&tT`OYI8???Nrzzizi*lcuzQciJ z?Z+!j=$0n}+&kL=`m}ifYT1N>DmHByTJNua)^zDPZEf}K@}Ao_F4JqRZqIuOEi16> z!IVF2Of~T{b{P&Wm5E|!b>Ci!6c~Ivi>o}yT5(T%vYFC&Gf-1Ur8_^$<#}0l7)$%K zzeXF1_Rw0L$yQ65KdwKXUzPXJ<pV&<RBoRR%vdfTwsTJlTACC#Nz1R+Fe&<l@Gd~D zIY}=5=2h;<G!R+!F)#J>dH?M6PRpaKAwo=$tbT>hm5=jxZqqP95Po9!j;sy4ntAv} zUgVl%l`X0A=pa<2A&*$#b40H-`y$a~Re&~G^Ubx!XGE_!u@<~+q7zhC(*^w09%>uL zz6b}so{-TgF@LTV^Z3;=;!o!>*^@KIT%O(7XMp-@IAT2&AqZSk)9KVvmK_R(gvLN? z#>qbayn57q`|>HH7q8pUieP*jUk=!$?Ghc9)rNG2OEFG|BJ&ac3>Q+{Q4N+46!vlP z2G|M8@p0J(L={wZ0^iUDV7hczz>>0=AgCD_3)5!J{dt{Ew3{8$e1rXEV@*bbh1&i8 zXbH%bD6#$6`#NH#BweluZqq2S^<t{+0-i+vX9Rqz=2fquYWpyMs0#ro@;Kwa6i(Yz zX@wOOtc%U%TTD<sbPA$P%@`CiOKfLi3~>kgnX3Vf_;Vqk%_^yz_LH0g=Iy`)q%Z9| zZF$(>XhwqYM1~+SHdJt2|8EwUt6hbdK<3cz=9#hi*tvB7<S%$AHXr(qR9Mkp1n0nF z)ggF95R%D9mm%3P%E*@BJct_n0ImlAFXvx}%Kp1fqg$-!8NmK}#~!Lrj^xaslRbY3 zbo&yC;C~lmv-VNax>Oq*UG}rvjV=FsBxNS#F~iY@^8!)69J);d2SIPs*i<M2eaJ72 z@IKT@qSPEji(%Er86JzJO}i=dJ$T9$P@x8@C62P!$_YdAi0~ZPbcPP_OgGE%yld8Z zk#KGsAex^Ge4%PWgVryL1-~<ify+^FUW2AxaJuP|2Ca4@x9~jirNba)pn2P?&f}Lf zZASKtHvdNoKk>G`HhVv2yZ=<=8XK|LUK={h&<quFe&ew?G<gEFTsguB3x$4#MT~2F zxL9((?16e=AKq2NC$wk0m+Tl!5l^X%WJR)S@P$f`+c1i=D;Hp*Ku@}a$({VB%!k)n z%SO656NORg7`s}jN)#6ctDzklEna2^#LA)^FuP%687)Bl3WFyRhcd^+H5~g;51MJi zD9JzRHkAFc?eCiE9Y0_eS>z+C^HeLe<9yd`Csg`ZRt7%NGT5VJ8LQ)58K|QZ_Gb@Q z95k;mFppGKu^NtYms|@alC<OrKObXFcE)6g8Dq(&>vtQW5|~zv+R%U>^f$*cIxyGR zXvrPWYqma5&H^{!v}Et{bF*E>;fA-8oF{^*@1pd*ZwaH##j`pI=}jJeBH7OtVdB}0 zMHm7wj7@_4jTkmY%N^0&CVvA58@|5X(}2DtO$avhN$TNV$4!`bW=Eu5RUX`bNJ7vB zx9vzg0sj6!rj*19j}1$xd%0=HSD=!*89$Ra&_d#m4fkRsv(wKS^Cd}h3lYSrsgk-_ zXp#_GnXuLwlWv~6SmSAD*xq9>TJvQch)g=sxQ1IelhP)!07=O=ad(`*t$evFg>-gm z7}zRF;<JWsQRjH&iA71ewzJwTl69FQM_zAy2^6A>&P`4_7?$*e@+wfHW^7v!lQxD8 z5h*w!Wvk|68=qHwRQMa;i3nWxIh|KZ;|PKoPkr+b>qgMo?8)+CzQ0?Y!a{HW6Zu$Q zq?~7W<5gG)XE~gcBpd*<qzToM9s3Y3DB*qJlln)P;PAL$I{Ow`d=B2EFFMBpC2=v? z5pCRph<!$kA_PUIkoYi=0TKcOuOXq{QQ&meJF$}_HaQAE9ce|rJI>cPy)8sbxxju^ zCK`nSZ;O9#c)A+GG4}x2gEX+7h<!VbY(Q4UE{-D_*qp`lIOu&!C8KNi8FY+VDOo`& z;mzwHm>ZFw^x5k%SoD#_pLvV=N9o^O`KrqPkF4_(!C{#MT=G2Z$vlTL)syP)yd<O> zejm#qjBG)McM_g~6Fz$QftJAbiGJLQK#nKvWj+kJC1&hfz`eVox4nM%$;aQ0^>Z2t zCw%5C5`ul_NC{PbKZE_|CK40`6Fzk-qJ)ekANu=c5^gyqq`y^65Yn|1YE2i?O%uec z*d5#G%=E~pxLEMa&5zBdQ7~Ds23fw%;ZRh3s2o*Cu&+({GHf$_biw`9bYOWbrv#<= zgqnR%Py&}sf^Y1PO{!-LDaVQ<khSAN`*`fMhaA>fn;t=0XH3L)K~q=+xPmlE^1;VJ zAN{VYrHBdW%f&gvs{a#r)S(F~XZkvdxbj_}ITxv*Dh}Lms<-KVkcq2&VKvoNw1~ny z&t|N^F#OSSd(K<cbKdE%Gx*FSm(qHUhb-c<S65(S*@r7Igm9^DT{EZogQd8hMc|Y9 z!rL~^6k!2%xnSq7^lZ^p7(cKutM--N;CZRTE53`hl5m!HckxQ(CHLS5H%-{BW1{gJ zAGDUXohP;@g|Z^#)*GGMcv5j#bM3z%uarKIifO94!uJ;m{upRpTR9%-XUw09F0}1> zNHzhdT4M8>PbB6U9scwDFmCC_^VQSkA^f}Jr^kvNWC#&HYdyetdYc5r1d(c5*w*8H zca?iL)DlQRV}*W^`Fbl=6XHGe6#Tqm!rVlSOKiq+PZ#@17w;Gtj8WLO^~?iIyZMh+ z^5)`sbNzW;3oQc<!VE^e*+$Qq1pwN`lTvI2)>2nna_BXL;v1*hs|w=_597T|3|1rB zSEl1zn|SulnF4|lI-Vik?c>Yw#rr%7-z}IQU5t%+Q17HLQ&uJ~i$Cc}VfLcinH_AC zsd!AQ#E%|Ogr4Wb)A%={c#DH$o_mz|`~Ez44o`UQSVl)3G~8lYjG$M2Uk#(iu`EuX z$+<xg(f%FP4pFcD`90oy6^8+|Jm=Nf-f~GkiPG}C*97RT-;2NdwXY(P$LhEAk9QJm z{(9M@)uF|Sp~k~)eLWrT*~XY1FILwP>%g8m4~d&~=N1$$l!pG+X>^df+1*;=wtePj zS776i*v+2_!58mlScyar3ztp}7>!-X$PkS(tIsW+sz_a>8JS%cc{c3URck%xn3pqp zZbbe-usfg{r~>v#wa%jan+s0LhX(e@UIv1W&ZJn<Aog+ZN$lkiH+|J|a2*XbNI}p! zRpRh{9InLU0nkx>tvOHujeQBErLWF}M-tInabq;DEee><vIM7)SUD)sBt1be3qxNK ziHcQHM4>1WB#1?vj3TEW!&Z@fhN0~Y+QT|&AJh~a76kwQ_mZ?bX}C}a0Gj)H8^!xG S*(2+)W2~x39L~tv82K+W7@J4{ delta 3699 zcmai0c{CJi|DVk^SsG&vVXTFWZLCvc4P}VPZcMH%G=zj{jOp6<ozSRjDHVh4GMK_8 zO^8t>uAPvrQh43>{?2*N`MrO<e|*n#KFjxezR!8i^E}^sbMTlsc!oR>m9M4>I!ns1 zzQn+AzuGtu(8YF%Ds0z0yXa{zB>1i?IWl2tOsG{Qv{j(9<Jm}ZUujnR#ZT!b-NNS0 zR&#}sU$O_p9$_qIit9e#z*Iy0*&H4+P1z3tHwU%t|IE!@I~1r;dsQ5`U7ft!@}#=z z+q^g0hV<~<!RAj7$f>eaJEho1{9}6lpB<8)DkAXOL!-TK&{|)z@<hX7zbioJ`2{U@ zh~oP_3kHqz%qs~!5@8QCa;+T8aOzhCgqj->w^2s!agjyKZ-HkJb^hF6m>%V>kGw8I z?HI|5?U$5tXKjNA^G}a|C)G^;nB(X-b*j()$^oZff$>=2-vK%fa1#~?xiieAuCA_z zLaJ$L<}*hir~U(*wnrdFCv7zhbu_fK)O3x^%rrHSW@=`-#+sVO8k$CC>N-Y9l;(LU zga2u9gQ{NsEyyR-S4u-eTP+*Np_pGY2jL;<BuZ@j%wrwGKPG<BN&Jfu)h_E^huxc^ zBBV`VH<GDTsN#Kg>38`cHbKZ)ezt|OtIQ`-f0PNEoCt)e<Ux0USGb&Wg}72J3paM8 zJ=Tk(j@n9Y4h_2cIOTP?_0<{47e4*ts4n_(M(*=dco3A423IP3jJtU^RwU{~IW>jE z62<S=Tj4Zlw-`FN%ESYt!&@>6Q^Se`aY{5LM$pJ4dt;?b(YcdtruF<+Vb${C*$ccj zR!{R;JVjd6JQjeqs=10m(|Q=s-vt0t8Lt!F$|oR2i4t<*zk8qXl|vb?slP!nOYxp3 zXqPngF$%P2jB~?lpee>mf*Z93PFh2RXRz)Rp{d6e@p;~oibBJk>i9+9b@r%)FACv# z-WNoqP}XbQZwzbmS;6>9zjd%N0}IzTy(N-zQr~z@_RRq<r(nT1bpc4oI9_uXq>*`e z?5zf)ZKQ~TgHb@?0*sL3s7-@wD$r$VL`K?3F=&J#pP=%t7+B9B?dS^m4Uw-ilxb{5 z+c+{S4F6%2lAkbz2v4bSSDZ4GUO8BPyd!@tArOJOWG6{TW!=F?itUGBVI$&JBcsCi z-QD_2j4n$WW{0G)Q21<3t+K^L3F(UT8g*CMisusLj}c!#1nR31!_IovjeJKlUi&?v z8$8)isHkz9A9p7i-tM=%J#_ZPh+n$%q7J$%#_Qsz;k(Zz?ynb*kZxr@UE65wA$Ujk zXCf;V7C&S!ced<#L<T<Z$a`6IlVgY34rQut`(thn-T)GjH5@zb?J(x_mN!Oqzy(ND zI(AgG!<p$@L70vH+ra(HX-m2t2-R%mDTGT0weQhN8mR*#>CH)vJ`XyHmSkHhk%X9+ zqys<s4Gj$S8(||uw(>@%w}6<|ZFE+k%KKGph((9a%ejP{>-h63PV?1~oZa)iI@q_d zkw0R+v^>T-lC#2yu1y4$%J_wX>>Bg2os@M<^Dkuu7FWamPK+Byzu+Z5WN5inw`gAA zQ86^1^dLXLC%1GZ%j>U=NuAia(OGfgmdmJ~%I3JNSVU>2r*m1_ZCd%TjnlSR7V%4b zYZG?>$i?un*LM1H+8e5P08kKfBTB9c_)%7WR}S5rbVGpk0k{$)v@UO>G%<e${T%4K z8w7NIusc>H*Vghpz5)2<A~7JW)|6Pf?sY?z<f0FJ5#h|YoVSL)Fg(2%Glk=0aU^9; zIaNpf?2=;Eb5mdh0Jp^+%?urML4+-y&acCpMy6y<{cJt0{hCK`LJuTQmn{H|;DiRr zaGdDV82egwY^>d9O&#!1>@9li_GeHt=Q;AgXJ|9@IeGOndo$N)!be<*T2d4*$eeUl z5y+kcGT@9jsrmH;F0&%7dOM3aqk;ySLA*FW0?Z&OoGD+)YaC{KF;e8O2A>V3zLFX7 z@=rzsG30OB!14(XAF3XGOp9QzPD*#Ty|~6p{Y&#DM55%Y)KbCaSxOp11ZHkYr^Ij^ zrvWj0;0eBFSRCLq#DG)we8zWDOaTzyW8j;)cK_P0yNw*xR0JH~rGp_81U?)7odx9U z=ElUua2wv>x?bgj+vAov<UigIzzq4;=J@SRitkO0Nd(>pq1XbTEP>iHI6HbpjFlmY zZ1rE{zlk^JWrATcMrR}VE>JfBZ%CjxHtrK5LSwq;z#u3UB4Ps-sYGXskf6no8(9Zo zHl#+u0Psgcxhjx8Mym?=g33EeVP|p{VKjV!&!{{N6kaA*D@L2e6;3|QJh2~xoel?= zH0**)p74N5s9(T(Dq`#|7`6h?d=~o9f~Z_lzT9wm(K8-UUo-1TFD6w-K#(J6v4Gby zolpn5y4r&IE7Mw&H3-gsUJI=ev+Qt%5Bt}coqgn2U3zhK-`wK}*i+E4>6TRL73=95 zjt7v-IY~ZUcL+dNHix>!>HZBlDslJtkb}q{0es@Ux^cVsQ%UZ>N>T5+r76bj*VscB zP_lImPvWUD#=!Xe_7#X2$%bC`HvpxH>xRtrwOrDToUe~`n<O;P5PH;1qUu&Q=`-XW z@VF{oZ&$c#*5*~F$GFUdnB;p2$JttjXQJ^*?ZF>HU7!Mm3ixVpW>WY;;ZUzy_wwb) zPOqC69_kZ%mQ%!P#1SoEz<qI43tMJm+YYY8ZFRX&xJ@*(2*<a=I~c52`5GKAhpk-X zoE=KwMpyS{5^tZ%@M=118=b#S=Zsh7RS|dA2?$A;L-x7>t7bRpZbG8dPdhu<ZC+hj z(T<>HO2A|gdCg&&6Y0JwtuUG_-a;AvV>7!IoZqwxksvWr6U1QJh#-^61jUnAr0^Du zEc2%Hc|_&Lh(0~ld@5lyHNiNu6_zQDFlOW@sKPvErH8E^f4hYfsukHC!9jg}d}ij< z5VrP+VH2WNpWrtzzobR9Nn8Rq%pO6!kTqa_P6lcskdTvNJ}Z-$-V4N=F;WCdb)-V( zrHLp~K$5wLlW&xRzB}JLQ{k5;ZvIyc9-gc1yEFP*?kAmGC3p6VCS%j1*$7($FjL{7 zbpwEi*f){b-pLv)Z-0r*8+We+KEg;!)*uk3e_FL8wqA1Vo*FGnAOx4liOOKx<+cuM zyfg({2PI%XUULQJ#j4keieyHeelKyKE@T5FHBxd8tkKm`O|fTd!K1O3nbw^ZQPqY# zRUAB2m?qhq334_R^W~7B!b8bHweU3%nku|QMzDDHV(uaV>|O4)eB5MDBxsLvg#ZwT z#M4D|xV`Dh1>jz~fg>Op$0g38Kv#DJR^xbzA(eDL>cDC}M)<wZlI=dI01!q(c(l7r zPwOyEcjXA8uE1+uS_FwnfOeM(L9EsUC5kJ%Zr(JbLH5)QumpPGxhbg=+>I1Vdflrv zKy<OX7FB3-s`uZQub{c;pJs71ykn(Eo?^v`+6s*n**LjUPnyqn)^GcO0oQu5+D7eY z9%S^MIt8bS3-=|(0se{?1r`mQ!LX^FUHzl)+R@|m2VTTq*IG?`)k39>ebhshj5#zy zwR&!A7z=AhcOkDz8cV2Om3`z>VJW(jTNWbfUofMQJ0n&&15WhBXb2*v9}HhoZwTBB z8&C#UoQtzaaRLwSa@U{l`So`5{h!E3T7!W+^{ze9<H&6-(jb{9w+pF?8qDC4wB;TE z^(?}BBD;{qB4a1x-rws24|F&h)JEXG(r3x9z{wm!e9EU;A#~?S2SDkYtpFiI<yc1u zjT8SL{b?lKYY?eYzrxJwvpy{UW~;K*bS>;exw55Go&OEf(*449x^(h+A)@lW;|?vq zZ5<*G_fxi@{n5*t{A=d74%vSS=C7?oq)3C-DmQzw6x$THx|1U<h`P<5!9BBauXvKh zgtV1|94Bl4A8{}l_m7fNE8=M%Cx%c(R|t>K%R5IjY|f4QAZmV5I!<3|ziZILpDyPv ztmHULV_Z+{JqCC03p7r4-P8_E={`oMWui|ByZ<D0lomdjRqM91H-JV6Y_jHP{i`9( zPIH}amsI;+D*P<Hx9^atEjcEkr)0{W&V5?cKs~~1v+pyk-!8=f^#hxE<QKmwGLzZG zXIa*6dEI<zcN;Ii(BHP}X#&-ERzGu<Pj1xpa@9e!(UdiO<*1nHn9I~GWE$i%w|tFO zRryIDUgk0n+wP^s^Xri^n7igi-)i9D_Od%UayxtSJG%-3`uySP3TsZ-r6ZeedNvn@ zWXT%OK!)D#-b8cBsLG{;<bfY?aV)}lgDbC3GFg&v-XoOfFY-MZK6&vD8BaXmm%itg zDwo}~MZsM?&xO=`6Osyp2l6wlOZ(sVgGr)%s7;)4=kzK+8z1V=a^w*~FJfkqD|wPR zOyW=LEG5j&-<$W4e>$08yTU)#{4@KTeDQ1?cKQKfp^eMuSYHQo?PW*0wSQoCo?oi; zS({|Ob<d&l95lqaioLhhIl6cF&<y(RQ@P6v+wXe{q19NZwLzuJu5E(qk^?1&6zaD- z;hU57ZEx8jJICOA(3F2(*2PaP6rnTyFWdtgl9mgY&roWTN5w(Qy*f``#T_nF{Ap_P z3oUQGe*Io0kV8Hm;uSfLzd9DQk^F_qf0ZmjJvAERY{Ri)2=;|oQAHbK9GL7M3^|q{ zZd9=~NE?Q4iH%6*45y%}lH67?hPA?LU}Ky}O3VRHKpeo)C5>d~r34co;%smn|7Eft z671b2uEW021#*P!Uo$wUFF7m;`oDoE=}tIe_e1`J{zE=~pPyFwAHPDRIW?hja;Da1 G(0>8;(4O4@ diff --git a/src/lv6version.ml b/src/lv6version.ml index 93bef373..5fb61029 100644 --- a/src/lv6version.ml +++ b/src/lv6version.ml @@ -1,7 +1,7 @@ (** Automatically generated from Makefile *) let tool = "lus2lic" let branch = "master" -let commit = "732" -let sha_1 = "33d4cd49003dd0b3d3b21eca09e86d8ef25ec0c2" +let commit = "733" +let sha_1 = "8fd1d262784f8a40fdde9b9fdb1345b4fad850c0" let str = (branch ^ "." ^ commit ^ " (" ^ sha_1 ^ ")") let maintainer = "erwan.jahier@univ-grenoble-alpes.fr" diff --git a/src/main.ml b/src/main.ml index e40244ae..6a3923fa 100644 --- a/src/main.ml +++ b/src/main.ml @@ -1,4 +1,4 @@ -(* Time-stamp: <modified the 22/02/2018 (at 15:50) by Erwan Jahier> *) +(* Time-stamp: <modified the 21/03/2018 (at 14:18) by Erwan Jahier> *) open Lv6Verbose open AstV6 @@ -73,11 +73,6 @@ let (gen_rif_interface : LicPrg.t -> Lv6Id.idref option -> Lv6MainArgs.t -> unit output_string opt.oc ("#outputs "^ (String.concat " " outvars_str) ^"\n"); flush opt.oc -(* make sur f is fresh *) -let fresh f = - if not (Sys.file_exists f) then f else - Filename.temp_file ~temp_dir:Filename.current_dir_name "_" f - (* Generates a lutin env and a lustre oracle for the node *) let (gen_autotest_files : LicPrg.t -> Lv6Id.idref option -> Lv6MainArgs.t -> unit) = @@ -135,7 +130,7 @@ let (gen_autotest_files : LicPrg.t -> Lv6Id.idref option -> Lv6MainArgs.t -> uni let invars_str = List.map (fun (n,t) -> n^":"^(my_type_to_string true t)) invars in let outvars_str = List.map (fun (n,t) -> n^":"^(my_type_to_string false t)) outvars in let name = main_node.Lv6Id.id_id in - let lutin_file_name = fresh ("_"^name^"_env.lut") in + let lutin_file_name = ("_"^name^"_env.lut") in let oc = open_out lutin_file_name in LicDump.dump_entete oc; output_string oc ("node " ^ (name) ^ "_env("^ (String.concat ";" outvars_str) ^ @@ -144,7 +139,7 @@ let (gen_autotest_files : LicPrg.t -> Lv6Id.idref option -> Lv6MainArgs.t -> uni flush oc; close_out oc; output_string stdout (lutin_file_name ^" generated.\n"); - let oracle_file_name = fresh ("_"^name^"_oracle.lus") in + let oracle_file_name = ("_"^name^"_oracle.lus") in let oc = open_out oracle_file_name in let invars,outvars=soc.Soc.profile in let locals = List.map (fun (n,t) -> n^"_bis",t) outvars in diff --git a/utils/lustrequiv b/utils/lustrequiv index 78eba3e5..048ce8fa 100755 --- a/utils/lustrequiv +++ b/utils/lustrequiv @@ -1,5 +1,7 @@ #!/bin/sh -# compares with lesar and lurette the behavior of 2 lustre programs +# +# compares with lesar the semantics of 2 lustre programs +# using lesar and lurette. EXPECTED_ARGS=4 @@ -8,7 +10,8 @@ if [ $# -ne $EXPECTED_ARGS ] then echo "usage: $0 lustrefile1 node1 lustrefile2 node2 - Uses lurette and lesar to state if node1 and node2 are equivalent or not. + Launch Lurette to check if node1 and node2 are not equivalent. + Launch Lesar to check if node1 and node2 are equivalent. " else file1=$1 @@ -17,11 +20,13 @@ else node2=$4 oracle_node=${node1}_oracle oracle_file=_${oracle_node}.lus + riffile=${node1}"_equal_"${node2}.rif env=_${node1}_env.lut + oracle_ec=${node1}_oracle_prog.ec - echo " Are nodes $node1@$file1 and $node2@$file2 equivalent?" + echo " Are nodes $node1@$file1 and $node2@$file2 different?" echo " let's check it with lurette... " - set -x #echo on + # set -x #echo on if lus2lic $file1 -n $node1 --gen-autotest -np; @@ -39,12 +44,10 @@ else echo "node P1 = ${node1}" >> $oracle_file; echo "node P2 = ${node2}" >> $oracle_file; - lurette -p 6 -l 100 \ + lurette -l 100 -o $ {riffile} \ -sut "lus2lic $file2 -n $node2" \ -env "lutin -seed 42 $env" \ -oracle "lus2lic $oracle_file -n $oracle_node" -# ./lurettetop_exe -p 6 -seed 42 -rp "sut:v6:$file2:$node2" -rp "env:lutin:$env" \ -# -rp "oracle:v6:$oracle_file:$oracle_node" -go -l 100 -ns2c --stop-on-oracle-error; set - #echo off if [ $? -eq 0 ] # Test du code de sortie de la commande "lurette". @@ -53,7 +56,7 @@ else echo " let's check it with lesar... " else if [ $? -eq 1 ] then - echo " ===> nodes $node1@$file1 and $node2@$file2 _ARE NOT_ equivalent (cf lurette.rif)" + echo " ===> nodes $node1@$file1 and $node2@$file2 _ARE NOT_ equivalent (cf ${riffile}" exit else echo " A pb occured in lurettop (exit $?)" @@ -61,8 +64,8 @@ else fi fi set -x #echo on - lus2lic -ec ${oracle_file} -n ${node1}_oracle_prog -o ${node1}_oracle_prog.ec - ecverif ${node1}_oracle_prog.ec + lus2lic -ec ${oracle_file} -n ${node1}_oracle_prog -o ${oracle_ec} + ecverif ${oracle_ec} set - #echo off if [ $? -eq 0 ] # Test du code de sortie de la commande "lurette". @@ -73,6 +76,9 @@ else echo " ===> nodes $node1@$file1 and $node2@$file2 _seems_ to differ" fi - + echo "rm ${env} ${oracle_file} ${riffile} ${oracle_ec}" > lustrequiv-clean-me + echo "rm *.cm* *.o luretteSession* *.log " >> lustrequiv-clean-me + echo "rm lurette.cov my-rdbg-tuning.ml lustrequiv-clean-me" >> lustrequiv-clean-me + echo "To clean up this mess, consider doing a \n\t sh lustrequiv-clean-me" exit 0 fi \ No newline at end of file diff --git a/utils/lv6 b/utils/lv6 new file mode 100755 index 00000000..ee4bb58a --- /dev/null +++ b/utils/lv6 @@ -0,0 +1 @@ +lus2lic $@ -- GitLab