|
CBMC
|
Remove function definition. More...
#include "remove_function.h"#include <util/message.h>#include <goto-programs/goto_model.h>#include <regex>
Include dependency graph for remove_function.cpp:Go to the source code of this file.
Functions | |
| 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. | |
| 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. | |
| static void | remove_functions_regex (goto_modelt &goto_model, const std::regex &pattern, const std::string &pattern_as_str, message_handlert &message_handler) |
| Remove functions matching a regular expression pattern. | |
| void | remove_functions_regex (goto_modelt &goto_model, const std::string &pattern, message_handlert &message_handler) |
| Remove functions matching any of the provided regular expression patterns. | |
Remove function definition.
Definition in file remove_function.cpp.
| 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 28 of file remove_function.cpp.
| 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 70 of file remove_function.cpp.
|
static |
Remove functions matching a regular expression pattern.
| goto_model | The goto model to modify |
| pattern | The regex pattern to match function names against |
| pattern_as_str | The string representation of pattern |
| message_handler | For status/warning/error messages |
Definition at line 84 of file remove_function.cpp.
| void remove_functions_regex | ( | goto_modelt & | goto_model, |
| const std::string & | pattern, | ||
| message_handlert & | message_handler | ||
| ) |
Remove functions matching any of the provided regular expression patterns.
| goto_model | The goto model to modify |
| pattern | Regex patterns to match function names against |
| message_handler | For status/warning/error messages |
Definition at line 119 of file remove_function.cpp.