cprover
remove_function.h File Reference

Remove function definition. More...

#include <list>
#include <string>
#include <util/irep.h>
Include dependency graph for remove_function.h:
This graph shows which files directly or indirectly include this file:

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...
 

Detailed Description

Remove function definition.

Definition in file remove_function.h.

Function Documentation

◆ remove_function()

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.

parameters: symbol_table Input symbol table to be modified
goto_functions Input functions to be modified identifier Function to be removed message_handler Error/status output

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().

◆ 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.

parameters: symbol_table Input symbol table to be modified
goto_functions Input functions to be modified names List of functions to be removed message_handler Error/status output

Definition at line 66 of file remove_function.cpp.

References remove_function().

Referenced by goto_instrument_parse_optionst::instrument_goto_program().