From 5d95919c994f871de7719cbc1fd19f7e13b5136c Mon Sep 17 00:00:00 2001
From: Michael Tautschnig <tautschn@amazon.com>
Date: Sat, 2 Jan 2021 22:40:35 +0000
Subject: [PATCH] Rewrite unions such that all members are of the same size

In the C front-end, rewrite union components with types smaller than the
union's size to anonymous structs. Each such struct contains the
original union component plus padding. Assignments to union members thus
always assign all bytes that make up the object representation of a
union. The use of an anonymous struct ensures that member accesses can
still be resolved.

As this is a change in the semantics of goto programs, the goto binary
version is incremented. rewrite_union is no longer necessary, but bugs
(hidden by rewrite_union) in handling endianness in simplify_expr_member
and convert_member surfaced and had to be fixed.
---
 jbmc/src/jdiff/jdiff_parse_options.cpp        |   2 -
 .../ansi-c/arch_flags_mcpu_bad/object.intel   | Bin 3778 -> 4471 bytes
 .../ansi-c/arch_flags_mcpu_bad/test.desc      |   2 +-
 .../ansi-c/arch_flags_mcpu_good/object.arm    | Bin 3704 -> 4391 bytes
 .../ansi-c/arch_flags_mthumb_bad/object.intel | Bin 3780 -> 4473 bytes
 .../ansi-c/arch_flags_mthumb_bad/test.desc    |   2 +-
 .../ansi-c/arch_flags_mthumb_good/object.arm  | Bin 3725 -> 4411 bytes
 .../cbmc-library/float-nan-check/test.desc    |   6 +-
 regression/cbmc/union7/no_simplify.desc       |  11 ++
 regression/cbmc/union7/test.desc              |   6 +-
 regression/cbmc/xml-trace/test.desc           |   2 +-
 scripts/expected_doxygen_warnings.txt         |   8 +-
 src/ansi-c/c_typecheck_expr.cpp               |  31 ++++
 src/ansi-c/c_typecheck_initializer.cpp        |  41 +++--
 src/ansi-c/c_typecheck_type.cpp               | 144 ++++++++++++++++++
 src/cbmc/cbmc_parse_options.cpp               |   2 -
 src/goto-diff/goto_diff_parse_options.cpp     |   2 -
 src/goto-programs/write_goto_binary.h         |   2 +-
 src/goto-symex/symex_assign.cpp               |  28 +++-
 src/goto-symex/symex_assign.h                 |   6 +
 src/pointer-analysis/value_set.cpp            |   5 +
 src/solvers/flattening/boolbv_member.cpp      |  76 ++++++++-
 src/solvers/flattening/bv_endianness_map.h    |   4 +-
 src/util/simplify_expr_struct.cpp             |  31 ++--
 24 files changed, 343 insertions(+), 68 deletions(-)
 create mode 100644 regression/cbmc/union7/no_simplify.desc

diff --git a/jbmc/src/jdiff/jdiff_parse_options.cpp b/jbmc/src/jdiff/jdiff_parse_options.cpp
index e84e0d96599..2175971a882 100644
--- a/jbmc/src/jdiff/jdiff_parse_options.cpp
+++ b/jbmc/src/jdiff/jdiff_parse_options.cpp
@@ -40,7 +40,6 @@ Author: Peter Schrammel
 #include <goto-programs/remove_unused_functions.h>
 #include <goto-programs/remove_vector.h>
 #include <goto-programs/remove_virtual_functions.h>
-#include <goto-programs/rewrite_union.h>
 #include <goto-programs/set_properties.h>
 #include <goto-programs/show_properties.h>
 #include <goto-programs/string_abstraction.h>
@@ -296,7 +295,6 @@ bool jdiff_parse_optionst::process_goto_program(
     remove_returns(goto_model);
     remove_vector(goto_model);
     remove_complex(goto_model);
-    rewrite_union(goto_model);
 
     // add generic checks
     log.status() << "Generic Property Instrumentation" << messaget::eom;
diff --git a/regression/ansi-c/arch_flags_mcpu_bad/object.intel b/regression/ansi-c/arch_flags_mcpu_bad/object.intel
index 2ba432c93b368d71d39d3e3a6816782f6c234d46..b9bdd513da6e369d12ca18ef3c5c6d7624a48114 100644
GIT binary patch
literal 4471
zcmZ{odvp|69mns@h8eKfv^F9lF_vJ9Vh9@`-4=>;V_%9x%Rp<XcAVY0*-W!Lvz-Sd
zR9mICY6}ew?*yoow=HP35`jwlw~zXMKTdhS1QH&{bDBT&d*|NWo%Kl0fv`I>pWpZQ
zyuab;d(-zQQ^~}vYcZnLHTiDnWtow8vu0qs4xxl-H+9%~Mr!`8ii^{-_^v*0JB%dW
zu1Vs<;o4=c*JV37!?Hb=4P38>)V`p$bh-uB5@wn+X0|IVwghGv_}NaUC7UT^n{#&1
z8D^&8SBuAT9`k+JYcU<)ZqBxtUbfTd$eTIeC}fMFkufa-L&MZ#LFhR~&{Je&)M($%
zIn2r|CE5U8W?MlgQO+teT5;#`L{nDWrS{f{+YH+YIAl+vXnJOW1<dowXnZqf->9rx
zD8fk?q3@{~(<39&S@NE`J<*Q8$;aN8E4n~1kLcHphQYDFRZ_qmscFi(jvttyCt&ye
z&(>r+LBOTD>k+)VchxzW(9Q?8)6Ctn14JnFShF8^2$??@H`d?qcO}VThihxOFE>7~
zw#@|L0|%&SSv)p|+d=f3CfSa~x`|%jPsP(l*|b(0#pHvQ>3L=k(Z@v+xgMf1-(Jqh
zhuUK|kLQ<f#N`jaR0>btMFM4v(o4;J$jF4>D7Qfd_e4v7<Y!8Es?FfSv_rHhFK$T?
zePX*-J6=mSyj3%u-&;Ele?FSi$8igUTz^?LjP?f>E_mqfg+@F8(FX+jG9r9gCDR+Z
zBn9#0QAE5!9i`RX%tNTvPx`BpY%2vQ-Sm#aRlG@?GN#YS<lievZu;ioYndvr0*cab
zi_9|}%ZTDJq7K9IFt_}1Ve1xQ>(;+0$ysGv37DBoZW+23+RUQ}3k=yGQHKB=0&vQx
zjO*qJ`9z!J2JDH@%oF{S!p2nC_|!^S63x6OEX(GtCJLeXZ%Ps&7ln{+h-~ZAqDRvW
zi0c%sZYr6&B_^g|=FzQ&?HdkThM4l~kEmOqWD9q#MVOr~T$>=l$xF&iL@dHjKNX`@
zB`B(hQdt<H!A8_mK%WA-)zW8-3DK{W9vq9z&3v(@^rca5gjw8ct-kG#N|JYHROalq
zA!<7vwqpl9@NB$RhoGktj*Y<0+8EO$k_V?Y!tzFyv^L%@oVr6eHT%~}r8Fi-KHYIL
z_I#C3ey8gNyv)n~oCNhG{FyUGw#1!%6%R_@qq^oc@D9tGen9k33jy<lTX+3INs2j$
z?v+W?YUhx78)7OP)*To@r^igo=wdua8(?^YN>Yt!L2DQ8eCAh5rTWH3?zEqXfvVi$
z5iWaj0>BgS<Zes9C#T;#QLDR82%Ib;K1}bQ%L+vvZhmD?;<H5m+-h1LhseVGoPIwp
zMy<<lLb58KH1_!+8f6L>QunQoiK;keSeXAl+*=Pd>*1cp<67$L1*<Eu6|*MwfYA8h
zFO?axG<sv;(#%52M5!1de{MwW1-=)~F3jorT&-@Ape+8Ak}P5PD1rP%kuwh=#tXId
z!|zaS@%;JlYtg2d6^lh(WCl0_M$}C}ZvwjU3nDR(h{TL7HBXe2M^49{ugZx$Cdz3!
z4cuwqmW<Kr9u+bZ0>wx0723q>%3>Yli>qQtKBEjASZJv`N$Sy6>WI1upj9ea`F2g?
zmxQv%gt7;#ls$GVhN)6ks^+q^V;~-bv^hqD{$+tQg~F1vVg&JOHrK|m@oKht%+`Xm
zmd7k3Fj=9jSt=7#G<zwAs8Yrp%QhVcCmmRqz`6vMmD3qg+aVO?{;9O`nH3EWk=l+Z
zwVkkNA+@AqTO7~FqG`C9$8p{Qx((26fZ93zaX`BS^oBUDE5hZ0vpKG7YYZn(kUTTH
z0NV=KR_<*<c<Tsn+oZR-s6w3cvFEG2T^6-%WdxlE?mWl20#_6`StV(KD;~KPE<VkU
z0CfbYIZrg`o}l@{)!9;9C8K^{j3_%eN@gD*eQ4bPBP0}0C&kmlbSZ*|@Af1{lT<hu
z1Mop^<21yoF`^EFFo;9EahcH2Ej;S^g;JjX(yi{JF-CQiT(5jo9|i9y+*)qwI0By(
zn&fH5z9Og6lbA|Ru8HA<Prkvrv32n(T?5P-9_X(MSx*UBO)@lM+CFtWhNx1+PxW%|
z90%(-SWjE}*Jw`vIz?bsP@(J@`a9+J>RMevqw3=KXzUwQO2z{uwSumTS*(mw-V5ts
zWgSxSEKFRd)jh`zU?2J>{fCk)Ti}b<x99<?f16IypQrs8(l1a88yH(j;V71~*${(=
zwe%|ba|OG5*o`j^QNF#&g^fH%uf$YT`R#HgSD@qy{2lcoXJR$$mCmlF?<%d8w2D^m
zr8{CYxukTMb{?y*QNY`VAy;`P%;!Ph0s0P}nU^HJPkOqB{#i-#Z7=G3dAjz|i!pkY
z)>3a_Au8=5z+VLZBFC?l_;nJWlU$*C9ld%jE<ZN-mbILDE`V17yvn1oUII7BXl$fM
zl-BYQl<tW}!3MfB#{GZMFnyn4F$p@EW8mLmfp^hP7}*IUOE%F4y`LMxmNXy@ZKg++
z)=FTu(A{ckdi)15<EyJyyMzqTT~+qG4XHtH!n<H-7x!kX^yX!0<U90~(ps)F8U2^(
z-WbhuLkw@cJMgSR^j@&`qGDg6;^04?SU|oD{o5pZyF~AxL&}WuOHX-idWDkhbbpLr
zw2KVyIbn3_?+1K8gziK;?BX4_Thi80kw|ec>=w<ohnw7qs(+a5ru{J{&U>qJH1q@7
z4`}1}q{LS_6kYa=gvwF%Dm@cpR8^gi0OVPDHk<+R42Z8m=3XvypOkrPT;)EY^84KC
zYmv%*bRcFy=BRvx4S+hpb^bu=d|m34`&~L2CH!@IHU_DZX}Mu0Ci5(SX8~N2`k~Y}
zDblw&_I!1rY{nCtxr84{32#UVcga5bG5r_HP?p{s^jwTor6gKK{zuL^z|V2`ehD9x
z@Wm1?j;=v^;ab$_T&?c>3xHk#l=9d5#82o%{eYw&<n$V?KA}zM2%T*7{~d?${$Cn3
z$iC>GH|bnV&x2H(hu8doMK60lrKT8QSS1hAv8n&yrw+6HAf<;ne~OlViw@Gj!)r7l
O(N#+M<uNIY{Qm-Z{4SUP

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{<xI!7JFJ}PS!JWYVh;F5)vAR?(JV0tG{HR?gq~vr!!^mo
z6yF|jWU080X|M7@yA+g}`X@233*H=8+AMl&%8MC#&9I#SA#W-*(=)3wke<(`GVMS{
zRw{PQw|%BCcFQk><yLEuF+}9&)uQRKu{d*fUVTGZ3jeb?ACff}c+z9~ty3U+^It^|
zu;0zJS+3&;CWKNz#D_O!tTGVbQ8o)s-u63nQ8BbDf$el)j&=Zcg`Vv20}uT3?}ry#
zKJp)tN7&m<O_<oUlVU+P5L({iW~qcm8E!w*KRU;DN^*$lAKS_4+eRa_rbGsP9K?I(
zFw>_;5>XG+EZ<%)*(Z7vFVDco)8O$ZU#fdmabY!M!wT!nN+?<DU&KO?fthH9na9OY
z&jJI5Y47m13caE*{ZqY~GD9oO`gLY5zN<`!pHEADI!0hDJE|JS(v_=LtbTBnku)Is
z07j33!=oyjI~ygb;3v8`h0Ot~(6YCqg<8vJ{w4AY>IN0s{wPqzuXtP0^d)Qmv&duU
z+fSv1s>&)<sNvS6XF4S#@?%Ur1(8o-<j+#9J1Ewj?}<F(qs1u9f-vpujuUC<L0oMk
zFl^rlp^~vWA*mC9K7r`Z5&AAd-~A7fpZ5XuUB}bV5&35Bao`?D?&pbn4{<xLiahQC
zlHB>e=mI|?;rAR%qt}JgE*evh0s0uCbA+Bt==|SBo_0KxW})l%YEK<K_h=eADy5Pe
z7Aw-I<BtOVDB|Z4zMJsvvF7=&soiyO_mMR42bf2Ic?6jYh`ErMJ%1DTPMQ(fu<&pi
z(uYl$ka-x8hY@)%A@3t(b6sXcyYEmMEp8EwtPcV15aPZ-xJ86pd|u3NC~S_Hi}t56
zqcW)5xF3M~5qLiVmk_Wm)<>)*`_foN*R3?f?E}_6WPOoX1!DF7K}^=@{7773ZyK=P
zH5$;p0Nsnwr38I|pb!3A<e`_uGL?w>!09xqbV|1AIMDcDFP#SBX&^3}THj#Q{;_>M
zv^7)zBTTSH1N+iU?1q-<2TcDm>3A4)eC4#DUfhArxKy%n;86#zFEDL)O<Besz9=Re
zmm`M)BPe^)EEzU#@QdON<)Q#l%V+9er3e~E&{|f!D<(VDBu*Po;F6?qAdL&wv$6>n
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<aR|Q0+pt<nvY(lw30XKLi~wpD%8d0rIVxaQ
zfv{1*Mt++qO8r(XYmu<he?`90ad7I%x47OvM<3Y9HKkmHQE1ta2@J^<fXiB1;i(e>
zj#J?fe0+!F42{Pov(BU?<l<g91DTwGOx6_j%2b$_%^<G2WpWQRjvfxB*%L2?dli(x
z3OKL=&ZR_>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%C<pMp~vpsxV>3Rd2Fa^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&<TJ$h+@j#1}Zax0&Ba*cTuAD$-m73U7dYH^9Cvz<d#zBQdih$s8f(OUT?3
zF-Q1Bl1Xi~Q7;ofodD`qPE|gx`0NLKrvAg&hHY_>?R=Zs)o2m%p;A+}a<+|cPgqj3
zYZ4CiVN~ba!G`T%gVFbLjJZ3~dhP!O#V6WpAm<v$*}+@2>?`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_bad/test.desc b/regression/ansi-c/arch_flags_mcpu_bad/test.desc
index 5b43f9022cf..2cfda406b60 100644
--- a/regression/ansi-c/arch_flags_mcpu_bad/test.desc
+++ b/regression/ansi-c/arch_flags_mcpu_bad/test.desc
@@ -11,7 +11,7 @@ This tests the -mcpu=cortex=a15 flag that should activate ARM-32 mode.
 The object file 'object.intel' was compiled from 'source.c' with goto-cc
 on a 64-bit platform:
 
-  goto-cc -c source.c
+  goto-cc -c source.c -o object.intel
 
 preproc.i is already pre-processed so that it can be linked in without
 needing to invoke a pre-processor from a cross-compile toolchain on your
diff --git a/regression/ansi-c/arch_flags_mcpu_good/object.arm b/regression/ansi-c/arch_flags_mcpu_good/object.arm
index 6593905c6b48c9f45b19be6994f3e27a98ffc1b9..cfd8751c1893a141adadddc10de171d4a5a07646 100644
GIT binary patch
literal 4391
zcmai&dvp|69mnt8Br^oTRSQ;;)Joc-v?1AK%R@_SH<lKq)5^3|v@*`_-0V)XJG0Ep
zLO^Y+6<d^s$eTcj))=4_tfE4XJ+=R<_5HR$c)ua1l7IDk=ic3&wI|1%1KG#S=lA{o
z?(g@zck=WDsm02jWRh=Z9cHCh6KywLV_QLv&`U~3J0aR=tU2R4eqcHQiM<g^;G@%Z
z%^4$DTV$keQ%u}x*!Y@|`mV~gT77s$!z2(XZmA<$yxDh4UWOTYH)962>ktLBo4V~h
zBkEh~J?WC24{WE!^fEa+V40xgu@*n@Y$xk?;>u}x+hJtVaizTt?_RH8<9a>#&ai9`
z7rWkC(zsD=&AA2ET1vO1%}h_J*czCnz|Z8I)=avPY026_u9TjOU#%X?dd&ABqt$eL
zyCu`g;~L$0GwU0LOtEBSUDtvsEw$Rrml%m@uhHhT=`%9<&q@Lkh%%-cM%N?D9$tR`
zG9#+m&>ma5)UbVH9rIi=t_t5|OdYQ4!vCc0UD=|GlrfL!QyNPMUrqniKPn3lbTk%2
z*5187mdTkOR}qgRSE@GcJ;#*9!q9&sUoA@B`zkdpi+eHLZlb?$mhD)qm*_VQP?0<%
zvMAFm)AP)=M4#S>o2T*+L}R|aj*<6wY4r_S>gL}o^AL{*)KVY#m4c*~dhzxbv^g&m
zLG%xbYiIm2#`B=nPshIxW%cQyAQHbmQC?gh*|?50Tt^aSX7wpryh+%)<t-(_eZO8W
zZGHGvs^2<G|HuH<>Zjo{Ej8=cis=<{-JzHmM98?L>Dol`_@W@<HAK9Ih@?5x9luS)
zy#1d_0$xST)E&Q7l6dnPolI`KG7+%A3Me$gEi%t^EF(<ZxOxTrE8x#=NV{&HkdMxD
z+<>hrnR%jrOoW_+kaxZyi@b$bxn<eB2}Eh%^)DqczanKusDc}ut;Oe%IeQ~=3T7Vt
z!;8ydYfyE3HOJMxP_UOfY!Tt+3Wu%#P!e}nu)KmNlew28w3@0l^QglDLo1J~mjS#C
zU|XXWPjKzpv{+?vw13lP-rg4LChdI@9M6Y=Nr1ZQ=#P~PTTX{$ons?8cMIC>A#E^n
zvvekNItT%S+|fMYXufc?;4eyo523J5QVZW!l6)9&U-QpLST(-#E}s%^DV=AAm~P|h
zdEn0j|8YzIM7b62>8nbvwA~^hxAU(`g3rS+F8kzlYCGMwV+U(d`3+ip5h2M%yCMQa
zp&*gF5NMZ5+R44b$9=-b<g$ZM`+eskx7KL?AKB+XI|tb*u9?r(uFX}=p-(Z1Kh?z7
zCu8~n(eD?57Yic`WMENaT78Nv-Wdt*u-?E3avn1+qlfX*+KG@mRkDCQAUF>S155s-
zRK`$hQt0Brvk_2@3m<bjlKitko`s7~Tl#0R`qG&h*J2nr4+(`bHDlCc*a94})o7ip
zP~_R>R~@J;nx0u;7@$6RnCOr6)5-@}kI!ax4cCRkh+mIotG?6Nvg;TrSTlT)d}v2R
za@DqBVL#!sY6q0=;O2E<{!wB64w=NMq3=gWBaj;3d>m9tZWOFhUeS*U)^fqROR_|F
zF26bvi#e8UIu7PMbX^7ODp-$a_0M%`@f9L-w+IyW4me&B`u{v)J+7s`@FwMZ5>l~Z
zC=x)9vph3<038B!2+$|8`WFFRDWJyRltf3l@&$Tji2f4LPXJ9;4n&X^3kQ@LFbl{5
zAP2Z-Q+Q4b&z;h<sGIbK$o)0>Tf^JX2r4PO0Ne%O+LDPrbzJSk+dh?Sd?Q9Of^P{v
z`-4)QrVGPGvQAGFBy5{<?^Hsa2KzKZrMjE+tbpf4LZ(Xb)eg#Si?E{|Wb+(s18Eyb
zw&+>0vv-i>lLFWCrczFCe*{zBv@txzpfO6kwa3+d;QDz=^FmcYSayD+ROXZH$HMUl
zuQso)SJ}LdgLfP}H>(%1>Z^pRNzqbT6|T33crIV>Rl`v(-;PYfO+Sf47~~BDH_YYv
zLS7)`m42sGHzLtC!O18la_BR{RWDEKlK`FsFtxf#Un7{kLgUTvScu*&5u|MAa1FKq
zvITv-cBU3zC+=P-?jECGhHHFwpzbSZkL0?e5d@#`Hnv3^kH*!bU>sG+t>mjh#Z$sr
zS;geA%$_<GxxFUme$Mp*z7<wV>=b~f;OuEj$3FiI6}p(v#lA-6oWd6*`3&6}0Sjxs
z!Fq8}<~6nzsI5HfU#CLcvz&(GqTIA)MLbK7MJP4$qQZ`Wc8t@$A!+L+tz7z|Z`ac^
z6Vc@Hwqo@Rh-X0jCbjhEXjXroBIz5X<0a8r+d$>q#tZhXat?4QNp7IqBk`)!nh(V7
z2(X<G>TgTQ8>QqPStLU8MtUNGs7b&(Ccp_GPeAhv6h+g=ahvGd@+?0$gNay9?ig(d
ztEZnHYRI^SA|7b);Lt~JsA-(t$JHAE-9X_qd`D{AERAoWqe^?VYsC(*nT|vx%0p4N
zY3K1cWE8Md8ggHBO8GqKBcP8!X2VuV-zMqX=}D!%JX*Ar6V~T8y6^wcP2XoI)F8(k
z1FuU3Ui<qHWFLaG?VwHiP8n#I3^YJbDee61EDmM6=>c^?8~?#a{A8xpw~<|Re@)z8
zqxQJB9|87r7keapP{Q}p^GbX5q#=gxAUzbJd2R`NBhGj{I}m#atV5`UAzD5qb&&5u
z_xB|FMT!1C9aB0g4;`uUJRhRuMS3K{FWN<hhp19Gevbft1VV>V#XsOxJR)iP=--t@
zB@1Gs91+F5p9dbMe0Gk|-4QZ2ORG9McLTi}XmUUbeTk#d#D>hQD3F)v#R#INhQq;$
zM}zXo8_Bo`=tV$ZhTb1?y$7Y<)@auq6haU2z%PeF57Ir6C~~nXQ+^Mqd$`meNvW?$
zsr#tZDzf<sy%eF;Xf5yUwQ?^3d<kI6Tc_^Fbf*3j8R0OGu!-`no6%izGT~nkeu^e5
z*WD6XY(Jx&IQ|@_+P(O*MZm%bnx9isbPY!QVLB!GAN<5IQVvskg!5->siSxmczDn!
PB>WbS*7&+HiOKU{4!#ca

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<<J@I??nM%Hu#
zr^CuhyGDP>90-iERjC>So@c`;Ex+C@RRv3Fzu@f!GZ1X@pOhRVF!dePFcz;|wc_a~
zRvAgvhPHb7a>EIX4Z`<WO(nnCJL((h#du|NJ|Zd}LMD8sPid*b{8;#>{zd7A(RWiR
zL@l#9Wfe_ds>n=3tR`x$AN`M#dnEFIlFSxocf7?-+m^l<UO&@YXF9GehM4}b-JF7F
zB$9Gx!SsD|nCa77@bFY=f@xOZY!K|@i?p<&<?nh=c^LMjK`npxuN4HnI)slu=k299
z5KR9B-P^V|CF7u_r{jNy(5FX&*tB!a;^GB}#yN!H9D?vkp-<5=_mEqk`nQske!o2-
zcI(q`aed}Y{WH6{mcA3WY59B4E2dvA_D5n;5E0vD_nd8JPbLKx&%)waSY+*y?#wK*
zdEdX3-2A%Dyv*-pHtS3?mT+yybX~+5#4{kCk;Kmu@qQwH?w?8y(IYSN5Bx#t!Uu`H
z|8z5KS(H(_hF1~3>Doq=ikf;F{L_;EdE!4v{D<CGauOLuDc=^MA3WI%Jt%9(2xTGG
zYYfs)0)0}VI|x0S(AmE$xw#EA1!MM!X6T4Ko_hk^6OucJxH;l>-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<R-)!xHxe!Yv?N&!3gC
za-A1Bz2HzYX30Zqj9$=a8stMDAClz9h`f-<cf~>{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`<em&CxrU|-3RD0*+J!K`_hh7{dhG3j;{FR3^@TUGYFafWwO5<
z_MiH#LX)mTjyl_R<Rql|RxcMi*IIfRTYg0un=q~z3XQPn3)40n8z=dS@<#fK!scjg
zmS+oe>=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<yp5bzP
zK><705@1`HrD$)9vULsUYsgkf=;a<Q;}X=MU=q}gpdO$lK$&}eJj^z{!gE;Lkf7^;
zT?eevre)R<$$wRy+epqR4`2gV-b~9Svv1u<B1^K=9J3@Bn3_6*jEtZ{pY5v>CmSic
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#?j<P)vIMTvW>SA3gd`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`bTSIJ9whiI<a|d{2TfE~v=?y$7^CpmEv6)4O<^{%VXJk=T`T
zMBLq9b*<<Z*^f9nd|VXW(b(3~KjuAX5+ht&h@XL>h${UxZqPu%fgIse`aZzlG@Q*5
e&UZ_Eua<wE|BQz|emF4}UByooT%NQW@9e+kHAVse

diff --git a/regression/ansi-c/arch_flags_mthumb_bad/object.intel b/regression/ansi-c/arch_flags_mthumb_bad/object.intel
index d1b887e5bef2cdf13bb5c320d8bcbcf3ddfe84aa..e6a6b5e2bd53766848cccf6f1e732e61f001889c 100644
GIT binary patch
literal 4473
zcmZ{odvp|69mns@h8eKfZEZwEVl2TH#Sk_?x-Asx#=aDXmVwq%?Kr!0vzcahW;-(r
z323X-);>r>!#e?L<!uXEtwf;G{_Uf_-;Yz?FM))|@to!l{oc8EcV|74b0F-_%;)$0
zJ@0RL>fY2n%2YBj<64Yp@kZY*dKqTq+>9C6u0tpx+D+|tj**&wtK#Cc48E(&*$yMI
zcWM&&aJY7v>vh^r*05}kWdhghCbciB%^hx@H5b!OX*1JVEHnpZG4L}TPID%m&opK2
zpre?chF{Gd%X-ZBVXxVAe7h;rY<igvqdjM4eIt+C@@XS&S_GzssmFq%=NLhEfss+8
zeLL$gE4`Fx19X{f1sy~=tITM@oyTL18F81|TO)2WY$xE5J+Xr6nRym4&nKht&6s_o
zGH$*AH(`Xnucl3pj7WFM`|9>s8~!Gr_&~Pc0>M0@UpE>C$NpAH0(YdQG2=RZV1gcl
z-48xflj#5fm*UqWeDU|xIq9OE3v8!}J7x!nQPE>fe&8W!{#@Kxcf;S61cx22t>wPl
z_=4Ix6NC>Ppr&Q<=ooH0(Qle$I~MCAdR;#iPa9>^T5TAU4_l_^ncYMm7fR%Mh{k+-
zIU^rwi`+b(U%nBSKl*YhJUJIBlrc&zHFHHqCj3UZ4KlbVTIypzQ@WC^1{bCsqK!Fm
zON{6f+qBy8TB`o-n(6%B+Hv^v@vJ_MTOj26%c^0tJ+N@WLw7GUq5%j$Akdc);mazS
z-oPa(h$oLC;tlF3Eq*f(p;kBPuS%k|6rfb&y9!tF7Hv$MJ|mNVuOztXn}@GuD$nvL
zOT#TN&vYy!jK_#N49mmZ@+XC@TZFA!|Dq&jm2JgfW-_^D=vrtqha$`~WPd~*0&obx
zDWlS^n<L~?t&SV8CyHi{=${rgrozT&R>_iR;x%DeHg7gj2u*)e5(v2{gj9WKTb~v_
znyN=!r)cr1Wa^fPn7o-ozZ$l0IBXeW%CkSBZh?|5+_h$5cDitFf&?cnDKinV5I_A?
zgjSWHup&xjVTcABQBMJV3g{L~pE0J0j;-|ISY&SIOEsl0jdCN*;$CZYt$$P!ygS1(
zXSWSe+iABQJLraI<Fz<~o{Tv*0yk@8M3YD!oZ1M>8&%TMaJz8o4&l`7Un`Z;m>l|a
z$H~a^RX+J0t{3n!FZ**6)RXXM&KTJeclK30D0z?Snp@91EMxis(LXB$%oA?i^#>&(
zCLy|4CQYlIL*{LWsBl<UU<4f=GcBW&@f>Y{;SDNDHlzftO}O*9Un!O98ymXQb|M0*
za)(E_?8ylLPr#GAE&ZOXe(yvrexDFHSwwu8-anV+3q0KX%AVNgiT;Jvv^)-xh51?i
zeq0P&m*0eBRX%C#i$gTb6fPw1TOScsam=uA0{C!mJ=Cm+dm4{xsjnBTuEbW%n&bmQ
z<Ac9cX2{a$jetut3n>$&VifsvBWf@3y>ND6R@dih@kN5N_)kirgyEwE@)w29JcJl8
z)KU+>OSQ%G=fkf>n<7>$7Iu*t;0PE|Hvzo~=!P$e#5^JrGq%(`VNM=79eKVgC-Rsm
zr{y$or-55CMvFfxWX1%FkKik`k=K>Q+R2xDB1k@?3>;W!sXIyX(H?a~?E$DqC9B@4
zY50mz_LxxiV3o4Rjzut4%1YH-mUaxpV~{q-sMo(Lkfu;ra#oBWUd`s(2sT>HHjmj_
zkk;~;r3EG<lr>3ZVv1%iMG#fWm}A+d<KUzN>k?R(z_PMBLu%WFqU=AF7Cy7W;UQAn
z9;UVf7A>Tfv~P>z`B*d!H~l!yTR^t~x(!e}t3M8Cr-0rN#dU_b9B?+rb#9H|<Oz~v
zW+z}<0o%&G%?ocG;cct*HXBxmb3XEXmAA{nwylhy^T3_wI9K2b0w=2^C2)l!*TO}o
z*%6?Q05#`{dfgK=U${D3imPPQ?~4#+2Zzb*1EdeF8(@SK#nTD#^e|nD;NiPHvC$-1
z9E<??Ah&TEV$~Q?2SFIbA>Ob|Xy_6ib^k&s&wuGw*U<>0I!dlrKB|v`cNA_dw{#qV
zD}*L_nz66Rsk8!9X~midPWa>-tP5KguhKQZtl@$Fx{&pxkku$dBc|<>$0LX;Mf_AR
z_s(&!j)V1-rGJBF^>0!HW+fHMo~FN3Zm+J@l{Bm_evih!MWtjsK$0uzx`@TfDCNDd
z4p!D770<xLbz1ycZUFnxx9LBWMA-sgw4S2}sQx^iq`yG>F{EFl7B(=pio#JWXR{#&
z4{NC&`f~-_d$9{&9HM-ClM5SpmR^adsPfz8O0Gc375F>qCC<cZ)+?P|P2W>mDrpt1
z-b;5xXmUwuH|-o&Un7tA4MVQ-PBE7QeFx|}cxGOf^gik78v17?!MDAz@8#**M=wU`
zRa#5Eg@vfJhX8*O_=_CBR^r!5d{%OW>UH$$wYdD);9J&m=D7e~1@J15#(D|dAfvI7
z9#LA#M^LIe90eQb&ItGaMZ@%chQ%c4V2*)*7xTP}cEZR`7+JE3*6aP;5VoWNX=pP&
zs<c!BvxV+flhdO=h#6m9wb~_QfbOcY-(^S*auePKL%X;)TctOzNF(2&r<9g*oyq9G
zLia{!o?FE5#=8U0Dn#!EYcDGHRVoht<FN(gyU@Q)qPI)*4mzaFD8KZS*QQq~*-rOI
z_yxPb@Sal)PyPLX?}yNxXop?A<918h8Y&Vg4u;*L+4gXgJ5luylijpG!o+!RRgQ*!
zK>Go0_@0#b8i%6Go|aHKs$QdKB8;l4^AUg?E6;{AAf5s7b;#VyW$u$QZ;h(lCscl)
zTYWuLxsMJ+EXW*{kFWty2e{53NS$v;opQfRCBlTiLC;1YRWdENn2yLi3*cD*mn45E
z^-T)(ZH_!&T_~IJ#AYtxM^eI@Qo>!bkA6)5g))?-_a;3TAyp{}SCRjba}Mxx9KK(|
z2PJ&5go~qVkY2bJH9S|VJO2Wp7XYRFwLbO}I#E9$=?6KzMyrcy6WWVTCj1|dLwNr$
zjT&TM^v_##E~e)}s?Eb|e!#+)y`NH33^1&c2kF@4fAAB>EI&x;Va}hTrQW84H1O~m
PO-Oi^Qhs?%5+nb=9P%%4

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<aS=*@o>
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^<K?Y``6=oh6
zLp=)&6sEny+Z=jDVfv?fHD!iYnDy(-TzprV4nLok`gDxISawu3jHN4AtyulwDkEt?
z^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<z
zMrhc9QG;5>>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{laR<H(~9Twh???wYcUJ$zA2
zHZE5Vg+^HRrCBm;+~60*8_GoiqL$Cpze*7_jG(owcvnnzs!5zSp1>tZ<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;<n<VoIlKHJOBGKfc
z5_)1!no2mKG#dRLP`L+G8dJ6GlcZ50jW`6~<84?iCE3r+(S$6V5=IC$3uVUoo*Wf0
zt3cSOU?acH6s3NvmbFM&>Axc1=r}m_<Xc?tpQ8`#<eE}0!YH(C$OMMu3czJ8t?<+d
z0SBtu5PW=x;|z_*CbQ0@CFJ2=I0KoSflSsEb!RHf%VrQ)*)q8Y8b=S8((H+s!n+De
zU<F)Q0ryfONt%p6z67aV60B=>l{{ZdsjY}>u067Q?SV9PLD}<R2)bdT5gY)i2SBQi
zI_q;i7@5>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<u$%W3?1=<=<
zpG|WC1K^%pFMSVaXTgHAV8Js||Mp@nyMZLeBab9*h$KD>(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--E6G<ku)keKc0CfVWTRBzvxDv1*@R|A#V;i=`LALX4YFDF0#D_{v*~-~AzCB?{
z)vii7)Yqaq-wrlx2OEsOmt)M`k=ASfFDO3IUIRJTK+X={s%2k^zw{&ivO2GEgqz?$
z#_aLoo61hO?y<gC_>P1G?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_bad/test.desc b/regression/ansi-c/arch_flags_mthumb_bad/test.desc
index f163942b27f..2a1c9d3ea88 100644
--- a/regression/ansi-c/arch_flags_mthumb_bad/test.desc
+++ b/regression/ansi-c/arch_flags_mthumb_bad/test.desc
@@ -11,7 +11,7 @@ This tests the -mthumb flag that should activate ARM-32 mode. The object
 file 'object.intel' was compiled from 'source.c' with goto-cc on a
 64-bit platform:
 
-  goto-cc -c source.c
+  goto-cc -c source.c -o object.intel
 
 preproc.i is already pre-processed so that it can be linked in without
 needing to invoke a pre-processor from a cross-compile toolchain on your
diff --git a/regression/ansi-c/arch_flags_mthumb_good/object.arm b/regression/ansi-c/arch_flags_mthumb_good/object.arm
index 6a398a5058be91104beb8926a8071eed71ac89b2..9e725a7a4a84a4cf23a41673a91003e9897c5c2d 100644
GIT binary patch
literal 4411
zcmai&dvp|69mnt84YNcmi!D`J!8WAWRtRAOfmA8QrL<~sicE`Es>AHg&F+xhneEIh
zB!Hq~Yqd1Q@=kbFQv%guts<a3wSViezTc1Xe!o)mkpJ|1=ic4D>p2{A4rF)c&gb|2
zJ@1{YeK`G)HihI$p5unhCkAaSyMdE)nVnfd^Z~lkvBNxx{Z8v3L_Zd5&U$VTT5d?<
zZ^lx%bTZzYHN&0~BMnc-vU$rVxR`7Xyt1EVX2Hu^q2sw^6t3RV=@b~z-cHQPl$}E8
zxGk2S%{w8>hGn0%1flP^xnM3<jw?7WBZ+@%sr&HljfRz;--Uao?f6*i`8{Ox`b2Bq
zE3(#drX^!#yUL~3&?<*PHt)7(GsSF6&I$A7%ryLJ^;ynmK>!)87JO^TwsN~>XTiz^
zW)aJZ88hd3Hdj7C8!u=x+VJsRN2q1n{6W*}B*wcZIj+sRiE&du6-v!&DD;LX0PnFa
z-?w^*F{Tlm7(&xPbQU<P7)j1o7LOgR2DlOH-n$_tE}6&zmyup!70Qg<{2Of+z9OKb
z^z<#i&=8h#H@^OqHW$Q-I5Eb}*Bi#_>05smo6eUujKRP6<%}`h7eYq8lQ7Nsixxk+
zWWi!njkoCqWF#T-MBYgZ#^>XIGX4EIgX+og$d;y$yX_xZis$`}hS5=I$n8g{@qtOk
zgnp_wOtfKxeNb4x<G0#up>({SzVqi=cgHMq*33vMmnc<{@xwP#!=*vbFoX<4M$>36
z9|afZ;USYEE6HXd>#o0RDOeM-(sBKD+MKZhMkfD3OYs;qU%inP=Gu<sx=1Q)U4^Zy
z+}4K#{cb_O=WkjHQJ3_4f2DCZUZ<1E-B)geEwUnt()3Eqw_MwdQa+Nn0{#`w|FGas
z5&WsY*F;q#rs<ZqwKhnO_*2f_h##Q%3(OR~IFdLE@L7PT*+y%n)TZ~wDvfJa+b{)-
zZO_YoYvB!N+YawX(PcCKq@_^m!c#W$Ds|jW$92LURM1#GiS}-fyH0_S)OJOga2D~~
z4jJ1Mq^)U|@Nc&8FD4_`5;-;djPht*{mGG2_38|8XW&%_cZqk!eJ|8pDtKsr(HtL{
z$h$3T1tBp$DlE_8e(K}y|D%@TGbt+9^sSM7y`h85*`{c4S$AlLd7oLf*~NO`$2J(=
zmLMHXa|P`I;l~}4Gw+%<vy!3*PAjB3Zz6#el~tck1AQ7keatq}Ib;5WtY<TH^MgX~
zWMN^L`V14$6=QV4Tvjac6!2C1<0Z?tiVUMUAP*7a;XYcufFyl9XDq<FsMGm+_+I;_
zvrk+_n<A08(f;68MS0DA)5bXE&9D_pxAGu-QUu`<5rl=m)T$Md78!lym_n+H0mgK-
z_>X~i44!{VWK%S<-dD@0NM`$^A{2|>(q_oa^(pwu)I{n<WtwIF+(@Di_&(s9J}u-f
z7IKZhYN_^W1@Or*nJm7n0PFNx1#EOh76C5<cp1RQa>nCx_2d#E>o$=gs7GX%L~;HM
z3_hl(Kl>KdA78i-Az!jv;mb)-U{)7Y?gn%>piktC&jGqrK%e}xmZ~_*CmhgABlPEi
zegbH+v|mBm%qm3tD6@g=2eO|#{srN<DIAxjl%5y4Y@Sn|uXEY<${A&noCEC~Xv-S)
zq$SkFh0DAJ|3#a5tJ$oRWO@}MpKm7iDfFmL+O6KiNTL^@-UM0yW~?bIgxNwE`?Xd}
zNGwukpHx_N>iFQQ_RdKlPeNNq=R_kXn0X<wGGS^Rp5Lq>)ed)f%r=9xna9i#nB_uR
zi)?UFCd;oWh&oj~&!!WYtC;VBb`7*^pmpVp0+L!3nj}o5vlyk*g|#l8&f=hoj*@A5
zndLaj05=HSAQ$HeaU~&ckrXF-u5?@_D5oZzu*6`jhV3|b$9dSEnrQd}83>6tOJpr<
z!A1ouhe8ywjeu;#Gzcf?$+CEQo_Kngu7K0Hwm-fS#ot~&tRVR2;h?K<;u%RC2IFvo
z+}YGERA8j>GsV49g{Xy|6UyUtQO|f@q3YBLuuj0KRkpEu6u*PwORf>Z<eX+-l+$hv
zRIS;hV1;9W$+~gY<n^!#v`swZUlPjJ3T2h}OpdB_?I{IOr!2^Oe#keYs=QMGo&xa8
z)Hc3CbH-OGVziD5eN%<QqB7P|Ijr%4eT_=VSW4R0(JhL_+KA@Uc?%3|;nVqPDkML{
z;fSW}RymrVp+^-&ooH3=QP7S;?%1zO+OtyXH|Q~~tv2sPV?0auD$rsyjLc5UDd5m<
z7O|n3a{F@2g#xth1${54e^b(*ll1lUxYkx3eCdTzn4hCV|A%e`0YkjQJabKaE*E)m
z4Z+9|j66?Kp}pL|2KsM#nw^$KbyOlVOvgs0+D8wJ%6i2TUO{ls@1@rh8N92EB(4K=
z9aXyQTXdrFf>gXwD&9m-Xl?xXCr%Wb>Hb8=bpC@&d~4AgmXVEgU!4QprVNoh1@41^
zeLNgnBz&ucZ=+|mw%SQhbmdlhK%x0w83$H0I1e+#9suhA%3wQ&vp6H^q#wEmBzlKL
z@1(=pjOxL?dJ@`B$qsr*;g_5e!)r`A+5ry%eh5N$p@4Vu0^TEOFVeqgscIBN9q$o!
z{B3S{7v)244;@g**tG20j2i%Y0O+RgNTGuqjq<%;MpkTFgY>+Ds4L%S%>B>ibsp67
zpuPmbd%55tDcDduZb&HI$1T4UDIKCa6f-hg)p@)F)E!*weyR0ksda|bDkk#F^nwDZ
z)4DR+#%j~y0*DttT-N?wDe#^MwNnAq*UU~lv6E}~p49M))bOO#AUg9EdQm~tX^13X
z&#Jr=pm;6<dJ)jo2k0!<3)xd;t3ZtJOAD_`X?IBrq8#~~+iE?Do3GMciY+M@23)oh
zua*3@cO<b37ItyjKakMZr0f@I9rZPONnzFLuEefh`Xzub0Ze(%#(zjB7(bF04sr_{
zC~x=MJIii1`eVb7(cP7vohlpk5S@!H;~>@N;m;Q#i%xxqsU=1iHnM~CruP5fCy7aX
ekkTWZzgkcKgdU=yk5_R*qPvvx+l}oQ*#8BhH6A_y

literal 3725
zcmZ{n`;!z`702(L*=`n%lg*kaf*NoWOiY$xc44!a5S%3hqohN&vw8TS?diU|+o7j>
z=<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=UBYv<N_YB(!@US0@
zvDWvL{IFjZd1=AT7qutyky(vGYuL+MrLxsI<V3^O(medi2Vy7?VF(#{6TWp?d1==e
zbj_jADC4nm$r$o|TPokdr~g*z?!uoRd7GQIE&tK*2buoS*^Xz6QKsLtos&|d5eh9E
z2jF8RGYHHvrsrD0$sjZ>OtV5~onSZjr5<jZmJaZAJa@~c3|%si1u3Jr)^w|awZE_Q
z;3ER6XvL48RuGozC_es@cewOKmg%?lY1uZdc-y;~`SQ_h4&R>;dQSSnm~vV*jHN64
zAA53Hzmbl&;fJiIQl8jp_08;3{ABY#DRi#oW*}Rt*8ZvgC<U4KcUoHG(6E_rbA8rq
z{nOjImi<f#HmuK*_1piV+($}hXvNv5l+oTEqh~=ZRZ2`$u^FeDsgcs4=M;pTf{Z!S
zq<j=yR)&XtF1C{EAX#_(ODP~OB&&Gm9~5cmSG=QShJwxgvr>?O=s3~LR9Tc!LWW-v
zf$7;soS>R|0+vrm%bzD(cag2T|EUxfHf&{KW-hzycr&!=;^>qGl2}uZ19)5lzd*oy
z2zc)YN<r$4V_Li|2Htb58E`}%DI+qR(5RnFppOB4OrkppJ&(}&e<+3S2AZ_aJK78#
zlW*i61^1}r&L?hxxLsG20**u?x%)$<3jvOW7mhTe*M(F6sHsPQJ|fWz2)&Tda}#LK
z&(sBV=)yzIptfHvxx%P34}p0|GVdd1FEJPWO`*1dqAhmEI(rW`Lx$)pDda&Q4@%@0
z33)#uGj-o%+WiNb(ULaWP<Q~i0}}TD;T99FJ;BY5af|mg!-d0sfZTgg1Go>seG>Q}
z0hbW)OMg_RiZl~bm+WmujT2vw;a&juN??(IeFVHSQAn)5J<V7p-*+40_JFlVvX&C-
zA!052y)spml#hpYHv_sp`h42s-GJ_v(1!`SoS<K>DXEf-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(bHw<zW&#XJd6u_rDhbAPj#$MsP!l1AO{
zhur-LeW_K;S)?clhODp;c!#VcTMROLBBe>r9Rt%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$i72<r
zel3TaFY;?CrAhSAAw4mI)mN_OHT4=~UW3e+xX^#dk*kdf^lpMuZEfUnalI@Jzr<yE
zZRFR}Y+4~*VXg-AI+)kN+yv%k$=s4KyVA@p#C%0EH^s~?d@{|XY&WWQ64XghUrmyO
zHo<<xXX&pc(HKvRyv|=!yQUVN`ssa@vvEG2igm@Q2)wgY<7|y1(BsHFmkl?&mCw|F
zoM5*}?9;NH&ls$FR{Zw%6OL}21btE5BDL&xj%6mdjcZHrJ{XC3>D|E%YW^twZTzNz
l5Ak&~PQf<L-;nrzt@u;^3mye{w_z;4%elNg{SEwP{{x0`Q(6E3

diff --git a/regression/cbmc-library/float-nan-check/test.desc b/regression/cbmc-library/float-nan-check/test.desc
index 4217f58c852..722f2f63ba4 100644
--- a/regression/cbmc-library/float-nan-check/test.desc
+++ b/regression/cbmc-library/float-nan-check/test.desc
@@ -1,7 +1,7 @@
 CORE
 main.c
 --nan-check
-\[main.NaN.1\] line \d+ NaN on \+ in byte_extract_little_endian\(c, (0|0l|0ll), float\) \+ myzero: SUCCESS
+\[main.NaN.1\] line \d+ NaN on \+ in c\.f \+ myzero: SUCCESS
 \[main.NaN.2\] line \d+ NaN on / in myzero / myzero: FAILURE
 \[main.NaN.3\] line \d+ NaN on / in \(float\)n / myinf: FAILURE
 \[main.NaN.4\] line \d+ NaN on \* in myinf \* myzero: FAILURE
@@ -9,8 +9,8 @@ main.c
 \[main.NaN.6\] line \d+ NaN on \+ in myinf \+ -myinf: FAILURE
 \[main.NaN.7\] line \d+ NaN on - in myinf - myinf: FAILURE
 \[main.NaN.8\] line \d+ NaN on - in -myinf - -myinf: FAILURE
-\[main.NaN.9\] line \d+ NaN on \+ in byte_extract_little_endian\(c, (0|0l|0ll), float\) \+ byte_extract_little_endian\(c, (0|0l|0ll), float\): SUCCESS
-\[main.NaN.10\] line \d+ NaN on / in byte_extract_little_endian\(c, (0|0l|0ll), float\) / myzero: SUCCESS
+\[main.NaN.9\] line \d+ NaN on \+ in c\.f \+ c\.f: SUCCESS
+\[main.NaN.10\] line \d+ NaN on / in c\.f / myzero: SUCCESS
 \[main.NaN.11\] line \d+ NaN on \* in mynan \* mynan: SUCCESS
 \[main.NaN.12\] line \d+ NaN on \+ in mynan \+ mynan: SUCCESS
 \[main.NaN.13\] line \d+ NaN on - in mynan - mynan: SUCCESS
diff --git a/regression/cbmc/union7/no_simplify.desc b/regression/cbmc/union7/no_simplify.desc
new file mode 100644
index 00000000000..34a9fb40918
--- /dev/null
+++ b/regression/cbmc/union7/no_simplify.desc
@@ -0,0 +1,11 @@
+CORE broken-smt-backend
+main.c
+--big-endian --no-simplify
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring
+--
+Although this test can now be fully solved via constant propagation and
+simplification, it should also succeed without simplification.
diff --git a/regression/cbmc/union7/test.desc b/regression/cbmc/union7/test.desc
index 58448e0655b..b33c7528f52 100644
--- a/regression/cbmc/union7/test.desc
+++ b/regression/cbmc/union7/test.desc
@@ -1,11 +1,11 @@
-CORE broken-smt-backend
+CORE
 main.c
 --big-endian
+Generated 3 VCC\(s\), 0 remaining after simplification
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$
 --
 ^warning: ignoring
 --
-This test reports a VERIFICATION ERROR when running with the SMT2 solver on
-Windows only.
+This test can now be fully solved via constant propagation and simplification.
diff --git a/regression/cbmc/xml-trace/test.desc b/regression/cbmc/xml-trace/test.desc
index cf2fe7e8135..dea0223e101 100644
--- a/regression/cbmc/xml-trace/test.desc
+++ b/regression/cbmc/xml-trace/test.desc
@@ -7,7 +7,7 @@ VERIFICATION FAILED
 <assignment assignment_type="state" base_name="u" display_name="test::u" hidden="false" identifier="test::u" mode="C" step_nr="\d+" thread="0">
 <location file=".*" function="test" line="\d+" working-directory=".*"/>
 <type>union myunion</type>
-<full_lhs>byte_extract_little_endian\(u, 0ll?, .*int.*\)</full_lhs>
+<full_lhs>u\.i</full_lhs>
 <full_lhs_value binary="[01]+">\d+ll?</full_lhs_value>
 <value>\{ \.i=\d+ll? \}</value>
 <value_expression>
diff --git a/scripts/expected_doxygen_warnings.txt b/scripts/expected_doxygen_warnings.txt
index 31c3ab6b68e..64e01dc1075 100644
--- a/scripts/expected_doxygen_warnings.txt
+++ b/scripts/expected_doxygen_warnings.txt
@@ -79,13 +79,13 @@
 /home/runner/work/cbmc/cbmc/src/analyses/variable-sensitivity/variable_sensitivity_object_factory.cpp:188: warning: The following parameter of initialize_abstract_object(const typet type, bool top, bool bottom, const exprt &e, const abstract_environmentt &environment, const namespacet &ns, const vsd_configt &configuration) is not documented:
   parameter 'configuration'
 
-warning: Include graph for 'cbmc_parse_options.cpp' not generated, too many nodes (61), threshold is 60. Consider increasing DOT_GRAPH_MAX_NODES.
+warning: Include graph for 'cbmc_parse_options.cpp' not generated, too many nodes (60), threshold is 60. Consider increasing DOT_GRAPH_MAX_NODES.
 warning: Include graph for 'goto_instrument_parse_options.cpp' not generated, too many nodes (97), threshold is 60. Consider increasing DOT_GRAPH_MAX_NODES.
 warning: Included by graph for 'goto_functions.h' not generated, too many nodes (66), threshold is 60. Consider increasing DOT_GRAPH_MAX_NODES.
 warning: Included by graph for 'goto_model.h' not generated, too many nodes (109), threshold is 60. Consider increasing DOT_GRAPH_MAX_NODES.
 warning: Included by graph for 'arith_tools.h' not generated, too many nodes (183), threshold is 60. Consider increasing DOT_GRAPH_MAX_NODES.
-warning: Included by graph for 'c_types.h' not generated, too many nodes (111), threshold is 60. Consider increasing DOT_GRAPH_MAX_NODES.
-warning: Included by graph for 'config.h' not generated, too many nodes (85), threshold is 60. Consider increasing DOT_GRAPH_MAX_NODES.
+warning: Included by graph for 'c_types.h' not generated, too many nodes (112), threshold is 60. Consider increasing DOT_GRAPH_MAX_NODES.
+warning: Included by graph for 'config.h' not generated, too many nodes (86), threshold is 60. Consider increasing DOT_GRAPH_MAX_NODES.
 warning: Included by graph for 'exception_utils.h' not generated, too many nodes (61), threshold is 60. Consider increasing DOT_GRAPH_MAX_NODES.
 warning: Included by graph for 'expr.h' not generated, too many nodes (87), threshold is 60. Consider increasing DOT_GRAPH_MAX_NODES.
 warning: Included by graph for 'expr_util.h' not generated, too many nodes (61), threshold is 60. Consider increasing DOT_GRAPH_MAX_NODES.
@@ -94,7 +94,7 @@ warning: Included by graph for 'irep.h' not generated, too many nodes (62), thre
 warning: Included by graph for 'message.h' not generated, too many nodes (116), threshold is 60. Consider increasing DOT_GRAPH_MAX_NODES.
 warning: Included by graph for 'namespace.h' not generated, too many nodes (110), threshold is 60. Consider increasing DOT_GRAPH_MAX_NODES.
 warning: Included by graph for 'pointer_expr.h' not generated, too many nodes (101), threshold is 60. Consider increasing DOT_GRAPH_MAX_NODES.
-warning: Included by graph for 'prefix.h' not generated, too many nodes (86), threshold is 60. Consider increasing DOT_GRAPH_MAX_NODES.
+warning: Included by graph for 'prefix.h' not generated, too many nodes (87), threshold is 60. Consider increasing DOT_GRAPH_MAX_NODES.
 warning: Included by graph for 'simplify_expr.h' not generated, too many nodes (77), threshold is 60. Consider increasing DOT_GRAPH_MAX_NODES.
 warning: Included by graph for 'std_code.h' not generated, too many nodes (78), threshold is 60. Consider increasing DOT_GRAPH_MAX_NODES.
 warning: Included by graph for 'std_expr.h' not generated, too many nodes (245), threshold is 60. Consider increasing DOT_GRAPH_MAX_NODES.
diff --git a/src/ansi-c/c_typecheck_expr.cpp b/src/ansi-c/c_typecheck_expr.cpp
index a53b6f32343..cf3c2ea9fd7 100644
--- a/src/ansi-c/c_typecheck_expr.cpp
+++ b/src/ansi-c/c_typecheck_expr.cpp
@@ -17,6 +17,7 @@ Author: Daniel Kroening, kroening@kroening.com
 #include <util/c_types.h>
 #include <util/config.h>
 #include <util/cprover_prefix.h>
+#include <util/expr_initializer.h>
 #include <util/expr_util.h>
 #include <util/floatbv_expr.h>
 #include <util/ieee_float.h>
@@ -1105,6 +1106,36 @@ void c_typecheck_baset::typecheck_expr_typecast(exprt &expr)
         expr.set(ID_C_lvalue, true);
         return;
       }
+      else if(c.get_anonymous() && c.type().id() == ID_struct_tag)
+      {
+        // we also look into anonymous members as we might have wrapped a
+        // non-maximal member in such a struct
+        const struct_typet &struct_type =
+          follow_tag(to_struct_tag_type(c.type()));
+        if(
+          !struct_type.components().empty() &&
+          struct_type.components().front().type() == op.type())
+        {
+          auto nondet =
+            nondet_initializer(c.type(), expr.source_location(), *this);
+          if(!nondet.has_value())
+          {
+            error().source_location = expr.source_location();
+            error() << "cannot nondet-initialize union component of type '"
+                    << to_string(c.type()) << "'" << eom;
+            throw 0;
+          }
+          CHECK_RETURN(nondet->id() == ID_struct);
+          CHECK_RETURN(!nondet->operands().empty());
+
+          nondet->operands().front() = op;
+          union_exprt union_expr(c.get_name(), *nondet, expr.type());
+          union_expr.add_source_location() = expr.source_location();
+          expr = union_expr;
+          expr.set(ID_C_lvalue, true);
+          return;
+        }
+      }
     }
 
     // not found, complain
diff --git a/src/ansi-c/c_typecheck_initializer.cpp b/src/ansi-c/c_typecheck_initializer.cpp
index bf82c39bdca..b1937535733 100644
--- a/src/ansi-c/c_typecheck_initializer.cpp
+++ b/src/ansi-c/c_typecheck_initializer.cpp
@@ -530,27 +530,36 @@ exprt::operandst::const_iterator c_typecheck_baset::do_designated_initializer(
         // initializer; other bytes have an unspecified value (C Standard
         // 6.2.6.1(7)). In practice, objects of static lifetime are fully zero
         // initialized.
-        const auto zero =
-          zero_initializer(component.type(), value.source_location(), *this);
-        if(!zero.has_value())
-        {
-          error().source_location = value.source_location();
-          error() << "cannot zero-initialize union component of type '"
-                  << to_string(component.type()) << "'" << eom;
-          throw 0;
-        }
-
         if(current_symbol.is_static_lifetime)
         {
-          byte_update_exprt byte_update{
-            byte_update_id(), *dest, from_integer(0, index_type()), *zero};
-          byte_update.add_source_location() = value.source_location();
-          *dest = std::move(byte_update);
-          dest = &(to_byte_update_expr(*dest).op2());
+          const auto zero =
+            zero_initializer(component.type(), value.source_location(), *this);
+          if(!zero.has_value())
+          {
+            error().source_location = value.source_location();
+            error() << "cannot zero-initialize union component of type '"
+                    << to_string(component.type()) << "'" << eom;
+            throw 0;
+          }
+
+          union_exprt union_expr(component.get_name(), *zero, type);
+          union_expr.add_source_location() = value.source_location();
+          *dest = std::move(union_expr);
+          dest = &(to_union_expr(*dest).op());
         }
         else
         {
-          union_exprt union_expr(component.get_name(), *zero, type);
+          const auto nondet = nondet_initializer(
+            component.type(), value.source_location(), *this);
+          if(!nondet.has_value())
+          {
+            error().source_location = value.source_location();
+            error() << "cannot nondet-initialize union component of type '"
+                    << to_string(component.type()) << "'" << eom;
+            throw 0;
+          }
+
+          union_exprt union_expr(component.get_name(), *nondet, type);
           union_expr.add_source_location() = value.source_location();
           *dest = std::move(union_expr);
           dest = &(to_union_expr(*dest).op());
diff --git a/src/ansi-c/c_typecheck_type.cpp b/src/ansi-c/c_typecheck_type.cpp
index a575f3c7150..b06317c2e74 100644
--- a/src/ansi-c/c_typecheck_type.cpp
+++ b/src/ansi-c/c_typecheck_type.cpp
@@ -20,7 +20,9 @@ Author: Daniel Kroening, kroening@kroening.com
 #include <util/mathematical_types.h>
 #include <util/pointer_expr.h>
 #include <util/pointer_offset_size.h>
+#include <util/prefix.h>
 #include <util/simplify_expr.h>
+#include <util/string2int.h>
 
 #include "ansi_c_convert_type.h"
 #include "c_qualifiers.h"
@@ -1073,6 +1075,148 @@ void c_typecheck_baset::typecheck_compound_body(
     else
       it++;
   }
+
+  if(type.id() == ID_union && !components.empty())
+  {
+    const auto widest_member =
+      to_union_type(type).find_widest_union_component(*this);
+    optionalt<exprt> size_expr_opt;
+
+    if(!widest_member.has_value())
+    {
+      // GCC extension: arrays of non-constant size
+      size_expr_opt = size_of_expr(type, *this);
+
+      if(!size_expr_opt.has_value())
+      {
+        error().source_location = type.source_location();
+        error() << "cannot determine size of union" << eom;
+        throw 0;
+      }
+    }
+
+    // ensure non-conflicting member names
+    for(auto &component : components)
+    {
+      if(
+        id2string(component.get_name()).size() > 5 &&
+        has_prefix(id2string(component.get_name()), "$anon"))
+      {
+        const std::string suffix{id2string(component.get_name()), 5};
+        auto int_suffix = string2optional_unsigned(suffix);
+        if(int_suffix.has_value())
+          anon_member_counter = std::max(anon_member_counter, *int_suffix + 1);
+      }
+    }
+
+    for(auto &component : components)
+    {
+      std::vector<typet> padding_types;
+
+      const auto &component_bits = pointer_offset_bits(component.type(), *this);
+      if(
+        component_bits.has_value() &&
+        (!widest_member.has_value() ||
+         *component_bits < widest_member->second) &&
+        *component_bits % 8 != 0)
+      {
+        std::size_t bit_field_padding_width =
+          8 - numeric_cast_v<std::size_t>(*component_bits % 8);
+        padding_types.push_back(c_bit_field_typet{
+          unsignedbv_typet{bit_field_padding_width}, bit_field_padding_width});
+      }
+
+      if(size_expr_opt.has_value())
+      {
+        const auto component_size_expr_opt =
+          size_of_expr(component.type(), *this);
+        CHECK_RETURN(component_size_expr_opt.has_value());
+        // size_of_expr will round up to full bytes, and also works for bit
+        // fields (which C sizeof does not support). Thus, we don't need to
+        // special-case bit_field_padding_opt being set.
+        if_exprt padding_bytes{
+          binary_relation_exprt{
+            *component_size_expr_opt, ID_lt, *size_expr_opt},
+          minus_exprt{*size_expr_opt, *component_size_expr_opt},
+          from_integer(0, size_expr_opt->type())};
+        simplify(padding_bytes, *this);
+
+        if(!padding_bytes.is_zero())
+        {
+          make_index_type(padding_bytes);
+
+          padding_types.push_back(
+            array_typet{unsigned_char_type(), padding_bytes});
+        }
+      }
+      else
+      {
+        CHECK_RETURN(component_bits.has_value());
+        // Truncating division ensures that we don't need to special-case
+        // bit_field_padding_opt being set.
+        std::size_t padding_bytes =
+          numeric_cast_v<std::size_t>(widest_member->second - *component_bits) /
+          8;
+
+        if(padding_bytes != 0)
+        {
+          padding_types.push_back(array_typet{
+            unsigned_char_type(), from_integer(padding_bytes, index_type())});
+        }
+      }
+
+      if(padding_types.empty())
+        continue;
+
+      struct_typet::componentst component_with_padding_type;
+      component_with_padding_type.push_back(component);
+      for(const auto &t : padding_types)
+      {
+        // TODO: perhaps use the same naming as padding.cpp uses
+        component_with_padding_type.push_back(struct_union_typet::componentt{
+          "$anon" + std::to_string(anon_member_counter++), t});
+        // TODO: not sure whether this should be anonymous
+        component_with_padding_type.back().set_anonymous(true);
+        component_with_padding_type.back().set_is_padding(true);
+        component_with_padding_type.back().add_source_location() =
+          component.source_location();
+      }
+
+      struct_union_typet::componentt component_with_padding{
+        "$anon" + std::to_string(anon_member_counter++),
+        struct_typet{component_with_padding_type}};
+      component_with_padding.set_anonymous(true);
+      component_with_padding.add_source_location() =
+        component.source_location();
+
+      // based on typecheck_compound_type, branch
+      // "if(type.find(ID_tag).is_nil())"
+      // produce type symbol
+      type_symbolt compound_symbol{component_with_padding.type()};
+      compound_symbol.location = component_with_padding.source_location();
+
+      std::string typestr = type2name(compound_symbol.type, *this);
+      compound_symbol.base_name = "#anon#" + typestr;
+      compound_symbol.name = "tag-#anon#" + typestr;
+
+      // We might already have the same anonymous struct, and this is simply
+      // ok as those are exactly the same types, just introduced at a
+      // different source location.
+      symbolt *new_symbol = &compound_symbol;
+      if(
+        symbol_table.symbols.find(compound_symbol.name) ==
+        symbol_table.symbols.end())
+      {
+        move_symbol(compound_symbol, new_symbol);
+      }
+
+      struct_tag_typet tag_type{new_symbol->name};
+      tag_type.add_source_location() = component_with_padding.source_location();
+      component_with_padding.type().swap(tag_type);
+
+      component.swap(component_with_padding);
+    }
+  }
 }
 
 typet c_typecheck_baset::enum_constant_type(
diff --git a/src/cbmc/cbmc_parse_options.cpp b/src/cbmc/cbmc_parse_options.cpp
index d9f6a884ba2..33f7a5595d7 100644
--- a/src/cbmc/cbmc_parse_options.cpp
+++ b/src/cbmc/cbmc_parse_options.cpp
@@ -62,7 +62,6 @@ Author: Daniel Kroening, kroening@kroening.com
 #include <goto-programs/remove_skip.h>
 #include <goto-programs/remove_unused_functions.h>
 #include <goto-programs/remove_vector.h>
-#include <goto-programs/rewrite_union.h>
 #include <goto-programs/set_properties.h>
 #include <goto-programs/show_goto_functions.h>
 #include <goto-programs/show_properties.h>
@@ -946,7 +945,6 @@ bool cbmc_parse_optionst::process_goto_program(
   remove_returns(goto_model);
   remove_vector(goto_model);
   remove_complex(goto_model);
-  rewrite_union(goto_model);
 
   // add generic checks
   log.status() << "Generic Property Instrumentation" << messaget::eom;
diff --git a/src/goto-diff/goto_diff_parse_options.cpp b/src/goto-diff/goto_diff_parse_options.cpp
index f0478bd24c4..d0a3b0d6049 100644
--- a/src/goto-diff/goto_diff_parse_options.cpp
+++ b/src/goto-diff/goto_diff_parse_options.cpp
@@ -40,7 +40,6 @@ Author: Peter Schrammel
 #include <goto-programs/remove_unused_functions.h>
 #include <goto-programs/remove_vector.h>
 #include <goto-programs/remove_virtual_functions.h>
-#include <goto-programs/rewrite_union.h>
 #include <goto-programs/set_properties.h>
 #include <goto-programs/show_properties.h>
 #include <goto-programs/string_abstraction.h>
@@ -341,7 +340,6 @@ bool goto_diff_parse_optionst::process_goto_program(
     remove_returns(goto_model);
     remove_vector(goto_model);
     remove_complex(goto_model);
-    rewrite_union(goto_model);
 
     // add generic checks
     log.status() << "Generic Property Instrumentation" << messaget::eom;
diff --git a/src/goto-programs/write_goto_binary.h b/src/goto-programs/write_goto_binary.h
index a770e7bd391..13a3996a9bd 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 5
+#define GOTO_BINARY_VERSION 6
 
 #include <iosfwd>
 #include <string>
diff --git a/src/goto-symex/symex_assign.cpp b/src/goto-symex/symex_assign.cpp
index f533be10855..12277069952 100644
--- a/src/goto-symex/symex_assign.cpp
+++ b/src/goto-symex/symex_assign.cpp
@@ -54,9 +54,7 @@ void symex_assignt::assign_rec(
     }
     else if(type.id() == ID_union || type.id() == ID_union_tag)
     {
-      // should have been replaced by byte_extract
-      throw unsupported_operation_exceptiont(
-        "assign_rec: unexpected assignment to union member");
+      assign_union_member(to_member_expr(lhs), full_lhs, rhs, guard);
     }
     else
       throw unsupported_operation_exceptiont(
@@ -343,6 +341,30 @@ void symex_assignt::assign_struct_member(
   }
 }
 
+void symex_assignt::assign_union_member(
+  const member_exprt &lhs,
+  const expr_skeletont &full_lhs,
+  const exprt &rhs,
+  exprt::operandst &guard)
+{
+  // Symbolic execution of a union member assignment.
+
+  // lhs must be member operand, which takes one operand, which must be a union.
+  exprt lhs_union = lhs.op();
+  const irep_idt &component_name = lhs.get_component_name();
+
+  // turn
+  //   a.c=e
+  // into
+  //   a'== { .c=e }
+  // as the front-end guarantees that .c will have the full size of the union
+
+  union_exprt new_rhs{component_name, rhs, lhs_union.type()};
+  const expr_skeletont new_skeleton =
+    full_lhs.compose(expr_skeletont::remove_op0(lhs));
+  assign_rec(lhs_union, new_skeleton, new_rhs, guard);
+}
+
 void symex_assignt::assign_if(
   const if_exprt &lhs,
   const expr_skeletont &full_lhs,
diff --git a/src/goto-symex/symex_assign.h b/src/goto-symex/symex_assign.h
index 7e3cff721d3..16cf58ecc5a 100644
--- a/src/goto-symex/symex_assign.h
+++ b/src/goto-symex/symex_assign.h
@@ -92,6 +92,12 @@ class symex_assignt
     const exprt &rhs,
     exprt::operandst &guard);
 
+  void assign_union_member(
+    const member_exprt &lhs,
+    const expr_skeletont &full_lhs,
+    const exprt &rhs,
+    exprt::operandst &guard);
+
   void assign_if(
     const if_exprt &lhs,
     const expr_skeletont &full_lhs,
diff --git a/src/pointer-analysis/value_set.cpp b/src/pointer-analysis/value_set.cpp
index bc3d8b56753..37d4192e49b 100644
--- a/src/pointer-analysis/value_set.cpp
+++ b/src/pointer-analysis/value_set.cpp
@@ -784,6 +784,11 @@ void value_sett::get_value_set_rec(
         get_value_set_rec(*it, dest, suffix, original_type, ns);
     }
   }
+  else if(expr.id() == ID_union)
+  {
+    get_value_set_rec(
+      to_union_expr(expr).op(), dest, suffix, original_type, ns);
+  }
   else if(expr.id()==ID_with)
   {
     const with_exprt &with_expr = to_with_expr(expr);
diff --git a/src/solvers/flattening/boolbv_member.cpp b/src/solvers/flattening/boolbv_member.cpp
index 6a78dda8609..e9f3fd5796b 100644
--- a/src/solvers/flattening/boolbv_member.cpp
+++ b/src/solvers/flattening/boolbv_member.cpp
@@ -8,16 +8,22 @@ Author: Daniel Kroening, kroening@kroening.com
 
 #include "boolbv.h"
 
-bvt boolbvt::convert_member(const member_exprt &expr)
+#include <util/config.h>
+
+#include "bv_endianness_map.h"
+
+static bvt convert_member_struct(
+  const member_exprt &expr,
+  const bvt &struct_bv,
+  const boolbv_widtht &boolbv_width,
+  const namespacet &ns)
 {
   const exprt &struct_op=expr.struct_op();
   const typet &struct_op_type=ns.follow(struct_op.type());
 
-  const bvt &struct_bv=convert_bv(struct_op);
-
   const irep_idt &component_name = expr.get_component_name();
-  const struct_union_typet::componentst &components =
-    to_struct_union_type(struct_op_type).components();
+  const struct_typet::componentst &components =
+    to_struct_type(struct_op_type).components();
 
   std::size_t offset = 0;
 
@@ -42,8 +48,7 @@ bvt boolbvt::convert_member(const member_exprt &expr)
         struct_bv.begin() + offset, struct_bv.begin() + offset + sub_width);
     }
 
-    if(struct_op_type.id() != ID_union)
-      offset += sub_width;
+    offset += sub_width;
   }
 
   INVARIANT_WITH_DIAGNOSTICS(
@@ -52,3 +57,60 @@ bvt boolbvt::convert_member(const member_exprt &expr)
     expr.find_source_location(),
     id2string(component_name));
 }
+
+static bvt convert_member_union(
+  const member_exprt &expr,
+  const bvt &union_bv,
+  const boolbv_widtht &boolbv_width,
+  const namespacet &ns)
+{
+  const exprt &union_op = expr.compound();
+  const union_typet &union_op_type =
+    ns.follow_tag(to_union_tag_type(union_op.type()));
+
+  const irep_idt &component_name = expr.get_component_name();
+  const union_typet::componentt &component =
+    union_op_type.get_component(component_name);
+  DATA_INVARIANT_WITH_DIAGNOSTICS(
+    component.is_not_nil(),
+    "union type shall contain component accessed by member expression",
+    expr.find_source_location(),
+    id2string(component_name));
+
+  const typet &subtype = component.type();
+  const std::size_t sub_width = boolbv_width(subtype);
+
+  if(
+    config.ansi_c.endianness == configt::ansi_ct::endiannesst::IS_LITTLE_ENDIAN)
+  {
+    return bvt(union_bv.begin(), union_bv.begin() + sub_width);
+  }
+  else
+  {
+    DATA_INVARIANT(
+      config.ansi_c.endianness == configt::ansi_ct::endiannesst::IS_BIG_ENDIAN,
+      "endianness should be configured to little or big endian");
+
+    bv_endianness_mapt map_u(union_op_type, false, ns, boolbv_width);
+    bv_endianness_mapt map_component(subtype, false, ns, boolbv_width);
+
+    bvt result(sub_width, literalt{});
+    for(std::size_t i = 0; i < sub_width; ++i)
+      result[map_u.map_bit(i)] = union_bv[map_component.map_bit(i)];
+
+    return result;
+  }
+}
+
+bvt boolbvt::convert_member(const member_exprt &expr)
+{
+  const bvt &compound_bv = convert_bv(expr.compound());
+
+  if(expr.compound().type().id() == ID_struct_tag)
+    return convert_member_struct(expr, compound_bv, boolbv_width, ns);
+  else
+  {
+    PRECONDITION(expr.compound().type().id() == ID_union_tag);
+    return convert_member_union(expr, compound_bv, boolbv_width, ns);
+  }
+}
diff --git a/src/solvers/flattening/bv_endianness_map.h b/src/solvers/flattening/bv_endianness_map.h
index d15f3d463b2..ed16567345d 100644
--- a/src/solvers/flattening/bv_endianness_map.h
+++ b/src/solvers/flattening/bv_endianness_map.h
@@ -24,14 +24,14 @@ class bv_endianness_mapt : public endianness_mapt
     const typet &type,
     bool little_endian,
     const namespacet &_ns,
-    boolbv_widtht &_boolbv_width)
+    const boolbv_widtht &_boolbv_width)
     : endianness_mapt(_ns), boolbv_width(_boolbv_width)
   {
     build(type, little_endian);
   }
 
 protected:
-  boolbv_widtht &boolbv_width;
+  const boolbv_widtht &boolbv_width;
 
   virtual void build_little_endian(const typet &type) override;
   virtual void build_big_endian(const typet &type) override;
diff --git a/src/util/simplify_expr_struct.cpp b/src/util/simplify_expr_struct.cpp
index 9a8afc58485..bd46dacf21e 100644
--- a/src/util/simplify_expr_struct.cpp
+++ b/src/util/simplify_expr_struct.cpp
@@ -10,6 +10,7 @@ Author: Daniel Kroening, kroening@kroening.com
 
 #include "arith_tools.h"
 #include "byte_operators.h"
+#include "c_types.h"
 #include "invariant.h"
 #include "namespace.h"
 #include "pointer_offset_size.h"
@@ -184,26 +185,16 @@ simplify_exprt::simplify_member(const member_exprt &expr)
     if(to_union_expr(op).op().type() == expr.type())
       return to_union_expr(op).op();
 
-    // need to convert!
-    auto target_size = pointer_offset_size(expr.type(), ns);
-
-    if(target_size.has_value())
-    {
-      mp_integer target_bits = target_size.value() * 8;
-      const auto bits = expr2bits(op, true, ns);
-
-      if(bits.has_value() &&
-         mp_integer(bits->size())>=target_bits)
-      {
-        std::string bits_cut =
-          std::string(*bits, 0, numeric_cast_v<std::size_t>(target_bits));
-
-        auto tmp = bits2expr(bits_cut, expr.type(), true, ns);
-
-        if(tmp.has_value())
-          return std::move(*tmp);
-      }
-    }
+    // need to convert, taking endianness into account
+    byte_extract_exprt byte_extract{
+      byte_extract_id(), op, from_integer(0, index_type()), expr.type()};
+    // try to simplify this, but never return the byte_extract expression to
+    // avoid infinite rewrite loops
+    auto result = simplify_byte_extract(byte_extract);
+    if(result.expr.id() != byte_extract_id())
+      return result;
+    else
+      return unchanged(expr);
   }
   else if(op.id() == ID_typecast)
   {