cprover
|
Remove function definition. More...
Go to the source code of this file.
Functions | |
void | remove_function (symbol_tablet &symbol_table, goto_functionst &goto_functions, 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. More... | |
void | remove_functions (symbol_tablet &symbol_table, goto_functionst &goto_functions, 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. More... | |
Remove function definition.
Definition in file remove_function.cpp.
void remove_function | ( | symbol_tablet & | symbol_table, |
goto_functionst & | goto_functions, | ||
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_functions_templatet< bodyT >::function_map, symbol_tablet::lookup(), irept::make_nil(), messaget::status(), symbolt::value, and messaget::warning().
Referenced by remove_functions().
void remove_functions | ( | symbol_tablet & | symbol_table, |
goto_functionst & | goto_functions, | ||
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 66 of file remove_function.cpp.
References remove_function().
Referenced by goto_instrument_parse_optionst::instrument_goto_program().