CBMC
remove_function.h
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 #ifndef CPROVER_GOTO_INSTRUMENT_REMOVE_FUNCTION_H
15 #define CPROVER_GOTO_INSTRUMENT_REMOVE_FUNCTION_H
16 
17 #include <list>
18 #include <string>
19 
20 #include <util/irep.h>
21 
22 class goto_modelt;
23 class message_handlert;
24 
25 void remove_function(
26  goto_modelt &,
27  const irep_idt &identifier,
28  message_handlert &);
29 
30 void remove_functions(
31  goto_modelt &,
32  const std::list<std::string> &names,
33  message_handlert &);
34 
35 #endif // CPROVER_GOTO_INSTRUMENT_REMOVE_FUNCTION_H
dstringt
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:38
goto_modelt
Definition: goto_model.h:27
message_handlert
Definition: message.h:28
remove_function
void remove_function(goto_modelt &, const irep_idt &identifier, message_handlert &)
Remove the body of function "identifier" such that an analysis will treat it as a side-effect free fu...
Definition: remove_function.cpp:26
remove_functions
void remove_functions(goto_modelt &, const std::list< std::string > &names, message_handlert &)
Remove the body of all functions listed in "names" such that an analysis will treat it as a side-effe...
Definition: remove_function.cpp:68