dfcc_utils.cpp File Reference
#include "dfcc_utils.h"#include <util/arith_tools.h>#include <util/c_types.h>#include <util/format_expr.h>#include <util/fresh_symbol.h>#include <util/message.h>#include <util/pointer_expr.h>#include <util/pointer_offset_size.h>#include <util/std_expr.h>#include <util/std_types.h>#include <goto-programs/goto_inline.h>#include <goto-programs/goto_model.h>#include <ansi-c/goto-conversion/goto_convert_functions.h>#include <goto-instrument/contracts/inlining_decorator.h>#include <goto-instrument/contracts/utils.h>#include <linking/static_lifetime_init.h>#include <set>
Include dependency graph for dfcc_utils.cpp:Go to the source code of this file.
Functions | |
| static bool | symbol_exists (const goto_modelt &goto_model, const irep_idt &name, const bool require_has_code_type, const bool require_body_available) |
| Returns true iff the given symbol exists and satisfies requirements. More... | |
| static void | add_parameter (const symbolt &symbol, code_typet &code_type) |
| Adds the given symbol as parameter to the given code_typet. More... | |
| static void | clone_parameters (symbol_table_baset &symbol_table, const code_typet::parameterst &old_params, const irep_idt &mode, const irep_idt &module, const source_locationt &location, std::function< const irep_idt(const irep_idt &)> &trans_param, const irep_idt &new_function_id, code_typet::parameterst &new_params) |
| Clones the old_params into the new_params list, applying the trans_param function to generate the names of the cloned params. More... | |
| static const symbolt & | clone_and_rename_function (goto_modelt &goto_model, const irep_idt &function_id, std::function< const irep_idt(const irep_idt &)> &trans_fun, std::function< const irep_idt(const irep_idt &)> &trans_param, std::function< const typet(const typet &)> &trans_ret_type, std::function< const source_locationt(const source_locationt &)> &trans_loc) |
Creates a new symbol in the symbol_table by cloning the given function_id function and transforming the existing function's name, parameter names, return type and source location using the given trans_fun, trans_param and trans_ret_type and trans_loc functions. More... | |
| static inlining_decoratort | inline_function (goto_modelt &goto_model, const irep_idt &function_id, message_handlert &message_handler) |
Function Documentation
◆ add_parameter()
|
static |
Adds the given symbol as parameter to the given code_typet.
Definition at line 146 of file dfcc_utils.cpp.
◆ clone_and_rename_function()
|
static |
Creates a new symbol in the symbol_table by cloning the given function_id function and transforming the existing function's name, parameter names, return type and source location using the given trans_fun, trans_param and trans_ret_type and trans_loc functions.
Also creates a new goto_function under the transformed name in the function_map with new parameters and an empty body. Returns the new symbol.
- Parameters
-
goto_model target goto_model holding the symbol table function_id function to clone trans_fun transformation function for the function name trans_param transformation function for the parameter names trans_ret_type transformation function for the return type trans_loc transformation function for the source location
- Returns
- the new function symbol
Definition at line 249 of file dfcc_utils.cpp.
◆ clone_parameters()
|
static |
Clones the old_params into the new_params list, applying the trans_param function to generate the names of the cloned params.
Definition at line 184 of file dfcc_utils.cpp.
◆ inline_function()
|
static |
Definition at line 424 of file dfcc_utils.cpp.
◆ symbol_exists()
|
static |
Returns true iff the given symbol exists and satisfies requirements.
Definition at line 33 of file dfcc_utils.cpp.
