replica
/
diffblue-cbmc
1
0
Fork 0
Code Issues Pull Requests Projects Releases Wiki Activity

Fix remaining uses of ID_symbol_type in dump-c 

There were still a few left-overs that had not been converted to struct/union
tags.
This commit is contained in:
Michael Tautschnig 2019-02-27 22:42:12 +00:00
parent 1fdd2f5e38
commit 6dbdd19db4
2 changed files with 47 additions and 36 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

45
src/goto-instrument/dump_c.cpp
View File

@ -61,10 +61,10 @@ void dump_ct::operator()(std::ostream &os)
{
typet &type=it2->type();
if(type.id() == ID_symbol_type && type.get_bool(ID_C_transparent_union))
if(type.id() == ID_union_tag && type.get_bool(ID_C_transparent_union))
{
symbolt new_type_sym=
ns.lookup(to_symbol_type(type).get_identifier());
symbolt new_type_sym =
ns.lookup(to_union_tag_type(type).get_identifier());
new_type_sym.name=id2string(new_type_sym.name)+"$transparent";
new_type_sym.type.set(ID_C_transparent_union, true);
@ -72,7 +72,7 @@ void dump_ct::operator()(std::ostream &os)
// we might have it already, in which case this has no effect
symbols_transparent.add(new_type_sym);
to_symbol_type(type).set_identifier(new_type_sym.name);
to_union_tag_type(type).set_identifier(new_type_sym.name);
type.remove(ID_C_transparent_union);
}
}
@ -181,9 +181,16 @@ void dump_ct::operator()(std::ostream &os)
if(type_id==ID_c_enum)
convert_compound_enum(symbol.type, global_decl_stream);
else
global_decl_stream << type_to_string(symbol_typet(symbol.name))
else if(type_id == ID_struct)
{
global_decl_stream << type_to_string(struct_tag_typet{symbol.name})
<< ";\n\n";
}
else
{
global_decl_stream << type_to_string(union_tag_typet{symbol.name})
<< ";\n\n";
}
}
}
else if(symbol.is_static_lifetime && symbol.type.id()!=ID_code)
@ -297,10 +304,12 @@ void dump_ct::convert_compound_declaration(
return;
// do compound type body
if(symbol.type.id()==ID_struct ||
symbol.type.id()==ID_union ||
symbol.type.id()==ID_c_enum)
convert_compound(symbol.type, symbol_typet(symbol.name), true, os_body);
if(symbol.type.id() == ID_struct)
convert_compound(symbol.type, struct_tag_typet(symbol.name), true, os_body);
else if(symbol.type.id() == ID_union)
convert_compound(symbol.type, union_tag_typet(symbol.name), true, os_body);
else if(symbol.type.id() == ID_c_enum)
convert_compound(symbol.type, c_enum_tag_typet(symbol.name), true, os_body);
}
void dump_ct::convert_compound(
@ -346,7 +355,13 @@ void dump_ct::convert_compound(
it!=syms.end();
++it)
{
symbol_typet s_type(*it);
const symbolt &type_symbol = ns.lookup(*it);
irep_idt tag_kind =
type_symbol.type.id() == ID_c_enum
? ID_c_enum_tag
: (type_symbol.type.id() == ID_union ? ID_union_tag
: ID_struct_tag);
tag_typet s_type(tag_kind, *it);
convert_compound(s_type, s_type, recursive, os);
}
}
@ -378,7 +393,7 @@ void dump_ct::convert_compound(
UNREACHABLE;
/*
assert(parent_it->id() == ID_base);
assert(parent_it->get(ID_type) == ID_symbol_type);
assert(parent_it->get(ID_type) == ID_struct_tag);
const irep_idt &base_id=
parent_it->find(ID_type).get(ID_identifier);
@ -1183,7 +1198,11 @@ void dump_ct::insert_local_type_decls(
// a comment block ...
std::ostringstream os_body;
os_body << *it << " */\n";
convert_compound(type, symbol_typet(*it), false, os_body);
irep_idt tag_kind =
type.id() == ID_c_enum
? ID_c_enum_tag
: (type.id() == ID_union ? ID_union_tag : ID_struct_tag);
convert_compound(type, tag_typet(tag_kind, *it), false, os_body);
os_body << "/*";
code_skipt skip;

38
src/goto-instrument/goto_program2code.cpp
View File

@ -1410,31 +1410,22 @@ goto_programt::const_targett goto_program2codet::convert_catch(
void goto_program2codet::add_local_types(const typet &type)
{
if(type.id() == ID_symbol_type)
if(type.id() == ID_struct_tag || type.id() == ID_union_tag)
{
const typet &full_type=ns.follow(type);
if(full_type.id()==ID_pointer ||
full_type.id()==ID_array)
{
add_local_types(full_type.subtype());
}
else if(full_type.id()==ID_struct ||
full_type.id()==ID_union)
{
const irep_idt &identifier=to_symbol_type(type).get_identifier();
const symbolt &symbol=ns.lookup(identifier);
const irep_idt &identifier = to_tag_type(type).get_identifier();
const symbolt &symbol = ns.lookup(identifier);
if(symbol.location.get_function().empty() ||
!type_names_set.insert(identifier).second)
return;
if(
symbol.location.get_function().empty() ||
!type_names_set.insert(identifier).second)
return;
for(const auto &c : to_struct_union_type(full_type).components())
add_local_types(c.type());
for(const auto &c : to_struct_union_type(full_type).components())
add_local_types(c.type());
assert(!identifier.empty());
type_names.push_back(identifier);
}
type_names.push_back(identifier);
}
else if(type.id()==ID_c_enum_tag)
{
@ -1633,9 +1624,9 @@ void goto_program2codet::remove_const(typet &type)
if(type.get_bool(ID_C_constant))
type.remove(ID_C_constant);
if(type.id() == ID_symbol_type)
if(type.id() == ID_struct_tag || type.id() == ID_union_tag)
{
const irep_idt &identifier=to_symbol_type(type).get_identifier();
const irep_idt &identifier = to_tag_type(type).get_identifier();
if(!const_removed.insert(identifier).second)
return;
@ -1833,8 +1824,9 @@ void goto_program2codet::cleanup_expr(exprt &expr, bool no_typecast)
if(no_typecast)
return;
DATA_INVARIANT(expr.type().id() == ID_symbol_type,
"type of union/struct expressions");
DATA_INVARIANT(
expr.type().id() == ID_struct_tag || expr.type().id() == ID_union_tag,
"union/struct expressions should have a tag type");
const typet &t=expr.type();