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

recursive structs 

git-svn-id: svn+ssh://svn.cprover.org/srv/svn/cbmc/trunk@4021 6afb6bc1-c8e4-404c-8f48-9ae832c5b171
This commit is contained in:
kroening 2014-06-14 13:39:22 +00:00
parent 2e2c52d62d
commit 7faa9fb124
1 changed files with 17 additions and 7 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

24
src/ansi-c-with-declarators/c_typecheck_type.cpp
View File

@ -493,7 +493,7 @@ void c_typecheck_baset::typecheck_compound_type(struct_union_typet &type)
// Anonymous? Must come with body.
assert(have_body);
// add new symbol
// produce symbol
symbolt compound_symbol;
compound_symbol.is_type=true;
compound_symbol.type=type;
@ -506,8 +506,14 @@ void c_typecheck_baset::typecheck_compound_type(struct_union_typet &type)
compound_symbol.name=add_language_prefix("tag-#anon#"+typestr);
identifier=compound_symbol.name;
symbolt *new_symbol;
move_symbol(compound_symbol, new_symbol);
// We might already have the same anonymous union/struct,
// and this is simply ok. Note that the C standard treats
// these as different types.
if(symbol_table.symbols.find(identifier)==symbol_table.symbols.end())
{
symbolt *new_symbol;
move_symbol(compound_symbol, new_symbol);
}
}
else
{
@ -533,7 +539,11 @@ void c_typecheck_baset::typecheck_compound_type(struct_union_typet &type)
if(have_body)
{
typecheck_compound_body(compound_symbol);
// add before doing the body (may be recursive)
symbolt *new_symbol;
move_symbol(compound_symbol, new_symbol);
typecheck_compound_body(*new_symbol);
}
else
{
@ -543,10 +553,10 @@ void c_typecheck_baset::typecheck_compound_type(struct_union_typet &type)
compound_symbol.type.id(ID_incomplete_union);
else
assert(false);
symbolt *new_symbol;
move_symbol(compound_symbol, new_symbol);
}
symbolt *new_symbol;
move_symbol(compound_symbol, new_symbol);
}
else
{