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.
static void	add_parameter (const symbolt &symbol, code_typet &code_type)
	Adds the given symbol as parameter to the given code_typet.
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.
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.
static inlining_decoratort	inline_function (goto_modelt &goto_model, const irep_idt &function_id, message_handlert &message_handler)

Function Documentation

add_parameter()

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

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

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

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

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.