33 goto_functionst::function_mapt::iterator entry=
38 message.
error() <<
"No function " << identifier
42 else if(entry->second.is_inlined())
44 message.
warning() <<
"Function " << identifier <<
" is inlined, " 45 <<
"instantiations will not be removed" 49 if(entry->second.body_available())
51 message.
status() <<
"Removing body of " << identifier
53 entry->second.clear();
69 const std::list<std::string> &names,
72 for(
const auto &f : names)
Remove function definition.
symbolt & get_writeable_ref(const irep_idt &name)
Find a symbol in the symbol table for read-write access.
exprt value
Initial value of symbol.
function_mapt function_map
symbol_tablet symbol_table
Symbol table.
mstreamt & warning() const
void remove_function(goto_modelt &goto_model, const irep_idt &identifier, message_handlert &message_handler)
Remove the body of function "identifier" such that an analysis will treat it as a side-effect free fu...
void remove_functions(goto_modelt &goto_model, const std::list< std::string > &names, message_handlert &message_handler)
Remove the body of all functions listed in "names" such that an analysis will treat it as a side-effe...
Class that provides messages with a built-in verbosity 'level'.
dstringt has one field, an unsigned integer no which is an index into a static table of strings...
mstreamt & status() const
goto_functionst goto_functions
GOTO functions.