cprover
Toggle main menu visibility
Loading...
Searching...
No Matches
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
18
#include <
goto-programs/goto_model.h
>
19
20
#include <regex>
21
28
void
remove_function
(
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"
49
<<
messaget::eom
;
50
}
51
52
if
(entry->second.body_available())
53
{
54
message.
status
() <<
"Removing body of "
<< identifier
55
<<
messaget::eom
;
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
70
void
remove_functions
(
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
84
static
void
remove_functions_regex
(
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
93
<<
messaget::eom
;
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
119
void
remove_functions_regex
(
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
}
code_typet::get_inlined
bool get_inlined() const
Definition
std_types.h:709
goto_functionst::function_map
function_mapt function_map
Definition
goto_functions.h:29
goto_modelt
Definition
goto_model.h:27
goto_modelt::symbol_table
symbol_tablet symbol_table
Symbol table.
Definition
goto_model.h:31
goto_modelt::goto_functions
goto_functionst goto_functions
GOTO functions.
Definition
goto_model.h:34
irept::make_nil
void make_nil()
Definition
irep.h:446
message_handlert
Definition
message.h:27
messaget
Class that provides messages with a built-in verbosity 'level'.
Definition
message.h:154
messaget::error
mstreamt & error() const
Definition
message.h:391
messaget::debug
mstreamt & debug() const
Definition
message.h:421
messaget::warning
mstreamt & warning() const
Definition
message.h:396
messaget::eom
static eomt eom
Definition
message.h:289
messaget::status
mstreamt & status() const
Definition
message.h:406
symbol_table_baset::get_writeable_ref
symbolt & get_writeable_ref(const irep_idt &name)
Find a symbol in the symbol table for read-write access.
Definition
symbol_table_base.h:149
symbol_table_baset::lookup_ref
const symbolt & lookup_ref(const irep_idt &name) const
Find a symbol in the symbol table for read-only access.
Definition
symbol_table_base.h:105
symbolt
Symbol table entry.
Definition
symbol.h:28
symbolt::is_file_local
bool is_file_local
Definition
symbol.h:73
symbolt::type
typet type
Type of symbol.
Definition
symbol.h:31
symbolt::value
exprt value
Initial value of symbol.
Definition
symbol.h:34
goto_model.h
Symbol Table + CFG.
id2string
const std::string & id2string(const irep_idt &d)
Definition
irep.h:44
remove_function
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...
Definition
remove_function.cpp:28
remove_functions
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...
Definition
remove_function.cpp:70
remove_functions_regex
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.
Definition
remove_function.cpp:84
remove_function.h
Remove function definition.
message.h
to_code_type
const code_typet & to_code_type(const typet &type)
Cast a typet to a code_typet.
Definition
std_types.h:788
irep_idt
dstringt irep_idt
Definition
verification_result.h:16
goto-instrument
remove_function.cpp
Generated by
1.17.0