From d8b909bf6cf0fc9f1ac00c7b4b398f5ac90e3641 Mon Sep 17 00:00:00 2001 From: Daniel Kroening Date: Mon, 10 Oct 2022 09:04:05 +0100 Subject: [PATCH 1/3] C++: __CPROVER_integer and __CPROVER_rational This extends the C++ front-end to recognize __CPROVER_integer and __CPROVER_rational, in the same way as done in the C frontend. --- src/cpp/cpp_typecheck_conversions.cpp | 28 +++++++++++++++++++++++++-- src/cpp/cpp_typecheck_type.cpp | 15 ++++++++++++++ 2 files changed, 41 insertions(+), 2 deletions(-) diff --git a/src/cpp/cpp_typecheck_conversions.cpp b/src/cpp/cpp_typecheck_conversions.cpp index 8817ed686aa..b69caf0a58b 100644 --- a/src/cpp/cpp_typecheck_conversions.cpp +++ b/src/cpp/cpp_typecheck_conversions.cpp @@ -1451,12 +1451,36 @@ bool cpp_typecheckt::implicit_conversion_sequence( { rank=backup_rank; if(!user_defined_conversion_sequence(e, type, new_expr, rank)) + { + if( + type.id() == ID_integer && + (expr.type().id() == ID_signedbv || expr.type().id() == ID_unsignedbv)) + { + // This is a nonstandard implicit conversion, from + // bit-vectors to unbounded integers. + rank = 0; + new_expr = typecast_exprt(expr, type); + return true; + } + else if( + (type.id() == ID_signedbv || type.id() == ID_unsignedbv) && + expr.type().id() == ID_integer) + { + // This is a nonstandard implicit conversion, from + // unbounded integers to bit-vectors. + rank = 0; + new_expr = typecast_exprt(expr, type); + return true; + } + + // no conversion return false; + } - #if 0 +#if 0 simplify_exprt simplify(*this); simplify.simplify(new_expr); - #endif +#endif } return true; diff --git a/src/cpp/cpp_typecheck_type.cpp b/src/cpp/cpp_typecheck_type.cpp index 0ec59432b39..d55c39f7b10 100644 --- a/src/cpp/cpp_typecheck_type.cpp +++ b/src/cpp/cpp_typecheck_type.cpp @@ -10,6 +10,8 @@ Author: Daniel Kroening, kroening@cs.cmu.edu /// C++ Language Type Checking #include +#include +#include #include #include @@ -69,6 +71,19 @@ void cpp_typecheckt::typecheck_type(typet &type) if(type.get_bool(ID_C_constant)) qualifiers.is_constant = true; + // CPROVER extensions + irep_idt typedef_identifier = type.get(ID_C_typedef); + if(typedef_identifier == CPROVER_PREFIX "rational") + { + type = rational_typet(); + type.add_source_location() = symbol_expr.source_location(); + } + else if(typedef_identifier == CPROVER_PREFIX "integer") + { + type = integer_typet(); + type.add_source_location() = symbol_expr.source_location(); + } + qualifiers.write(type); } else if(type.id()==ID_struct || From 782e9a9b7947ca38ef9b220934cd2db574bbf42e Mon Sep 17 00:00:00 2001 From: Daniel Kroening Date: Mon, 10 Oct 2022 09:04:27 +0100 Subject: [PATCH 2/3] constant_interval_exprt now recognizes integer_typet This enables using unbounded integers instead of bitvectors for architecture-independent constants. --- src/util/interval.cpp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/util/interval.cpp b/src/util/interval.cpp index dace8934b85..2d87be0bcb7 100644 --- a/src/util/interval.cpp +++ b/src/util/interval.cpp @@ -1094,7 +1094,7 @@ bool constant_interval_exprt::is_numeric( bool constant_interval_exprt::is_int(const typet &type) { - return (is_signed(type) || is_unsigned(type)); + return is_signed(type) || is_unsigned(type) || type.id() == ID_integer; } bool constant_interval_exprt::is_float(const typet &src) From a4ffe596dae149917c39155f00465e70aef6d197 Mon Sep 17 00:00:00 2001 From: Daniel Kroening Date: Thu, 6 Oct 2022 21:47:52 +0100 Subject: [PATCH 3/3] change type of numerical architecture symbols to integer Following a suggestion in ##5878, this changes the type of the numerical __CPROVER_architecture_ symbols from int (which is itself architecture-dependent) to integer (which does not depend on the architecture). Closes #5878 --- .../ansi-c/arch_flags_mcpu_bad/object.intel | Bin 3778 -> 5651 bytes .../ansi-c/arch_flags_mcpu_good/object.arm | Bin 3704 -> 5568 bytes .../ansi-c/arch_flags_mthumb_bad/object.intel | Bin 3780 -> 5653 bytes .../ansi-c/arch_flags_mthumb_good/object.arm | Bin 3725 -> 5588 bytes src/ansi-c/ansi_c_internal_additions.cpp | 3 ++- 5 files changed, 2 insertions(+), 1 deletion(-) diff --git a/regression/ansi-c/arch_flags_mcpu_bad/object.intel b/regression/ansi-c/arch_flags_mcpu_bad/object.intel index 2ba432c93b368d71d39d3e3a6816782f6c234d46..12933c39767423e1ced8afd84327b067fc7f7ea1 100644 GIT binary patch literal 5651 zcmai2dwdkt6~1>iI2%LVT4_sUTcy!fTMP0-YO<+(CSn=!RK(2LsU$lM-<}n- z;}%n2@DC5??Rd^k4lpy3W;K2^u^$%une ziBGRqw4^d)@TL*9Ggz9+jAf^9QU^xDiO9f=)s(TaSuhSXlUaK}WFS!(vAEfkH4>3@ z-UypfiZFDm8P8j+YNJw%PiuHh*vwk2_x)-u7@?lA(>D4IW8|po8gIP(I>Q^Nq1|xx z)rOrlZnH8eR`3g{Y@>g^ZzTR@gFY8aJN{;veuf{m1!k!Yzwd!L`CM4C;c z0DhebcT}y<7ame;>DB5=$UL1aKkF5BXgyx(vx1w^C}}fNF{Xd9znzR)txW&YJT81Q zTx_l4%V9H5!uR~8{ zG-^}T6BY47m+vj5ie7il+2x37gciDDJEx+AGdpshTB=$}tHnr#Z$^>CHrl7o_w7?5 z<;tM`10m%qA*ITN4wW|0RSU{VL78xsEP#>)Q1ZjD{-es`o)yg^fC6*%Y^C_6;nuoq zNT}AQ)@6;u&P z0_851HQX51e;m_)(l3&VTFA<1f!kY@?{1#4(Atth*-gWp=N-PZnK2Vq&dOxjPnrI+ zncV#Xa(^DvZ_)z4DB@HbJ3VofLNKCed|8BE>=O<-J_klS8-xCjz{_7AE=;{iiaIOi|MhMKxm5TQ7zCc-`A?`qn@ZtG~A}7 z8AfyO5l^$$F8ZpGgkE;@`)WFecBj3g)YwrJP&;O00;y#B7@~+*YJr3xsB%?lAMqL* zF``zCB{zFGskR$AfW7Ox7NS#PVfqEN&M8^8KxpT;M2Qa^8RE$HqH{=L0PG{{bt77c7u3nK;B8?FU14zpzKYBFw(IyJf@$a1!fZvCc<|9uv+Ww!ZcmY;VZa4m-p8n z;PbGn=Rr_kE&3qEfQhUP!4rTMdWhenVv^3c;)^a`g_%vOaKE!xZ-Kxq@ar)M{4H&{$0gDL zxBQCD{y2Ab`x7MRF{rqLJE2WPLA4gMtjiE8 zO?Xf8b>%Ful2O}CCNXRy?sc$Y9ju5qCN`rCYzE(El}+nXo`#S=kdXOO$TNJ7T1%c3 z+lkOKU+8(3Vtd-rGoSD2sVDB-lbmg}2l#tP&mW=ZIjN^Z>bb#%4n5Cb^f!2?rVhTc zoF1nIMpJoIXt#5(gshd2<$FPLERZS|@+Z{6J*Fnn6c_NRo}e>0R8hKwC8+Tg{8JJ3 zRBYcxFl8~B(kbEExf`>vqf^+iglHEzc69QC9%R!oqm$QcSBN)4=b)+LxZ}m;e7}b$;SkZRO=FU{Fctj!!M305UkUqPlq9R9 z{j2#jwamP|iZ3kZKCY|oU1T9#UkKN`VAC41X|0U^sZZOqR@k(TLg;dATFVc3!xwj* zxMhxk{Ra^C0ffDtYW)U@xsfka>%HSmH-CvZ>3N6mWzO_Jaq5b%Aefi97TDyj)2a*n zxQ9%fHY1be001^;ox zeH<-?{TX(@Chguz>rwk2EqM|e=1%Tg`J!@87e_sJlP`kZi|Fib1N?S^$27S^hPRVH zst)$r6WYb!P#Xq$|DaafO5$t>Kjd*FVYV7_2gz&ZAxJqyJ7+hz_DCsvrIa?0l-{nC zy?jYIDcR;!1{XoksJ#SQmO#rsO7VWF;Q(K()_Y4%H-DW{OwT)fe?f}>>SX0_Nb&1P z@j-W;R{eK=!XrqgIF?BzdZzebDaA~ZPeAJlO4}i5eM4$}Q)&&Aj$$cmZ}Mg3 zq{<&l+@vjo&}9(%772Y@2K*1+sn&a&em8%Igwpd4-#;PrUyjgsA@m&xea~H|RsWlx z{H)NH=G3R>)%SWReH*I^{*zF8l9c`jN)Jn=N2Jo;r&4-^uPCSVQzdu>gsyMtnwW}z%4|ObKS)U!sKkOm$eXJ<> z$0LyO7(!1_ARkM>lYFUK-*ZyTB7#p4!FYwr#snp%PgD>Ztq9zqhyn8?cKRe`q9+bi z*i(mchvF6w?5vOZM1(RCp-e<5>`o=9-=*Nh;)kKhgpGpmjOP>;Z)%K9R#to1di+x7 z+~s@znz9-Mt6}=x3bamJzaaCzkde0%0tQMN9EaSNhe&b~96Z{2Wahrk(+xfsbeX5+J HaK`=zzFAb! 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 diff --git a/regression/ansi-c/arch_flags_mcpu_good/object.arm b/regression/ansi-c/arch_flags_mcpu_good/object.arm index 6593905c6b48c9f45b19be6994f3e27a98ffc1b9..5a6ae1e2c48a122995a665fec5b9fab55d48ca11 100644 GIT binary patch literal 5568 zcmai2d7Ko*8LjGB>{*vMQHf^4B!R3ZYQiz>su)oRjbb+17&{(0J3TW!yDc-_W6z8W zlBj@qz$)MYiXtW&WAIq+`&c}f9J;}9pD{ty7)=ad++Ya4>Z<9f73UZJfM3&H?|tum z^?mi#+&b#w%lZr~|CiLQ)HxlW;IIz^(@vHvEaaKUbMtaS1w zqRpZ0cDmR`>Yh=Xh7qE@7ivry{#SiwD*Q78umrCnjRm*lr7R=srp%)4I^;O~@5vcE zYZ3MN@Q7r|&K7NFkm;q`?4p$_mON`vq3GF8YvDqC*)MB5775Q)hYiJ3G*fa?K1w~F zy6f6qZw$UP(zb`Ct~ZVx|B5;!mCU7vcvh=t6$)S+VmbwTP-+OHFfv)QwP55@`I6D< zx@i_-;wCd&vPi=QC61@{v@vNGEYkNuH4aM1C*-&n!iI6lRacL`_R^~jIZ{Kr=87u} zyI|aGc`hl3xmNN*cwXod{7r^_CX@FK_K1E$eFuX=XZF{TlUGqQon{IRH$(J(18pa5jV1c$W>fB-5uj>y zrzB0!GshAA)OswAFczYv3--+x`TR(&E~F)*Gt_fH$vCyd7pACiy)+h&U9>SP>>+x8 z{%!1Kg&T7!%=uzQKh+P2oVdQ0Np1nwtcNG-;RyLsO#iYE6dAzf4SZCMpDW2rG$09m zed7nLtA%MfY1?!h=m+*XV6S7?Uy13B9Q!nmefmRcyy?@iPg_+BoB7X@TFDm}R)Jv^ zWB6)J{~BjFgEO2tQ;oBIQ%O$ZtVL=w+p84~XRN5jlXcnFbxX;tW$=P3hgX1T1ta=; zO#cQa8pMePKcLE+AQ2821}&?_P(X1=;L8BMjDZh{=|eeqoP$TI@mF!?+Bn519~xoK0BtL!=caR(8H&zXUoP% z0{n9q)x!5vTk(1kpcgUd^J4lpIrRA)dc-uf`O~4#Usww|>AKk<>V<$_2_FP*koH{+ddqgXgvzsqN-an{5u8#vYI zw-VmZLt6UVA5z=N*pAIKpjSjj5z-QJ>?|Rpc1S_wtQ>2=~#9;Vb9YvK1{pZTPLK9G(wX=fl;}OjjM+*i{c#b@|oAPo3|^^s70s&NZGH zs7u7eE*VYq?NaoPHMVFJ+dRum8)GacV>@JQSIO}2CG~4E`nCO2ZrVaVuH%S(c`NRr zo`oaJ;ci_&!hhcx%A1~_Esy(PjVmkz-sTEvZAu&LL#ykV*!OP3q$^`ps}`JjWQ!0eIDq z7bza^r}$?g#p3}oeyb#>x?9*WxE0V_k@%k@N4Id$TRYVz9PCn#Zlj>Y+s;ruX}RT~ z1jb6-HnVIhD2ERM>mb4$J%PsbiIi`nNtB~Tc&Jh>O`=;QB)OREG|;vHZ3}wR?X*(4 zc`_NmcL?A+1@K+;Ikl-*=dG0M?UdX}4@ew&J8xmeDPhbkhYtY%0PydoNxh^+rUTIry|Nqj+CrqIn2AosFhSYt7VvYTK%o)km2@4^f;^WH#L;5v5s64Nj+B zK;H%QT#M6%bf*WKmh;TzJdZP;IX=%^y0bS=*1u%<$=eCw zo!}wAK=OVmlJ^9I#y~xb2H4UW^aNc{s}okvmf(C}0NWR^(cwwJ|4P6=CE!O^(W|5E zQ*=!&bktm{lS5~N`)dHa2Ed_T3(%*99lxPZs>9^*Kvdt;v_mq%LqVk3jVQ-Xt8%yl zHgsU?&4atoFn6C7a3=*Za(AEQ?mov@=lSkFOZQ2@rtfVvkNW_;5B`>(r)N8E(Ymo@ zW{KV@f}Sr}7SKo3xZHn4(0YF~Q7wYc=F>eAOU|cZvo{-Q_@$*B-UF^ZESC#m_98*C zSeQLk%H>(X1h|+kspYnx%VQF{1imkU?@L&XE*0S~ql?vMdARSP%bAJneP?I|CHhLr z&VyBOcRAG}tAlk~bPYW$3FG_UDCLW8r5~|d99x3ZZVW$L*7{&MEwWDFbkQYhvp+Gd zp}gPVB=WyS_gV^qa`-U3IgCEN9wEHIVtY}n9r%d^zsM8(60>i;pWqkiUMWI8z8P7| z9D{wc7qEL-nZ69mHweqi0{XY~adnt%OX7F*O?CKC_6O?t#V1F~bia&mjx|Jj#Wc4c z9Q#>Xe-Dm72#!}62THVW5PqVX)mP~9T3P+XHEKE1xg6jh4CV06K>D(Nw)1q7G5lM_lXU21Lz0-;Lypm3&s2hvQ;Umy_1Suk0 zp>vzixn1bIysEQ0l5M9eYw2wFZ!p#C(Mkwi386cf(48XSU38h+EO+W2x|<1Q?>j?# zAat)U^v@8w8$w?X)@jkd(4)r+ZEtfwIi$@KydBDnDfM*@{R{uuO~o zhfb0LfU%!0x2Kof16WiJPeLe@Aono9PtYPC38DX`bJVze3t(;S2wg?>|IvZ^QHtrH z?iBX9mbguss+wM|ErXKjq7C>xNvrdJLLwj0E-9>DzOV=Mqb{&_!H5Y8jF_nKF?5o$ zQf-!hIpRj#t`L2)!us+ZN=Cm^fe~y)90>!&{1(M?qKluQGb}bN5M=cCd9!a{r4&(h;|`5;K$)wCLgYNJ5U{PXukGL!r|Z|AA8WR6kw8`1&#J(mAgH 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_EuaiI2%LVT4_sUTcy!fTM?E73@x>bRIRN}&{13LV>-J#n~dxu?!yGz zA|Q&$ONj);XSG#})+mqg6v9(0i&WlE+fsbgR$IVIP{e*`?%mmmvcKjJ`0dWz?>paj z?mg$+z5U9|uIM$8rR`MCYP2$p@nCLjvlTV7Ii@QkqUlsNXQpyYtDvu$&!4p$Q&uc; zE7Kn4Ep{x|#46^iwSyVc-u2Z)4d<<1?TUEK04&3!KutEC&qOUFk&c=WZL z!_`+CcGkGf%A{GrFT}Eq{`tO<_?Hd(T)f$FIK%Wa{4g#sORWdyTS|>`eHhYJI-&kQ$;_t1BV&bTa*{SJa_(c%{z@ZpLDy&Pd0Z{>A=wDrU7Z{Y&$> zaL#bCwTdrC%uL1{%k;huJ#jHDmbGuQSoH|4;%xf%EPUHvTMQyDgYETeb7q3Z3-4t3gbC-(Q$s^NCWOzQp%VKV-rGq`&DwI%Nh^u{V5FO^jG2lVj^KiSEtu94 z)7OLgHw4oKg6YBs)X)$wQP0)W0R5FA~rL=BgnI zx|qrEIWF`?UFD!#Xg?S^+FN<-Upjgq=>ka?kz5?q2MUrwf+W4)Em!J~XIbBEahfc(4@p zumx%zo%CXY>z9^8ceZJ9ueu~lL9&!cz8%!RBS?k|lJCw`d*nCZat!Y*$Km9l7=I_A zI|=&Ip#D7p9Tw2%m*Ov>h8LGZjil2FH{iuUT@2I_as9I4Rl1QWqcu)36W!!&Ev6mgb}DYCZ1M#)CU6a74Zf6}VCSm zdZ$|O??m7`5xCh;3q%A<^m(<`+jY8m458v-htFbqd?pYY<9bXBG|Bh1YWt`sDibZY zF=a;3-h0H;q_vB_YNVi--Tc1VoI|_Q-cf4o7z(Hzw=siMGJOnDBr3H)QV>+Rsgq!cJ8e(t_7=GUzVN!;wawiQ#wT5+z02d zbzf7gM8a;)+F4e`*lk_CqUmHah9C?eEt~x4(bz|uaDX=X*}1=p=)aEZzk%=LL}Wum zSmLmclQ|vdjzk=@8oJc$gdt{v!Z90tZG-;z9jRKEi3*cS+!Yh}Z3Nqu5=1y9dd8gluYS z+kv(n^=LAuQ(J*V-p%Kfj;$C*rhw@l$uw0mP21qyN!S%Vk zzy1K9hh04ng8FK)2PpVy;iG)IS}PT9@n|ZJp_nE`2{-bT%7T9j1a5&}k3ryXY0Et> zkp{TsS8VpjxwG4!AUTgg#TD#vzSqMLqblsSwY`Ad3t09$q~Z564NpqZ@HuLT zJSnylp=Z9(^DM>ow4-M}-_ui1!nr9q+iDN+_mG}HLeFzjPlwcVg9{ygp1V<16^5 zBJ8QyzKdYWVlt&u!nJcZW?@ICuwx0)E^_SXV=4&Te1>3`zX6<I+?R&K3NqCq$xo_o*$~j#e_1sOq2zD=`v%3xO+X)`iREjiu%bxJWk@9_NvDgLXImA@gy zuOr0=-E~^^-}woTAerKLCY|h=;)A6WBW?S!sNg>VttTjLhoJQhsr5~%HBdT=rL4Wl zmz9$$e=Kp6whTg-LFii~^lcgNKX|8F=WY7k{2dZX&pUkogwTIELf?hZcOdjVcb!)K zZ+`N#LR*^BpPpCW>!I{*tSb0VLg`6T`X4AgER`OSN_(G5=@Gu7oYGH~;1v+M0z!|H z(D!A)|K&^6I&b;y<{ywydfwqX2BF=K(BlyL0fc_&uG6YN;^RHk@r-4Cb}0X_hsgJ_ zqTnBoK*nPTJwbtdECEmQrD|QzNimBEK0yTI6)GDOl(;@oL1?rhaEBrW%#+yZlaz^` zI8b3v9m*YwTRgC{KIRh<%0z@R5uva3c@p31v8IzRPsCYE4(E_j1DOghQPeLG*pp?@^z;~b0PoE{_wh?@*bEUXn!R0_skwawN zn62Q~jZ5)EZO(FjhH6&~am~b4rA_HQhfuOwc&@UH=Q8+>ld(_m7l6fW3MOpl1LyRq Ja*o0o`yVeORjB{~ 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 diff --git a/regression/ansi-c/arch_flags_mthumb_good/object.arm b/regression/ansi-c/arch_flags_mthumb_good/object.arm index 6a398a5058be91104beb8926a8071eed71ac89b2..d7dd5b25c97232e478514b27d555f2c19adc9d96 100644 GIT binary patch literal 5588 zcmaJ_349z?9e!^%?b|AKMJf^-ks2`yEoqvxv{-OUIXqy%j;V^uxW{ZVbay75-6aVg zr7eY0LJNhqP;Nm*5JP&WXL@j~LM`+@MQTA2P}>5rSnBuYy`6n&UGw|p*v!1|`oH&o zZ)VDsmtN7YmJCj~NsH)_>a3gh5|){E6S17_I)oCUpOLcD7SWy$i;EW|@V`N6+p$RK zd94l~DpPqU;on|?Pn#=RU2l@@G?_`;vl2PiYbX6)Vzr5QCQ<8IO`es_0=hQlWbI*z z+L)JUHdE%S-HIDn7Q^Ai}Vj??Iy=c#&0D0L$uXS=9&q6 zn$?fMo$rLI6XLG$d`;YD+D?vxbcR}DUMyqfEH6t25d9U+N~i6XteqtxLO#~hFX3id z;17)S#c(|4k%II|UJO4K8jqjkoR6nkT;N$AF-{whhwhS)f%mY{pm|fPPPk4s7Xxbu zdOp#iC7J<-OOXg7{N%IYvGKf}&e_f|?%2*DnY?EW%jP^pmAwQv4m$l|RyPKJR8}Cw ze%vM_pISv@$t2IrbW_AQV~Fh}tu|r|T1drEGvL)L{GdJ!6JD&H7-tRu!ay#D=*g^o zlSMu=PPw_i9=$P^&RgWHyV)oR9U)?TcAQ>;5rd!8hVxr1 z&ct_B$~e;(Ng^A=raAuF3D-=#e1fU^GuENQE zWCN6JfRY-&o=vDI`EnJHEfLG+i18JlEpnbvc>aT|4y=K~Xh>gAtK+e(MTX8}bs~rw za^CuKq?VJkV~&I3fqFft*K_J&RmKH^r&jO`U&!i4p3E~80oRb)b>*;QY0Scmh51$p zuLJZt4qaDej1bWE0=i*7tMiwroKn$|i&+DN!-ycLUsaAE?eZn;=HqG06w9p;UIn66 zoM=>)aiJg@Er`b4%hahGz334(Lgg9VU5+P<`L9rPgQA;Le6`9LD=01&6z7%-F*4A9 z@$z!GzJC7)mTur+IpCLb_)DscuL=05fIq7QKQw@kE-MG0ZFapJ?=k`OGC(im(BrC% zO9k|J0e#sV#^-8rrbh<`_~Vz9!;iaeI)GjR=p}%@JY`%l*2=Wx+Ob-%1o+oqW}>eQ zpwHX3#$; zaG&}hV*#t<&AymoqS|kTa(B>^-}!*rPRe#{9u9g{WC9_LA;(S=GGVvkF=J);mQ)Du zhQHm6jF`yT8T#aR?=P_z=mug;ngfJ%%CPlFM&7SiI!6^%F>LZpP7KYXubzxPU$juu!LCf)_gG5~ zO;~?RtG1KqW_HR(Q?4LJ3#XVoK#zEWAQZULKcv;XWhbo^$!=CS`5tFt*GDOH3reMw zCxJ*_0NuEV)%&f=5s33?Ym)PWvyF4M_v1^Cr*@MVFcQ{^xBjG;*;x~k&78}B`O0zX zA&pH(5#&(>d6bcJei}D^mNI^h#HI+0F#>Vi5REjE1qXKt2?PT@Xy@MIqOK+i|<<~ny6{K+*J)$7;)nQ}jz*(RWJ_5ia5Ib=O ztuk(<ZAZ75NsG%VM{Wo3ED3yv1n!{Eu=+mT zu(*b1QgR19tZ=m0Ef$V9d4G>P4E)2uzmvv|c0Dp%!ksI0@@YM%7$mNd#@Te60wto% znpPW5UR>@rz-5%^Kq4e^8OR_^Swad3-p?Wu>63u{2*t*Y3w0-CsVs?wA9ldq>IWmb)58*rhl|7gcqTo zFXG$Z!+?K8!apkEFA658e~1!ik4NdIa=?6ZGO^NbvOE{TYy$QsU{7xJHe;D>hLg>V zbo6MCA*o;Rq#l<^Jwfkdb?W9Ml6qVu^-C`6F+Zut>7KqxrTvEr{vMvxuVCfZ z(#n(4N~mO|l+ly4tDF_}h|mQeT|A@T0Qe~h{Impqf|ii^NmGRMG+k2;neUK1q~ex| zpw@t34G8-GR)RkxbNL;8f{o~N$P~-&8QP)5;9;>P`J-EgKMxkd9SEWWle-f!Kg(n8 zl5nR7QboR9BHu-vwbReHiyl;fV}81&xp)x32a$05Vmi`sbJpa1EKQ6hQuI>EvWz~! z>eTKg+YvwTqX*!&rF6f-lJRMHB>W&F9)k+u{ovZqtGOJZuaFeoGW3=7F4iZO(%Gz= zF8#mB7Z1ftk@-?&zKS>I)l&Kzx`Z{TC+}XmmIuhMcZSwcV)RhH+pI^jYpEXD5RB6+ zH_~H@DY1Udd`r$npI5f_4HSE+D|W6;KGn@a=RNYf$@2FWtd2S(F2Yi*qyGy?kyY} z&x$j&m8?O1btCNFsuANhjkn#ITFSUxgIzu%GAkISSKgt`Pz1EbgkQWKR9o*XEoi-1 zs<&WBAv^;@X22}vFA+l>+F;{O>3BAW*YrU+In2@UK2ab=$4Jw6X=90g3Emy%EdPDZ x-I^(0eB!ZUwszWFj?%72@6ozx&cpjULQdc-!q2!GovZmDDCM69%++x8{V#}UN>Bg* 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&~PQf static std::string architecture_string(T value, const char *s) { - return std::string("const int " CPROVER_PREFIX "architecture_") + + return std::string("const " CPROVER_PREFIX "integer " CPROVER_PREFIX + "architecture_") + std::string(s) + "=" + std::to_string(value) + ";\n"; }