cprover
remove_function.cpp
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: Remove function definition
4 
5 Author: Michael Tautschnig
6 
7 Date: April 2017
8 
9 \*******************************************************************/
10 
13 
14 #include "remove_function.h"
15 
16 #include <util/message.h>
17 
19 
27  symbol_tablet &symbol_table,
28  goto_functionst &goto_functions,
29  const irep_idt &identifier,
30  message_handlert &message_handler)
31 {
32  messaget message(message_handler);
33 
34  goto_functionst::function_mapt::iterator entry=
35  goto_functions.function_map.find(identifier);
36 
37  if(entry==goto_functions.function_map.end())
38  {
39  message.error() << "No function " << identifier
40  << " in goto program" << messaget::eom;
41  return;
42  }
43  else if(entry->second.is_inlined())
44  {
45  message.warning() << "Function " << identifier << " is inlined, "
46  << "instantiations will not be removed"
47  << messaget::eom;
48  }
49 
50  if(entry->second.body_available())
51  {
52  message.status() << "Removing body of " << identifier
53  << messaget::eom;
54  entry->second.clear();
55  symbol_table.lookup(identifier).value.make_nil();
56  }
57 }
58 
67  symbol_tablet &symbol_table,
68  goto_functionst &goto_functions,
69  const std::list<std::string> &names,
70  message_handlert &message_handler)
71 {
72  for(const auto &f : names)
73  remove_function(symbol_table, goto_functions, f, message_handler);
74 }
mstreamt & warning()
Definition: message.h:228
symbolt & lookup(const irep_idt &identifier)
Find a symbol in the symbol table.
mstreamt & status()
Definition: message.h:238
Remove function definition.
Goto Programs with Functions.
exprt value
Initial value of symbol.
Definition: symbol.h:40
static mstreamt & eom(mstreamt &m)
Definition: message.h:193
void remove_functions(symbol_tablet &symbol_table, goto_functionst &goto_functions, 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...
The symbol table.
Definition: symbol_table.h:52
void make_nil()
Definition: irep.h:243
mstreamt & error()
Definition: message.h:223
void remove_function(symbol_tablet &symbol_table, goto_functionst &goto_functions, 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...