CBMC
Loading...
Searching...
No Matches
remove_function.h
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#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
22class goto_modelt;
23class message_handlert;
24
25void remove_function(
26 goto_modelt &,
27 const irep_idt &identifier,
28 message_handlert &);
29
30void remove_functions(
31 goto_modelt &,
32 const std::list<std::string> &names,
33 message_handlert &);
34
35#endif // CPROVER_GOTO_INSTRUMENT_REMOVE_FUNCTION_H
ait
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition ai.h:562
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:27
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