diff --git a/src/goto-cc/compile.cpp b/src/goto-cc/compile.cpp index e5dec0e6421..247fbac12dd 100644 --- a/src/goto-cc/compile.cpp +++ b/src/goto-cc/compile.cpp @@ -724,15 +724,13 @@ void compilet::convert_symbols(goto_functionst &dest) symbol_table.symbols.find(*it); assert(s_it!=symbol_table.symbols.end()); - if(s_it->second.type.id()==ID_code && - !s_it->second.is_macro && - !s_it->second.is_type && - s_it->second.value.id()!="compiled" && - s_it->second.value.is_not_nil()) + if( + s_it->second.is_function() && !s_it->second.is_compiled() && + s_it->second.value.is_not_nil()) { debug() << "Compiling " << s_it->first << eom; converter.convert_function(s_it->first, dest.function_map[s_it->first]); - symbol_table.get_writeable_ref(*it).value=exprt("compiled"); + symbol_table.get_writeable_ref(*it).set_compiled(); } } } diff --git a/src/goto-programs/goto_convert_functions.cpp b/src/goto-programs/goto_convert_functions.cpp index 6701ae12f5e..eaa4b7cc341 100644 --- a/src/goto-programs/goto_convert_functions.cpp +++ b/src/goto-programs/goto_convert_functions.cpp @@ -152,7 +152,7 @@ void goto_convert_functionst::convert_function( f.type=to_code_type(symbol.type); if(symbol.value.is_nil() || - symbol.value.id()=="compiled") /* goto_inline may have removed the body */ + symbol.is_compiled()) /* goto_inline may have removed the body */ return; if(symbol.value.id()!=ID_code) diff --git a/src/util/irep_ids.def b/src/util/irep_ids.def index d88dd5fb478..287eef5dc89 100644 --- a/src/util/irep_ids.def +++ b/src/util/irep_ids.def @@ -699,6 +699,7 @@ IREP_ID_ONE(w_ok) IREP_ID_ONE(super_class) IREP_ID_ONE(exceptions_thrown_list) IREP_ID_TWO(C_java_method_type, #java_method_type) +IREP_ID_ONE(compiled) // Projects depending on this code base that wish to extend the list of // available ids should provide a file local_irep_ids.def in their source tree diff --git a/src/util/symbol.h b/src/util/symbol.h index 078f80ad7b2..ffb7d134504 100644 --- a/src/util/symbol.h +++ b/src/util/symbol.h @@ -20,6 +20,7 @@ Author: Daniel Kroening, kroening@kroening.com #include #include "expr.h" +#include "invariant.h" /*! \brief Symbol table entry. \ingroup gr_symbol_table @@ -107,6 +108,21 @@ class symbolt { return !is_type && !is_macro && type.id()==ID_code; } + + /// Returns true iff the the symbol's value has been compiled to a goto + /// program. + bool is_compiled() const + { + return type.id() == ID_code && value == exprt(ID_compiled); + } + + /// Set the symbol's value to "compiled"; to be used once the code-typed value + /// has been converted to a goto program. + void set_compiled() + { + PRECONDITION(type.id() == ID_code); + value = exprt(ID_compiled); + } }; std::ostream &operator<<(std::ostream &out, const symbolt &symbol);