#818 introduced MLK_UNION_OR_STRUCT (should be MLD_UNION_OR_STRUCT) as a workaround for diffblue/cbmc#8813. It uses a struct by default (which works fine with CBMC), but switches to a union when MLD_CONFIG_REDUCE_RAM is set.
Once the issue is fixed in CBMC, we should remove the workaround, i.e.,
#818 introduced
MLK_UNION_OR_STRUCT(should beMLD_UNION_OR_STRUCT) as a workaround for diffblue/cbmc#8813. It uses a struct by default (which works fine with CBMC), but switches to a union whenMLD_CONFIG_REDUCE_RAMis set.Once the issue is fixed in CBMC, we should remove the workaround, i.e.,
unioneverywhere