fix for qualifiers

git-svn-id: svn+ssh://svn.cprover.org/srv/svn/cbmc/trunk@1334 6afb6bc1-c8e4-404c-8f48-9ae832c5b171
This commit is contained in:
kroening 2012-07-22 19:43:09 +00:00
parent 1cff0ffeb5
commit 4b47f10b31
4 changed files with 13 additions and 13 deletions

View File

@ -170,7 +170,9 @@ void ansi_c_convert_typet::read_rec(const typet &type)
alignment=static_cast<const exprt &>(type.find(ID_size));
}
else if(type.id()==ID_transparent_union)
transparent_union=true;
{
c_qualifiers.is_transparent_union=true;
}
else if(type.id()==ID_vector)
vector_size=to_vector_type(type).size();
else if(type.id()==ID_void)
@ -435,9 +437,6 @@ void ansi_c_convert_typet::write(typet &type)
c_qualifiers.write(type);
if(transparent_union)
type.set(ID_C_transparent_union, true);
if(packed)
type.set(ID_C_packed, true);

View File

@ -29,7 +29,7 @@ public:
gcc_float128_cnt, bv_cnt, bv_width;
bool gcc_mode_QI, gcc_mode_HI, gcc_mode_SI, gcc_mode_DI;
bool transparent_union, packed, aligned;
bool packed, aligned;
exprt vector_size, alignment;
// storage spec
@ -62,7 +62,7 @@ public:
bv_width=0;
gcc_mode_QI=gcc_mode_HI=gcc_mode_SI=gcc_mode_DI=false;
packed=aligned=transparent_union=false;
packed=aligned=false;
other.clear();
c_storage_spec.clear();

View File

@ -262,16 +262,15 @@ typet c_typecastt::follow_with_qualifiers(const typet &src_type)
typet result_type=src_type;
// collect qualifiers
c_qualifierst qualifiers;
c_qualifierst qualifiers(src_type);
while(result_type.id()==ID_symbol)
{
qualifiers+=c_qualifierst(result_type);
const symbolt &followed_type_symbol=
ns.lookup(result_type.get(ID_identifier));
result_type=followed_type_symbol.type;
qualifiers+=c_qualifierst(followed_type_symbol.type);
}
qualifiers.write(result_type);
@ -493,15 +492,17 @@ void c_typecastt::implicit_typecast_followed(
const typet &src_type,
const typet &dest_type)
{
if(dest_type.id()==ID_union)
// do transparent union
if(dest_type.id()==ID_union &&
dest_type.get_bool(ID_C_transparent_union) &&
src_type.id()!=ID_union)
{
// the argument corresponding to a transparent union type can be of any
// type in the union; no cast is required
// The argument corresponding to a transparent union type can be of any
// type in the union; no explicit cast is required.
// check union members
// Check union members.
const union_typet &dest_union_type=to_union_type(dest_type);
for(union_typet::componentst::const_iterator

View File

@ -566,7 +566,7 @@ void c_typecheck_baset::typecheck_symbol_type(typet &type)
if(symbol.is_macro)
{
// overwrite, but preserve any qualifiers
// overwrite, but preserve (add) any qualifiers
c_qualifierst c_qualifiers(type);
c_qualifiers+=c_qualifierst(symbol.type);
type=symbol.type;