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  goto_modelt &goto_model,
28  const irep_idt &identifier,
29  message_handlert &message_handler)
30 {
31  messaget message(message_handler);
32 
33  goto_functionst::function_mapt::iterator entry=
34  goto_model.goto_functions.function_map.find(identifier);
35 
36  if(entry==goto_model.goto_functions.function_map.end())
37  {
38  message.error() << "No function " << identifier
39  << " in goto program" << messaget::eom;
40  return;
41  }
42  else if(entry->second.is_inlined())
43  {
44  message.warning() << "Function " << identifier << " is inlined, "
45  << "instantiations will not be removed"
46  << messaget::eom;
47  }
48 
49  if(entry->second.body_available())
50  {
51  message.status() << "Removing body of " << identifier
52  << messaget::eom;
53  entry->second.clear();
54  symbolt &symbol = goto_model.symbol_table.get_writeable_ref(identifier);
55  symbol.value.make_nil();
56  symbol.is_file_local = false;
57  }
58 }
59 
68  goto_modelt &goto_model,
69  const std::list<std::string> &names,
70  message_handlert &message_handler)
71 {
72  for(const auto &f : names)
73  remove_function(goto_model, f, message_handler);
74 }
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.
Definition: symbol.h:34
function_mapt function_map
symbol_tablet symbol_table
Symbol table.
Definition: goto_model.h:29
Symbol table entry.
Definition: symbol.h:27
mstreamt & warning() const
Definition: message.h:391
Symbol Table + CFG.
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...
mstreamt & error() const
Definition: message.h:386
Class that provides messages with a built-in verbosity &#39;level&#39;.
Definition: message.h:144
dstringt has one field, an unsigned integer no which is an index into a static table of strings...
Definition: dstring.h:35
static eomt eom
Definition: message.h:284
mstreamt & status() const
Definition: message.h:401
bool is_file_local
Definition: symbol.h:66
void make_nil()
Definition: irep.h:315
goto_functionst goto_functions
GOTO functions.
Definition: goto_model.h:32