CBMC
Loading...
Searching...
No Matches
remove_function.cpp
Go to the documentation of this file.
1/*******************************************************************\
2
3Module: Remove function definition
4
5Author: Michael Tautschnig
6
7Date: April 2017
8
9\*******************************************************************/
10
13
14#include "remove_function.h"
15
16#include <util/message.h>
17
19
20#include <regex>
21
29 goto_modelt &goto_model,
30 const irep_idt &identifier,
31 message_handlert &message_handler)
32{
33 messaget message(message_handler);
34
35 goto_functionst::function_mapt::iterator entry=
36 goto_model.goto_functions.function_map.find(identifier);
37
38 if(entry==goto_model.goto_functions.function_map.end())
39 {
40 message.error() << "No function " << identifier
41 << " in goto program" << messaget::eom;
42 return;
43 }
44 else if(to_code_type(goto_model.symbol_table.lookup_ref(identifier).type)
45 .get_inlined())
46 {
47 message.warning() << "Function " << identifier << " is inlined, "
48 << "instantiations will not be removed"
50 }
51
52 if(entry->second.body_available())
53 {
54 message.status() << "Removing body of " << identifier
56 entry->second.clear();
57 symbolt &symbol = goto_model.symbol_table.get_writeable_ref(identifier);
58 symbol.value.make_nil();
59 symbol.is_file_local = false;
60 }
61}
62
71 goto_modelt &goto_model,
72 const std::list<std::string> &names,
73 message_handlert &message_handler)
74{
75 for(const auto &f : names)
76 remove_function(goto_model, f, message_handler);
77}
78
85 goto_modelt &goto_model,
86 const std::regex &pattern,
87 const std::string &pattern_as_str,
88 message_handlert &message_handler)
89{
90 messaget message{message_handler};
91
92 message.debug() << "Removing functions matching pattern: " << pattern_as_str
94
95 // Collect matching function names first to avoid modifying the map while
96 // iterating
97 std::list<irep_idt> matching_functions;
98
99 for(const auto &entry : goto_model.goto_functions.function_map)
100 {
101 const std::string &function_name = id2string(entry.first);
102 if(std::regex_match(function_name, pattern))
103 {
104 matching_functions.push_back(entry.first);
105 }
106 }
107
108 // Now remove all matching functions
109 for(const auto &func : matching_functions)
110 {
111 remove_function(goto_model, func, message_handler);
112 }
113
114 message.debug() << "Removed " << matching_functions.size()
115 << " function(s) matching pattern: " << pattern_as_str
116 << messaget::eom;
117}
118
120 goto_modelt &goto_model,
121 const std::string &pattern,
122 message_handlert &message_handler)
123{
124 messaget message{message_handler};
125
126 try
127 {
128 std::regex regex_pattern{pattern};
129
130 remove_functions_regex(goto_model, regex_pattern, pattern, message_handler);
131 }
132 catch(const std::regex_error &e)
133 {
134 message.error() << "Invalid regular expression pattern: " << pattern << " ("
135 << e.what() << ")" << messaget::eom;
136 }
137}
virtual void clear()
Reset the abstract state.
Definition ai.h:265
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition ai.h:562
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition dstring.h:38
function_mapt function_map
symbol_tablet symbol_table
Symbol table.
Definition goto_model.h:31
goto_functionst goto_functions
GOTO functions.
Definition goto_model.h:34
void make_nil()
Definition irep.h:446
Class that provides messages with a built-in verbosity 'level'.
Definition message.h:154
mstreamt & error() const
Definition message.h:391
mstreamt & warning() const
Definition message.h:396
static eomt eom
Definition message.h:289
mstreamt & status() const
Definition message.h:406
symbolt & get_writeable_ref(const irep_idt &name)
Find a symbol in the symbol table for read-write access.
const symbolt & lookup_ref(const irep_idt &name) const
Find a symbol in the symbol table for read-only access.
Symbol table entry.
Definition symbol.h:28
bool is_file_local
Definition symbol.h:73
exprt value
Initial value of symbol.
Definition symbol.h:34
Symbol Table + CFG.
const std::string & id2string(const irep_idt &d)
Definition irep.h:44
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...
static void remove_functions_regex(goto_modelt &goto_model, const std::regex &pattern, const std::string &pattern_as_str, message_handlert &message_handler)
Remove functions matching a regular expression pattern.
Remove function definition.
const code_typet & to_code_type(const typet &type)
Cast a typet to a code_typet.
Definition std_types.h:788