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

use already_typechecked trick 

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

9
src/ansi-c-with-declarators/c_typecheck_base.cpp
View File

@ -713,6 +713,9 @@ void c_typecheck_baset::typecheck_declaration(
{
// first typecheck the type of the declaration
typecheck_type(declaration.type());
// mark as 'already typechecked'
make_already_typechecked(declaration.type());
// Now do declarators, if any.
for(ansi_c_declarationt::declaratorst::iterator
@ -720,10 +723,12 @@ void c_typecheck_baset::typecheck_declaration(
d_it!=declaration.declarators().end();
d_it++)
{
typecheck_type(d_it->type());
symbolt symbol;
declaration.to_symbol(*d_it, symbol);
// now check other half of type
typecheck_type(symbol.type);
typecheck_symbol(symbol);
}
}