From da4ce0e1aaf52b8708ec4b7996e14ed37e962043 Mon Sep 17 00:00:00 2001 From: kroening Date: Fri, 13 Jun 2014 09:46:46 +0000 Subject: [PATCH] use already_typechecked trick git-svn-id: svn+ssh://svn.cprover.org/srv/svn/cbmc/trunk@3996 6afb6bc1-c8e4-404c-8f48-9ae832c5b171 --- src/ansi-c-with-declarators/c_typecheck_base.cpp | 9 +++++++-- 1 file changed, 7 insertions(+), 2 deletions(-) diff --git a/src/ansi-c-with-declarators/c_typecheck_base.cpp b/src/ansi-c-with-declarators/c_typecheck_base.cpp index 7c2bfb89b1..82a4b087a6 100644 --- a/src/ansi-c-with-declarators/c_typecheck_base.cpp +++ b/src/ansi-c-with-declarators/c_typecheck_base.cpp @@ -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); } }