From 3a84988b75c72c628e56f0d6a6246a1a4b3479f9 Mon Sep 17 00:00:00 2001 From: Daniel Kroening Date: Sun, 7 Oct 2018 20:53:07 +0100 Subject: [PATCH] remove two fields from goto-binary function format This removes the name of the function in every instruction (it's known from the function that's being read), and an unused field. This also increases version number of goto binary format to 5. --- .../ansi-c/arch_flags_mcpu_bad/object.intel | Bin 4335 -> 3778 bytes .../ansi-c/arch_flags_mcpu_good/object.arm | Bin 4062 -> 3704 bytes .../ansi-c/arch_flags_mthumb_bad/object.intel | Bin 4456 -> 3780 bytes .../ansi-c/arch_flags_mthumb_good/object.arm | Bin 4120 -> 3725 bytes regression/goto-diff/syntactic-diff1/a.gb | Bin 5738 -> 0 bytes regression/goto-diff/syntactic-diff1/b.gb | Bin 5830 -> 0 bytes .../goto-diff/syntactic-diff1/test.desc | 4 ++-- src/goto-programs/read_bin_goto_object.cpp | 11 +++++------ src/goto-programs/write_goto_binary.cpp | 17 +++++++---------- src/goto-programs/write_goto_binary.h | 2 +- 10 files changed, 15 insertions(+), 19 deletions(-) delete mode 100644 regression/goto-diff/syntactic-diff1/a.gb delete mode 100644 regression/goto-diff/syntactic-diff1/b.gb diff --git a/regression/ansi-c/arch_flags_mcpu_bad/object.intel b/regression/ansi-c/arch_flags_mcpu_bad/object.intel index 0ddb17184a5f40df69373225165716361ffdeb00..2ba432c93b368d71d39d3e3a6816782f6c234d46 100644 GIT binary patch literal 3778 zcmZ{n{c{y(6~~|FZk~nOcq>s6g9tUTwYACRh5%`W;teg;iVLzWwZ^*LyZ1@%mV0+E z`$7_0DOg*PrYMvu6>IG;{R5nF+B&1-jJ&_eYd{>*sE8m$iujA;IQ5)8dvBIH%S_1J z?B37$p6_#>bDrnfhkBQZcGhaSCCRjGo9~96C5?(}nSt#(j5DT9>$fYCWzMPeu+xIS zwNz|JGUYd!JbZY&Y0&l7*v^1avOQ@9t~bn@PKjLEt;!stD!GF8NG>qLz_-dy&MH=| zjsZI;hs93#mGk6)Cw(8{_;5>XG+EZ<%)*(Z7vFVDco)8O$ZU#fdmabY!M!wT!nN+?IN0s{wPqzuXtP0^d)Qmv&duU z+fSv1s>&)e=mI|?;rAR%qt}JgE*evh0s0uCbA+Bt==|SBo_0KxW})l%YEK)*`_foN*R3?f?E}_6WPOoX1!DF7K}^=@{7773ZyK=P zH5$;p0Nsnwr38I|pb!3A!09xqbV|1AIMDcDFP#SBX&^3}THj#Q{;_>M zv^7)zBTTSH1N+iU?1q-<2TcDm>3A4)eC4#DUfhArxKy%n;86#zFEDL)On zhq149J8mG?hGvE7tB9-<`Oerqg6fY%4-2!P-LBNKI@7NwB2>)^jA86bjvRzmi$h^d zy$-RigX-Cj5_mN&&SU=+`N?{u#aVqaZE?&Bbh)a8c{iq>gta*dYxDJ@4jLXOovozP z`o>jmJN>p}2g9Io20mwf8OMesAHR^$N^bau9D?D9=3W4q7f|LmN#+wI^IK;`qRB-i z^u(Stm2f_3H2OWDau299rfS(INuxp zj#J?fe0+!F42{Pov(BU?G#P<>2~xWxSl8?tdA^oXTM^e>dt~?818M5~vg^SRbb>}BH~>-)fK(54 z*5|rEGO3l$8hrsN?TrGROGv99SAa@IWQ6#YG4&isJqP6xN`2j8S*>AtWd{k9C%tfr zz`sRDkReDY)C$9gx%TMt<#0|Iypo7g!Y%C3Rd2Fa^Y!mp)+=Yw#L(E z(_Fv+xaZbO&js39u;46M@Ql>Iy;#d`Ac^tFBZ(U#iO)i`XFwv`aQS9wxQR{L6qiBT zWt6s&leSHq#KqgKK&^TcKbWR2YLN9V*;uE8Ao3uH6yJ%t&mk8YSv_fLH_!2n39jdc z(4wK=R`C`wrfvktMwRu<{%#C;J{A}6vqEQ7KhN{s3CK;S!DQ*|2HI|r^a7Xq_c%DW zIhOQTa&?R=Zs)o2m%p;A+}a<+|cPgqj3 zYZ4CiVN~ba!G`T%gVFbLjJZ3~dhP!O#V6WpAm?`q?e#Bo^=QWOS6a2@R zJwAL>*$J0D*7pkEk&uA>+J+tvSB5cl2T0ffmmiLoBIQ-ys{bU;Y!}iqT8pC1=now$ zx;p+8Zcp_Q-xDpkro6@%!%p1AwIy&z3S=}le#Q;D)j{-Kyt(gv_;(u!*~R(mh+nA{ Ye$Ic%0}t*Xj73j5$H%w44!_y|0Cq%U$^ZZW literal 4335 zcmbtY{dW{s8NPQH%FY%Ci;5UjViViiHcd7uDYZ!3jPy$!8b+`m+F>$tH<@O4W|^5K z34SyQX_5s(2w&PlzhY}^{Z+(M>(L&6^#}h2{Y^dtp#&PRK6mbHcD6kme<0_;Ih&b% zp67ku_rC9Y^U~uTk1c5=b*5`EqF$sP3yPkj2LlC0=rZ5#c9_+*i>N1PpKS#_BrzYtbNxn8gBbnBMwF*9(z0h0PS z)!gIeS#z)FG6&C^3!dBUHJe>|v#Hw-nmyL-G2aJ#v*Gx5li6%|W{;lD8Qs2~Hw#6* z%djAaNUx_&H(vlfKHf5x?lL@5ie!+n^mJ0e|D-;hEw~7hc|^N)87x^oCap&>|4uZR zuHy#=;$I49zA%z7dw>A>C#ZZm)qX#Zcm)Fd;(w$KT}3+=*iI9dVh0GN=&>e0@Sxw{ z$Rob(H7NsFgq$K|!}E**qOA%g zay>+~e0w(|UsYl+ujY?sJpS6jasqQM{Ef2MvCGI68L9hJYPp%8Oor#1s2yuArTW*m z>ya1AhqNIl7?u+4>x!COt#*9lmGsR}@$Yh~#Cp<0E9n4N2FPr?+m|zGlQ$&NvX&c?KsI>}lcXM^sM_(Z_ZK%H!$}qScAi~zWy3Kk(;nqc`3r66 zGJHlFN2Cl_cKduSC3%)dLF;aTd4^-@VX{i;c?g^5!oDq}+_7hIDPjDIe5a6d*C8o` z!VAj?QX0vfS8LJt@p9Dz-S+h&&Iv#B@Z~D#uX6hD2>QD}T7(`pMD+Iv`g;#Z88nIt z{XJLyAHC=>rSugLU*W_}g806VYZ41uk%DGH+_GQdHCG{SzFdnqtar;TcIB8}Ccg~w z%bYwT$Xowjle{Hj=lO3F7ny z+ng%539%Y1N5lN#M56ply*&Lab%xqb)^_Y*06lrNB5#3&r>~^M5NzU8(6Vek|HbHQ z533VWw~)?+W9JCjvNxtpv`J{$3oUyk(z?~uv?bhXWZC-B3=KK9aSnCm_LrpxqT~Z` z8|mCO8iNXYJZ4zF&iXNfdAAz{padE*Rw<0)y{RDWc5M22NzLEHUO%mC49wj*k5eseGPv?wCuJ(sLYyw~t0Q0k20I;F}yZ5tTMY0QEJ_jpK#=!Dns1>+L zz)b?KFRR@eR;b)Bf*p86%9N)M+5G|4epavj{5X!-FHEdf)-QpMo$aNeo7>qk;bw&W zaFEWXu#UfZK z@liS*L-yPvss<}~o?pgF>1kk1qsG^cM_8!DQY3PWR!~ZGxRyP<+WA_yn|Uq}hhfw( zjMDbfb&eabokb%@w0#w+`y;7$RnWDG@?*4cO_A}+etI}2JE|zKIIIs#HNSk6(uX1b zFpM}rc^gWgtxVF%O6L=|jDvKIHdTgKA zI$Vrj;i#`hsK@CarMB{t$#1+TC@)()?tGP=iXrmRXJd-u@>NQo0^li$)V~&4B5oR! z_|oeU?uf|he5@~*Z){kL#30p++&kP3(4FT~DB(9E1F==S$#GD^QLpD)|C{u5Oixwu z#uu&A&~}>FEx-CE-=cNebOiewI=<);#}XWF7jJX!Wt@9;w&fG+jCbh{@wW$VB(TQPZ`0-PaSfW<@jLn_8hE&l;^$NRtRSS5zd+xk h;xnb>eLyFFPwR*}NNo!{i=DM`Q-4Q5Nq7@E`X5G!zlZ<; diff --git a/regression/ansi-c/arch_flags_mcpu_good/object.arm b/regression/ansi-c/arch_flags_mcpu_good/object.arm index d417b14bad43db553dfc0ccc5d627cbd03752a82..6593905c6b48c9f45b19be6994f3e27a98ffc1b9 100644 GIT binary patch literal 3704 zcmaKv?UNK&6~^zKp_>I^Fl#VzF^XAYjL9<0vV=`!g98a*Bn{F_Rz=h4>At(uVWxZN z?qPQ^3M67A5EQZ+^1%=Jl0U#ID^YoWe@`i+SYnx=h#;&4@rz|y@wt6^W_x3eTeUMa z)7`)GoR@pfnT<;qEm3B%iGefV3cIkLX|MA^#}12(*Oa-PjA`$t+AYrwLemXdYF{dc zuii_yTShos5iGqeMNb+IE;BY^QR7}M9o?Z!1d-#BG}AKefmih{VU#?}3?0v9Drk4~ zJ0-y;{!(2~s5+(4aXU=kDmtOC!m2Mig3x!|f#5OR*;;a3!CF30I_Kci+Y<&oe=V*V zw&UYw&mU%!exqcIURh+Ng;F-J^=3n}8U|L;&02-B)iL0N#cE+T-m<90-iERjC>So@c`;Ex+C@RRv3Fzu@f!GZ1X@pOhRVF!dePFcz;|wc_a~ zRvAgvhPHb7a>EIX4Z`{zd7A(RWiR zL@l#9Wfe_ds>n=3tR`x$AN`M#dnEFIlFSxocf7?-+m^lDoq=ikf;F{L_;EdE!4v{D-cWL~k&xt;NOJCY zGj3fnHKCe%9MIzuI+vhb1f3k?=KVzNlFdMdxa(*$sO?n?C1KQ=N5MQQnGX|lJ~6xh zsx;13o^;MX(hM1(@g$H(fIK3Rj}Y=vLQWm$^`nQI(c)&%P{N6>`_n?Zx3=cAqyz=HrDl)x_% zFi*fme^ll*l0G$}<_|QZM#WUm&H(@qNZ?`uK2E>~Vui$de19`m!ShNDZ})?>U$UMc z))HbZ{k<|)>6Gau`=odz{8c<|W?M)=Yl`AF%6)-(>eAd+v^Ucg(>KckBPd{BVcN-*D3zQ_-~=qi z*s7l@mRGJ|Fk=9&IIm)8z}$H_eqLoW^@83zLB<*U%xdY9*4jg6tfy~q$L)7qCmhB| zP~>&imvSB4yZUm%7jh#o#1JOE^yM;qxeQ;vTF}2%A5C9>c`UGvF}Q{dcE<+4aRc)K zcGkeonyU#5)K@{i3i4Hjb+T_#5}pA7bJX~ol9SsE^(8t@&m8-|Rq&xcat!e}hC+C@ zMa!6^Dvq|Si}!iE%)c%AS>ZxLmu&C`mL(L9wSCM#TA=#O3rbDB0L2#+w*5eAnLR@n zB)gw1)KBVIjr3ni(39nH37AU?>mCq#u}73EG9?*@FmVILmLb23#`bftGoa<705@1`HrD$)9vULsUYsgkf=;aCmSic znJ`_B+^CP)n=pM7rrCN5@*o~VZ4CWG$&IxynuUX>5?048d$2y>mIXH8ntBQfPN61- zsX5RVXR*Ewq-SZQ=VC%neK$i>rDJ1MWhvCui;#8^(v)wJwC9P?5*IAx|M^V`QNCBj zih{0RmffJHZi1FgD(mk3c9-jgVqMiNG5tG4+eoyB#?jSA3gd`j*t=p7 zYpz@$Yw9h?yCoyHi4$=%r`Wx~f2VwS-f!l66FSEQ4@-Pw>Dddxdl9@BxzNAMk@GE* ziS9B)GO4h(@TjuBC+)t-Wo>QYx08Blp(+V;Ep*<7&fC!W5}4nY%&jrAGs)aa%$Fte zrHHwek0zN^HI0%T1$7kEZM;4NEViA`&|iszu_HF}1HM!39NQ}DhjtrhJNT|dNGeW6 zU`?+^ncsyl>_QmW4`bTSIJ9whiIh${UxZqPu%fgIse`aZzlG@Q*5 e&UZ_EuaCY0ya-jJ%@kkhKpEd!rNivZ-DJY<%sMkm z0>vT`BL+f@7;PIYHNW(n{#;6r+S7XaYk%m!V0eFRAP9J1kNw`cv%9l+Hr;c`NtoHs z_j$X|^W2?J^giBnFKM+rn-T3I^;uZ*T_fC9WP~mVoIaP?*{wu7NCzD|>?f(urRCj( zsGp_VEb&%)e@eV&IBrM?(f*V!n!Z_JA@c*$g#Y+=iskc8F>nIX{AntKcT}Y<@JhbL zjJ#)=q2sya7NXsmbMlNV_(B%XmRb02OWtuAY1Te&8ua`vj@xJ0j?b*n^S2S{iqzTf z6>={#t(I3PLLYzLa$U}vJ}Jj`kn8evTE$PY^wwO_gO|)F`fXAP$Xa+7zA3MUV>78X z%X5R!L@b&SrLXNyS^a>)m4h^;Dhk}Z{WJODY{|)oj@!WvazZ#%@>xd^`tTy?;eOw7 zNY1RmFCRBagxvWNHEo;wVt6^Cw=8vBn+*~D>r+&G$Eb>G=_q%1S*Gus+lanMg789a z3DNAp+0Mu})WpkF>)mSRON@N;bGd82PbSmF1EuxeJtrY2r6Hb0Mg4@fV}Q$pI^JtNQTAm0_5Tfl5j;PUEj{>w~0_L z;i1%8zVm^cLF7fC?)ix7OPA{3ouXR$F0J=_mnG9L^yj#(OJFOvG1etZE;rKS;!wN{ z#mi7^TM+5ZqazOEk{AUf3A@w z%(WfUb&+@2GY5O-xII4*7X0wf^IMSNVOEs~gato(PtL5WSDoqAG-de` z1iJfeIkP;8&Rl4Oj>z@g3*cVh+~tD1;?sE|hHyoNsVXal_Nx7I2CXhCEaa@6tUTXH zyW*DUk!ATjgwJ!~2V-GXSuLPz-jXY)I%2Lq(})?M737&wL7oBf3`hRBihM{Q7uGC% z=yW4m+_$Q@)4-kPxQ7Mqk$*J~jfhNCOg%#K(KqBoHMf(VQ;l@<9$I$v1AViqehTWR zxcXy4{U@I^R!35}0lbuZg}VBsv@)5O-V=?~qnfBh@B~CpaM7Q}qN=i103R<)b@jXU zcq3re^YT?Mjstj{1D~j-bg`{wND;v1pG>9jsbd%L!YifpApb?Ur2T3_{`Bp zP>jmzu{{djQO^6B;N7Pxn&7SfQ0_)pYt^G&Z3NVwTeps%+3n2ta9*#1c@@kJe72;} z6@NaFsvPHPveDuslzc@1@}cHfh>0NW(H&y{U;84I#f;>3Si1rDW!bZdA#e z1-Y}91wNrRsmf-u`9OkPF!NZIcn(}Pi1Em0ds#jJjRUaOtRx~kUQ2{n$E?M=T~))1 z$Nk9tMeeTaLR#7+>~KP^=oA@tic%Dl!%#U4l|D<~q}lzm)Nyl;>xA1dzp1J?0{Up= z0#2zz22!pAkDZYOQG_Ni*bvqop1KiGM|kSC2=ns)n6C#!J&5;!0@N_|U#WL}wvF%!XkfQRrDw^2cTFnG z*QDw6HHqx|XX+J8_bWSAFjfnHW$m-WSu7)nQ%Pv8sl=&721=s|)5X|DWJY1+s7$)s zwu;C+qAG*J>-L)0gJ%<8t@GOUO4-EVI1AcYxI83W7HbULK=yboJQX2tB)qL`hX|ZV zvr*!uRF-eR=Nl5~+Md&Y-NOn+6o9Ji5SUl@$r&s>!aiuk>+TNn8~CtY>)rVu%9{w9 z!j7?o;Wj_XUUmQrFa*Y6>KHGH*QoG(g{thL!u2>sd=BrTGYLeU@5x-xfHni#FwN<& z(;ijX%~5bUj$+M9Ja~gE4r6)UNp{n{2|O(1C(jf`yBEy8V2*(KCTH%6nX7L091q^& z%#nz>hmI$h@nNp|Jr3$PsP4dMjO&hY6JPyKyo^oY8xuTId*eu0PgXWpJ1Ct=tD+KM~syPP^1Q{SV1m6um4k6%9D zr@T$z@xUZKk|6Sq<)GE$22_@h0C)r!I?6A4>EF^;{dcj;zo$3m>qC4Oi5B}QuD?KQ zY1Zz}m0T;j!ycr#B-Y}jr9X)5eV+=mw8wBS3|Ta3{y;a2t2Q?ltn2a=U3iGwuu1Fv zBmElh==3ygCE9D$u`#@yoP&GmL4lI-CgSivX3U$m diff --git a/regression/ansi-c/arch_flags_mthumb_bad/object.intel b/regression/ansi-c/arch_flags_mthumb_bad/object.intel index fc2d521766a2ba4b6dbf66c986efcd814df9c79c..d1b887e5bef2cdf13bb5c320d8bcbcf3ddfe84aa 100644 GIT binary patch literal 3780 zcmZ{n{c{y(6~~|FZk~nOcq>s6g9tUTwYACRh5%`W;teg;iVLzWwZ^*LyZ1@%mc6@| z-Mu8Cm4dYuX^KLrQnA+l(m%i%r>!$O&dB?lyavP}jfx0Dq=>&bj#JOsv-f7Hv&@9d z&F=l2@A*FGIp=wveW-VtXlJdKSCUN2wgq0zx1`~CmKoZf%Q$1&w0_%>EOSn!hn*Ju zt;Mlj$&}w@^6=s9ra{kNW4i-J$@Zlcdj2qLIwf*tuOf4Za&iUjkz8oj!oVuKIjdN) zItJ{pTq}0MubeLjd>I4~FK4=e-C^ZS-zppZjyVt*6?m;uG>T@4L8uAt%dqCVMmSuR zOiT&v0auoa>zMW`AGAwhnW=vg^Sa>8aiz_ox2C+9q1O!C4H5FDQZ;?EB17p1Y%0?Z zWTfNR)xZvz!q_dp5SCY|Le3D8pI3{f&&J~1*?IL1Whwm6=6pz2J>W^7>9 zJ-~i9(`I>Y5SkE50TCbGl(EV{fJfOZczN6J)J4Ub?S!`5fmzxi7*_LTM-ckpU~oUY z*z%G8h&;mHZfe5BrkxZEx`EL07B@>Jw94@Mnf}o^wp)@zO#j$UPTw{fp*1Bk=;I*X zH;0)%J(7rem}Uj`ddWV~n|OH!KAr}TKlxJKE60QNj14QSGo6}bt$z^1&2pfHg`5kQo&DjaSEFQRH0>WM+>!<&-_c|7t{?ZwEa<_ieK@zq8Uim{%4WL z(6^sT3ssR7s8PeKO5b!#M&!qsdI}<+!pNVcSa(pYJKqy|#7B!!m<3_l*&Qd+(1W>V%|D0Qv-?KS$`h2z~cIM1I}}(03hALr3JBxyONf9J!w-?mfiqxGM6v z2S{?~`=Sf{h=kvBER9|lPP=GKJqGAwh|UpuE}`>(7kS$AP@09V->W@!^xUIq=%|!R zUajazqmDlc_@juQNBC~Sx5t|2zovHA!QDsFz#m{90p<~8E+FPYV)pz^+&gJTWW&P4 zX~+OJVM69%KpsZqy@b4vkj-_O5$(Q1X|%XSG_pPfxI>8h0^t@BZt;0BzoD=>VlLXB z#*E6KZsUFc?nmJL1YAPEwpbsrmh4Mo6+O>sh}#FOeaQMEu?ocM{ezgS(fN_M!rnAs zy=yd}djYx^p-Tz+06`!8x5z^;iDfDg^?}oAROyy%({-Wo!CpEI#M3}rHnqONsQqL6 zdT48={zsT$jRy9mnb-|2GYFafWzz95==jQMLA|&Gn{laRtZ<3Ji0tY>8t zE)HW~>vp|RuC194(^nB$C-R-Kdj!=Vi5?baLAzb4Wp$=sPeiDg4h&-KO0FD)R*OSn zOuY`Vu7m2?j}mw_EzV>A6#2<|q{Uf%GHr282fAEE!n_+(Pr}-qgths4Q3nl=lg?Js zX?^1=x7~i*wZmc1I0K)vzKm-_l8;|VXeBoSLk_`kL~}2I%nK;Axc1=r}m_l{{ZdsjY}>u067Q?SV9PLD}cXN|s)l=en}&LyPPk1If>A~I_Dl`-`kNIeJTQIq<*#j;Yx^2!bpCQo|d z6oG$>jvzyjP)#cgALiPl%a_ABVem>KN(r~LS9}UiWq`f{=qp%x>&b(VhW`Y{TW7rQs$vX;WMV zX_ryjMo!u`aS|7Aw*s~5P5fY*x~M_cyJTaX4uZ&oAX0oM=01m9Xk_)IsogxsHzv5g zSA!M}{kDSlh%t2|KsKtZXZCkv$n&wdc%KzIqxyNC?@mB&It?aEXE)GxgQOR@)W65U zxy`Yp$C9hNnMdAzA0xiN(Y?+5M#8@M(C0{V4Jf<;_T2#cwgB@*WRAqljwEx0m@gr7 zOT--E6GP1G?AJE*c(^i*sXIWz4!Hbqyc8*~@>cyPab~-ap3zzqZAO31 zwW7=8PvQ1dAMriWf@{iad@=0AU0hoNccf58bK_^+pj#b8-^H8z-iLp;fskFCzmE8o ZTH)vXmpt_04#HUUlyiK1%j@u){SVK-WTF57 literal 4456 zcmbtYZFCe@8NPS7X|j{h)r4vZ)M1G%I%r01lV)x}3q3c;TXZMjU3v(;xvt*^oNB3AW-}{K?j&FvAe8|_&k#B2$heaPW+g?5J-Kzu(;K%c zx&ex6M&HHAd{pQnv(n{Y41be`s;a!6Hkg*!N#se|qic3I3B4C+YX$JWU}F;6Y}K%d z^oKwMkKVqcF)7Td9twzGB7hBEH50a^fQ9gOHIch^s+j^KcMUFUS>hAHcU(&t zK7XJ;DlFy>!w21le+7#*$=4}%H@J7g$ zyY6{MT0))k6_>XH@`7?*{V%095JizV>}!#_IaETYe?ETWb2$nI;&QS zSRWZ%%1Z8}W97ZvO1bW%FG(Hcq3#{=Gbi6|S~i#HIWz)?M&QtWA>?y;EZiXIOM>{G zKqL1-V=3~nTcMKUdDNPMnn3>VCY2u-ziIrF)Gqp>f?O{XnpHFCGKK#JQm;emb&0f8 zeL_fGHSI6e5h|qKFQnF%484ECPo-uS5*g-6oPfj$NPHljGa;Q>B>u_uvG9X}^{4(K zwR>f@FDUUQSx!C;au3K|pIM;tw#}PSa1Y)rSH!Ytb|u5q9Z+-=if(d6O+wM?Nq{=$%^9I_(GQ zVCs3r?E(mz2JSS+ZTE232;7dtQUrZdBD?08AFfMwG4wG&9|QDSUTz`G9|p%QPirS{To!%3)_fdxkp_6|k#f;YS4Q`j@4(<%T>m>WAt~7k9*X#W@P(Q6N8> zj&I;2HFhP?iRuu>bR7ur^zbu*7v;u_6vq)iMiete;*T}xhQ@kH{P77Y=BDEMf@$-4 zrdpQTN8+0tSlHY}Nnxf)^vQ6;~UvB=a&>SkL=DN z2Xj2Tagp7pj^B<1KPbc7gqo)p0+B`IciXIAG@Q|CBg>phokh@D9`ws1=;~Pb83Fi} z{nA6_CH2g>A6_13W!az`2jn;)>%O`&{xyM$k?<@~aUg|CP0Np>XD^hslfimzrTjd) zfHu0o+vw{8<{SHKmd>^q(uxr9%^@kWs40{aehRW;lA1YYsfOmB5hozz1ouW2;qQut z69PKKu6Q-H*x@-u5Ljcs$afZ>K5|*U@D7AZ|*Bkxah^b-plhm~`i;9Ps znb?j^1vPUG4qf98>4M@@vG8_5amR=hK?|4c-hR@LBQrEzH4HQ~5Kn^RNiI4g5HVx2 z0@3()Xwfjw4*CJQE$j&&1n3|KH3cZDEGIyp`&Y=*&c|Wyh#x4nTrV?6fOiCVRyv-C zk+v|h@SfC;mJpIXBX=UC#f`MDmKmw>rN^`JDr~&UZS3**^$LE)4TMwc9q^-8zR3)L z+5o8aiK7L_3fZ+X{w;xvK6qYm{r2G+oWU+x4lf7$$n*U*rR^rC=NLw5!Rgcfn#;ld z8q%`6f>#tFFRV38n>|-hGbH{Z_0acF0skHPXQ_QriN?R{zJ*A;V`03xhu$c2q*z)w zC=J%5h^ajvy#Z%#aA&?({5k4jFAsu+FIFn9y>!gaoZ`0Q)xsDI8iPTPexF{X@gLBJ z_z&p>m4h!)hC!Ly$KzlGzf4cxZu~7d3tA!()B+6ddWHTi)Z5viIIDK})gt-*bWDnP z1MXeQhktQklUL~}KQ(;GN0*#}h*J>pBaq%Lr(UD~q3#Xz~l0QmYH+tW*c-89%OkXH<~S zUCc6pdj_1(fb)Ho4Yxw`(OaR*!CN8n$~%EWG#&pbMIRk5lJ2Khq;{`3y-ph7d=63G zONZ$~nFKTw->p@_e*yd#!2bxm8Kk@oVmRQ3=wNBRa@UE}FpP8j8YzYzrN5Kf+^G$} z@Vs(_UMdSFW;OI&LYzwyXBNdWiom$ujh#bE>j$Qn!Z)M+^$Zdy6VJ$Ajjx$qe(NH z!_6JH=P7zNn!v_1A3Y1x&qi_mohg!>rAK}1x_HrWE>*{QFf`c-dO+fpTY(1v&^E3!fIcxz-h_f{}Foqhbyc%Sg$= zH)uVPH{cR)GiSFrLlffvJc_Sxx$7g1PK4C(BP6LF$L*Jz0 f5vAl8NC$xBJyh4QujnZq*QPn@ycfcIl#u@d@=5(+ diff --git a/regression/ansi-c/arch_flags_mthumb_good/object.arm b/regression/ansi-c/arch_flags_mthumb_good/object.arm index d0104c3b6059702ba2db08248a06360b62e47905..6a398a5058be91104beb8926a8071eed71ac89b2 100644 GIT binary patch literal 3725 zcmZ{n`;!z`702(L*=`n%lg*kaf*NoWOiY$xc44!a5S%3hqohN&vw8TS?diU|+o7j> z=6@c~IRkpPL=AVMsE$S?T=tg;fVit>KHG47OD8Wa(Pl_36NSyuesK0ULIRkKz5 znC{-s`JTr;=k)sJeGe;lFj4UxFA@RMd27`Rogq)yrL|1k!ABfB8fKZlD!q(pf68=N zz86NO7qRTGGX-3FKigp$(O5;Wmgh3ouo*C1%yoo*HL!%?`j#0vzQ+_?y=BmG1yg^c zK2WMUZsd5KW?&6Fk+7m_AUeY+aJ-@LK|I;+I-X$D{;L!g;nO=UBYvOtV5~onSZjr5;dQSSnm~vV*jHN64 zAA53Hzmbl&;fJiIQl8jp_08;3{ABY#DRi#oW*}Rt*8ZvgC?O=s3~LR9Tc!LWW-v zf$7;soS>R|0+vrm%bzD(cag2T|EUxfHf&{KW-hzycr&!=;^>qGl2}uZ19)5lzd*oy z2zc)YNseG>Q} z0hbW)OMg_RiZl~bm+WmujT2vw;a&juN??(IeFVHSQAn)5JDXEf-Jzl=685HxQan5&vw+p;S zWRsT7_babt>PHLnimao5e07#=>XsQsOkY8!ABAb{cM6TKPC379+mYjqhE}~u=uB(b zN7$nml&R+HiP6Z2h67>RhGXLtUr^r6UQpoKV}xHxo^>aor}Mk=Of#pnffXxcUsxvs zAG9;@>kRyQyrlQH$h6>y=5(o8Yrmb4))QB_;|)5V6OCa=w8{HyAmcfBRzIJTN-9G` zjAA-Vsplc}JfuE3)ADTr@KXRk{a!LY=2@`So+TrbJP?@Y9xVlJ+FRL*8JJ~(?IL8) zFzrxAxUN$PoseZ2``XVH%P&{37-0N9HKAgJ!rTOWnNZp6ub1?1)Mx28U!F=+W6xMc z{w+%UGp=AR!L3zrYt_Y+L)7v?z6eJyDy(bHwr9Rt%IB`7ve`9>SSfHk2Y4p2Lxu+2L& za|TK85a}KMw^G2oy`fTuPBv35Jlion5339!a1vrq%KCR^>CX~$HEFJQrK$Q|eJ-Up zUApHW?3}`SU7?p3i*iNQQ_dqy($X=y<+XSV@nOf+ij|{W7A+2!cPRz7h3UqNVq9vM zfWCxMTO;&fv6c%78vR`<$aOQGnuHExbQS0|K(p}jjY!+@OV46kgv*zKyetpeTJm>< zf|%qe84)8pn}sjkjdmh>I}yFnnOY7$%fq$qb+x-8ZIXW*qH*V~?04Yjz}VIlRUSMC zD*_h6nz|LFt*G(Rz;}t0kDa@k@}eBarM{qCg%?+)7vCc<){_@eQUp}G>kp^w-LUS( zRr`Mf^e{9WhBq5HHA7mr1RHpclcr@c{A@~7eUC+trbc2^WyRLivygWd^4gx~r0<1< zQSWC|Rxj`kDTRSwMQx(zmStP1sT&|@gUWjQzt0zVek9gZO_%9ENQf^c#CsE$i72D|E%YW^twZTzNz l5Ak&~PQfvP=H8OG09nPj!4!nn{-#|4AAl!CF>A;Bpm1&eS=6NN@i+Tc<}E1k7PcBPG0 z8{26M&Ju!iag1}JlmIDi8D{uQnhu3&nSSku{tN9)bH6xu6Wr40=xBGf>8y9gp0TC< zJ@4(j?|WW-w(psydr7w7Ic~swqSIu_Ejj}(vol+W_AVWA>|l^2-jI6z`7GWdtJyMw+%KtU=Q!gn#X(E6GJYc&v03y^?P+Bj;IW;CL>Xhv&Cu zog5?c|1Cd}DLJ{oaXU@l8gv3?1tp(#76adL2a3z_W=qa-8A-k;r=hR?xoODrH{qFK zJ3e0a{1GBwO?C}>dDgYb_n3=kT?OA8@Vl%`-s&81f-av8_^eojc9#j)I;}1)W@K~b zK+(ttgQa}N81OtBhLhB%)U<8>y5VJs{*89Wwb?MyZ$3nYQAX8&O$xpKre*rRIYM+L z3AYo7M-$QPqO+BeTh!Rg&GX|?y$SE#x;G*IWgzrCYJFSGT#1pEFXisJKIt^#&R_r5 z#pH1B5@X4uJkImf&uB+Z5G11CrfO2N)_41BbF-ksQIdk6Z)bIdXO570GqPc*FRWd& ze#KfNo|*6uQcj7Sk{NkQQt_K~FPP82iTaSZW8@B@{+*BKR!?(vRcS>*%-32Lz9pxZ zgh`f(`Z?{$m_D<3ec#_2Ya_b+!?o`h+7IlJdF|9(zkj-scFyC6%qwMb%n&W0 zoSKICG#CF~B(5qC3UFHu`QZ6R$Qx+qK|9ZB-xsupzG&=9xA29#@~}|s+$k@Od-CwP zMzTe;gqRcOAbXC>J`%~QN|!(;YEE>WZA6RuWHlydfji4_-2#{XYz{9_2~k3Ngyf>H zlZ)eC^qgv>8`eT45vL$}iiAGmhIC7U3wbthMoG_v+cOs?P*7{+V~L$RDX0+k~?&_59%6wx{n==BHW zblu@ucO?d?3$&TTLX&49@Ctxe0Q{+?uhi_HO;g9sI<6CpAfnBxvO!q+;_GsyK+$tH zkp6`0AdVY$#3V$(iv}CU;=+q!2hcmXtv?sGKBOuy30r^hWwNd&UOFD*)R~I?raHrp zgLfP}Lqu5FC~T8NzAn)YUgb8+5_2Y5o7a2*8rUarJl2r@jWfw|Y9=`)%_Pa5za}!4 zZdLXad%Tvf%Hn3TX&S~ME3`U8ErcLT`m?)YMvJKnr+2}~T{7ueFd&>B{L5SoFzn;J zjXNSR&(~_tIUU2-#iTgs`53~n)^Zx6rxBT#MP$U<0dF@6tCxn<*;r62ix?;(+eV3( zXgM{D(99;0vs|^l^1?Lt1Gxvovu0p^wvmC_x>c+A@z~0Ik27K2EUfdgdSN-s7f@TO zvRRn+fZ)O6a7*U@_o3`*eZ_xJ&cUv;c|0a$^Pb~nUdFZy^f=JtKnGc!hCNUz32V0; zmeZAEMTS15`f$5GatOKHYGJFhe<{5C)mL*R2jeN+wXjNH0_Th@l zOtbcpR4{!r&u}X$k~bjv_XNx3oI=ql5(!}$<5ujX|CPlu{D_5GX%T0W?4pw?%gYyV z%fYo`jE<%w+%w=d?~S+^kQ0$jZjC!Zr(#?mP1)wRuRM=fIW+~y z6voVgHzNo--ehE4)TKVBZDf)ji$Us)iy!J^pdEur`;h1TJkJLrd)D8WXFNE_759aC zK0pt~@X>W3$IMNz@F186!F-FhBEi4m)VCw*Z|NW9MU`!sAl>g!UhR0?|291uBl79s zV1(dCS56%T@Tg4MDNm?$h_>qQM!vsCx23{`yTLECzVIIKKG)w#d9B=$ExA^BDL#x6 ziM1L{`dw)7J5<=EJ&8Maz`_ys0o^DHm0JtgXzG1>^AtB?rPlX*`X?IrxJ2UfH9ofx m($8O@Q&jv-Dft7?(uWkcu2JgPn2Ju;!Oj1$K*@L$f%qTAa*zW6 diff --git a/regression/goto-diff/syntactic-diff1/a.gb b/regression/goto-diff/syntactic-diff1/a.gb deleted file mode 100644 index 0cfbfe7718c51972aa74d035f38a68997b2ecb2b..0000000000000000000000000000000000000000 GIT binary patch literal 0 HcmV?d00001 literal 5738 zcmbtYX_yq%6@71NfUa_;(TPL?iJ4?#)I^+VP(V~9Q-VuOX(*9s3`I><^-M{3S6kf; zGe#rJK(mNABE$r6856e{O`cHk)Z{`5f2IcQ8I*9y6LT^$n@XGV)znht=F(BbFI% zCeIj?YBFw$v0BEolag-AVT0x>=Ghi58&Yn@VS~HnL<_ElCkq)X?|K~D~Czk_K zbGw)KM%ivM*_`Xj!*$*+Qj@^-3!4v$L2aL+v1~L3uAW zhP0i~&(o%x2{gsn0);LD+fLZdS2|(20Csgl5E!n$S<_^BnOxpP0P0_^0UP2|!{TcB zt|kSsVp{8LGgWZd(0ApQWB&*w-jwqSzU3Gx&oYBhod}sHy)9qRR&Y~!H#5rgtqwPj zP!)VM`YIWfn?UhzB)eBPbO!F73J|z_GV2zT>M~njn!fL2rizSvNtyN z91=a8G-?eWx>rt|7b;*Qp5vx%(>57ilIbHG-Hh#YGX2AAxKM3GLiG{L^nJ67>8A#a zM8q^Z=icP7kE)u~NOw=c-H+W-%Dj|^oDu1#wSN3R$BXT8B2VcF;jK-3VrkRza)DFo z3%n^MHm{!PpCBDt>uIZ%V`ClvDKSZ>;?F0O`l;j?W5W**v`NrXR1RZn4r6OhPwFQJ zk%*rmB7WvNIf2ay_MCm{Ij(=YQ9o-9*Q8MvpzX7T=H^5HZ+Pf5Av`U+W1Zv28e-GW zKzt}Jp)c%=g9G_MSqCo;!i$6OqAmehKpXw&v1KJ%uq$eOjBxdw)pBBN=ql2CFdMUf zAilJdMjbJ{tmB&*+X&LAsO$&*exg5D&<|DPV+HiMyX3^VQRuPz27)$IsE=s}r@pA{ z1K>Ua94`RRTX1ZDkQwC91VMWKopJ()r*vEgvk7|#BAr7=&dAeQEo4OH1^r&o?IO~Bg(uk=`0xv%c2_)%Jonlf!9 zbxF(2<(YnspgvEHPbYV@hG7+IP14!)#S!|9)0sE&9lm4QhHJxv#b8`ayZD82Vq7ac zsIS0WyCDKm zG}9iEvZimQ9W>A!n?Z?kJu}uQmY2?AG_o1HzAvJI_RvL9L8B`wecsGgH*4EG z4>Of!x9vhX#}-?H?DEo9T1>JQMUX@+a)#51>3{;V2xyDog-u()kxI^r$`**unH;IN zmxJCR2;8US(N*V2lWf+pKEjlBvksbfAt-|D!LpvhenS~(mI!<54mm-SRXC3fX0!H0 zK&pZt)VJ#Dwg z38tv51j$N}%uecapuAInsz)pDWL?0X4dtwJc?8s^jP}}Yz=Q{|;V6r74CW_b6P;5gbjh6D>2%3+hW78{7nyO1t=>jS|cG<_KSvdMYdBKyL=~X2@TGK;J=u?g_OIK045Na3`r-5d^x2FN@$K zW9b~2qU~P6Cou{c6afe5%?hayC!mmHie(XfpI)!w3VDAp?-ilIZU;Uo36mGoH` zLfukHA8LN<_`Ha$Xycm)QS&H$?kT5_8o!rN@Je$cd_9>Op>BAhiz8keSKg{Sv`E0JR68 z_TfOS(51#72?dK}V8$c7pBI&W-YfNU)>s?7?hksDkI=ux$K|@xZD_dkVltPzHYR*G z>Ea#uF^;!>HI9!3(zp2trcFZ4%R9jvz~g+f?O15i^thkP@h8Y7Q)~SWe}?CMyz}Gt zK7KUr&8q>Rk?3ef@CcfpgsOjeP}s~jbP>A$4i#f{d})Hv0X zvO-++$#+NXUxWRx$UY78*EuE!KEahs8h0VkS8L$uX5O{a^eI9*j)E=b<;kqw^+zmM6^=zFZ+0 zF!D+>#Xlu%3(!_X{lCju{1(UPjHeQ1Zg}eG8>93#$TyT6+{p3qPmR}x`|~(5sFrmr zwK%&aqfJ=9xw5`|xYYQT@Q|q5@FAiAb}L(WfvO8WL5Ya&GlbzXQ%1rS7iqdOYkS$I4$rmIc-WNj+%~T%-kORxwmG>b&u;VVY!*mO zZEntOw46kuDchaSnShV`A7jw9kVvLXiA|X@n-!E+wm_N9`Xm+Kv(x3Vao4h$_73;# zT;59y%ao~hDwFGGYP2Ei=DoOWB;B~_OFjn14besqUnox|Q%3mWBl!1WDPwwO%FaPC zi!$xC8atVEGFd0fM!r%*I@IVfY}6Vh?xr&Ej>Xt9y-GppRr;h}h1IiT)wr9^=1llf zlY9p=t>q>&nYY>K`AT!upI9^fA^78jw&UN6OdxG14DgicqyvTOOT3}g%pwfzxOoaa z@Lkdcm)xp!!6EbDj=EupH&@@PX((wKiHO&*kEogiIb+_HtLhLBV5k~B5kkhkEuY(( zcak|L-DrC8b|;6p<~_SHoAVIM>{RF)J??&aJf*}7wGjq^L)nQ(WW!J|pLN+)(`Oms zZH9K`rI#8`)|hR3E;JvJ`=lc>YyM~=<0AcRkLf3o_~8&wl0P=TCf-iDMHzhZ-pIr= zNmxAz(?)-Mog6zmpk<$Uo|~3MiDbA5rZ?0(Y0K_n`X^U&A=N1PLX$ofH$BhnX8I|D z3`9(`vd(OqoeCFyn!Y_5^rtN=o{gl7tQH4EYx&IkALhTo-5aAoLwL()_e4@=+|Bw% zsW0+|q{x(!Oh27;Xf2Ja2FaPhS&C1INje38&q(N}kYS9~AFdW3XelU%5tYM;N>f5V z$@fIGS$I6QR*unup+K|o&vSi3y?*9uu1ROb0c}kbnkOClf89gp4DOk{JJL0Iq9KCb z4F8Z{0$W(~!D=>8!oiAzu;L)Bs5=|7fHvjP!DYpo{o{9zF!kKK<=Di)R6nQB* zWv5W-3^!wYX4*3RG%6_jLBF5qKPTwNsL`nc`nzSZP{Cmw3CjUk)vapPmA6F`n{mvOY|2A`suF> zLJwaC^fLtg%sb>5`c9dC#_kWJ7Y(bR>;~~}5Hm?yr-=G~Dr47+-%#-wdwfXUg+kOt z?^G2fBnh8fEJR&$yBtHRl|@~=tC}eP{9A6mHEA0~VY?t~7ld6p7LDig2=2qu2sTPu ztCVY>fllC2S0$OOP77S8MlTZzF27AKRxm%wF56K}Ko-?D#JvODJ181o5RkK8t!g;h zN+}w;puM73o)orQ-&T#*x4T&UN|tW}`!=v&8P~6h6mvw38N*RFzqq8P_@z-S-`1CQ zaVMQ{(hfQ@N}C$J8d|>mZbY<~M(Qt?qZ>g7Sae^0FPp)d-_8j{17s%;uPWy`Vl{ zjhbW*Mv5}ECSA+SLWn+Xcjb&+yJwr0;aISs0LB7Ev9**Kabdy8GE96!2%^FQ^rKQp zHUMe^pe#y8d#V~u2t94j$PR1p$61HUxy9;vy8Mpvw3!o}VF6Bs#)Y7s`MLSK8)7_F2 zGlJm8r{(b#=R%W`EVDkulyNdPI(pu(jO)R&p4{k_fU?4kxn**Url`_nlHC&msc@!W z^eRi<9^mc)Za$&k1dnzKapws%3@H9kLf?0RH?OsHzrks~L5g&)4ABJrA!(Z(aLG!5 zt^}wv`>eE^vv16sNv40bBz%q_QOlC`uLTcrY#cQ@hs{|L1~-$KYN=MI?M}>EG}aW9 z6(CswlA9CyEl}RW1?nY7OUHw`9Pl?oJnP|0LckVfsoQ!3<~;x|0pJpH@vXER-Eb7UkJ^^(Xi+y zmZFPMLFofXpUfuLEe}BMZw~QQsHd_~a`a{}Z-)Gp zaP-~e=v9ICp+`F!5AGp#D}6_=;)_H0$VSR@QKsKa}B1J!)XPO!Cnf27>tY1lK+;8EJHW72)WuAFb$ z@(_8DD8X#F9CXV;x6Y@dn;KnqQcU_r03aIJp%78=_JU&}ny8Vd`dLs8Mf#*e5p=El z`8d6=oFWedP`$jIBh--|;B!N|!rf>tRL!Lv`DQ6c)aZi*gY)|kKN6`JS|8+FLO2!9 z^-F1SO4=1{7`D(|o3hmmY1n*av$@JjIJk*JJ532ooI2+#QqtzYipA(#CSJAOnvP(6D1k5N3Z<(|+M zRF{5vRd~x!u;r(;#leoBar8^3&n|P!!TLENhM!~kFK9U$K@WcoeE{nhhZxW(`sGDo zhF@aK>$C-TX{yet-mSb#SdRKWv zC)Rg{6#fp&e^1M=#qvLJOqNVH%F9hGH$%(+h~{f5(o06!rWQbq71{5A8sS>X#n~@AwyXyh%IS!SNQy z=*aYc^EbIa*Z41X{u3OqxA}8CVJ7h=3<-?6RB9Lh6*Hs*&>bQ58%hbhkz>BaQ;Bjm zIGgnTQrZOa%|!#ZaJ*PlqqRYNp5*jUfi@5>$jEHm(GshQJd(bPm@K$uBWL<7dFj(0x?dAD3G<1i~TyI(PHAOrAO<)ndY`Ez3Dva>M(4Ewn&v$P@ns -/// Writes a goto program to disc, using goto binary format ver 4 -bool write_goto_binary_v4( +/// Writes a goto program to disc, using goto binary format ver 5 +bool write_goto_binary_v5( std::ostream &out, const symbol_tablet &symbol_table, const goto_functionst &goto_functions, @@ -97,11 +97,9 @@ bool write_goto_binary_v4( const goto_programt::instructiont &instruction = *i_it; irepconverter.reference_convert(instruction.code, out); - irepconverter.write_string_ref(out, fct.first); irepconverter.reference_convert(instruction.source_location, out); write_gb_word(out, (long)instruction.type); irepconverter.reference_convert(instruction.guard, out); - irepconverter.write_string_ref(out, irep_idt()); // former event write_gb_word(out, instruction.target_number); write_gb_word(out, instruction.targets.size()); @@ -150,17 +148,16 @@ bool write_goto_binary( irep_serializationt::ireps_containert irepc; irep_serializationt irepconverter(irepc); - const int current_goto_version = 4; - if(version < current_goto_version) + if(version < GOTO_BINARY_VERSION) throw invalid_command_line_argument_exceptiont( "version " + std::to_string(version) + " no longer supported", - "supported version = " + std::to_string(current_goto_version)); - else if(version > current_goto_version) + "supported version = " + std::to_string(GOTO_BINARY_VERSION)); + else if(version > GOTO_BINARY_VERSION) throw invalid_command_line_argument_exceptiont( "unknown goto binary version " + std::to_string(version), - "supported version = " + std::to_string(current_goto_version)); + "supported version = " + std::to_string(GOTO_BINARY_VERSION)); else - return write_goto_binary_v4( + return write_goto_binary_v5( out, symbol_table, goto_functions, irepconverter); } diff --git a/src/goto-programs/write_goto_binary.h b/src/goto-programs/write_goto_binary.h index c700f41cc04..a770e7bd391 100644 --- a/src/goto-programs/write_goto_binary.h +++ b/src/goto-programs/write_goto_binary.h @@ -12,7 +12,7 @@ Author: CM Wintersteiger #ifndef CPROVER_GOTO_PROGRAMS_WRITE_GOTO_BINARY_H #define CPROVER_GOTO_PROGRAMS_WRITE_GOTO_BINARY_H -#define GOTO_BINARY_VERSION 4 +#define GOTO_BINARY_VERSION 5 #include #include