cprover
|
Remove function definition. More...
Go to the source code of this file.
Functions | |
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 function with non-deterministic return value. More... | |
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-effect free function with non-deterministic return value. More... | |
Remove function definition.
Definition in file remove_function.h.
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 function with non-deterministic return value.
Definition at line 26 of file remove_function.cpp.
References messaget::eom(), messaget::error(), goto_functionst::function_map, symbol_table_baset::get_writeable_ref(), goto_modelt::goto_functions, irept::make_nil(), message_handler, messaget::status(), goto_modelt::symbol_table, symbolt::value, and messaget::warning().
Referenced by 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-effect free function with non-deterministic return value.
Definition at line 65 of file remove_function.cpp.
References message_handler, and remove_function().
Referenced by goto_instrument_parse_optionst::instrument_goto_program().