CBMC
dfcc_utils.cpp File Reference
+ 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 symboltclone_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 void add_parameter ( const symbolt symbol,
code_typet code_type 
)
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 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 
)
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_modeltarget goto_model holding the symbol table
function_idfunction to clone
trans_funtransformation function for the function name
trans_paramtransformation function for the parameter names
trans_ret_typetransformation function for the return type
trans_loctransformation function for the source location
Returns
the new function symbol

Definition at line 249 of file dfcc_utils.cpp.

◆ clone_parameters()

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 
)
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 inlining_decoratort inline_function ( goto_modelt goto_model,
const irep_idt function_id,
message_handlert message_handler 
)
static

Definition at line 424 of file dfcc_utils.cpp.

◆ symbol_exists()

static bool symbol_exists ( const goto_modelt goto_model,
const irep_idt name,
const bool  require_has_code_type,
const bool  require_body_available 
)
static

Returns true iff the given symbol exists and satisfies requirements.

Definition at line 33 of file dfcc_utils.cpp.