CBMC
Loading...
Searching...
No Matches
remove_function.cpp File Reference

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.
 

Detailed Description

Remove function definition.

Definition in file remove_function.cpp.

Function Documentation

◆ remove_function()

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.

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

Definition at line 28 of file remove_function.cpp.

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

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

Definition at line 70 of file remove_function.cpp.

◆ remove_functions_regex() [1/2]

static void remove_functions_regex ( goto_modelt goto_model,
const std::regex &  pattern,
const std::string &  pattern_as_str,
message_handlert message_handler 
)
static

Remove functions matching a regular expression pattern.

Parameters
goto_modelThe goto model to modify
patternThe regex pattern to match function names against
pattern_as_strThe string representation of pattern
message_handlerFor status/warning/error messages

Definition at line 84 of file remove_function.cpp.

◆ remove_functions_regex() [2/2]

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.

Parameters
goto_modelThe goto model to modify
patternRegex patterns to match function names against
message_handlerFor status/warning/error messages

Definition at line 119 of file remove_function.cpp.