#include <dfcc_utils.h>

Static Public Member Functions
static bool	function_symbol_exists (const goto_modelt &, const irep_idt &function_id)
	Returns true iff the given symbol exists and satisfies requirements. More...

static bool	function_symbol_with_body_exists (const goto_modelt &, const irep_idt &function_id)

static symbolt &	get_function_symbol (symbol_table_baset &, const irep_idt &function_id)
	Returns the `symbolt` for `function_id`. More...

static symbol_exprt	create_symbol (symbol_table_baset &, const typet &type, const irep_idt &function_id, const std::string &base_name, const source_locationt &source_location)
	Adds a new symbol named `function_id::base_name` of type `type` with given attributes in the symbol table, and returns a symbol expression for the created symbol. More...

static const symbolt &	create_static_symbol (symbol_table_baset &, const typet &type, const std::string &prefix, const std::string &base_name, const source_locationt &source_location, const irep_idt &mode, const irep_idt &module, const exprt &initial_value, const bool no_nondet_initialization=true)
	Adds a new static symbol named `prefix::base_name` of type `type` with value `initial_value` in the symbol table, returns the created symbol. More...

static const symbolt &	create_new_parameter_symbol (symbol_table_baset &, const irep_idt &function_id, const std::string &base_name, const typet &type)
	Creates a new parameter symbol for the given function_id. More...

static void	add_parameter (goto_modelt &, const symbolt &symbol, const irep_idt &function_id)
	Adds the given symbol as parameter to the function symbol's code_type. More...

static const symbolt &	add_parameter (goto_modelt &, const irep_idt &function_id, const std::string &base_name, const typet &type)
	Adds a parameter with given `base_name` and `type` to the given `function_id`. More...

static const symbolt &	clone_and_rename_function (goto_modelt &goto_model, const irep_idt &function_id, const irep_idt &new_function_id, std::optional< typet > new_return_type)
	Creates a new function symbol and goto_function entry in the `goto_functions_map` by cloning the given `function_id`. More...

static void	wrap_function (goto_modelt &goto_model, const irep_idt &function_id, const irep_idt &wrapped_function_id)
	Given a function to wrap `foo` and a new name `wrapped_foo` More...

static const exprt	make_null_check_expr (const exprt &ptr)
	Returns the expression `expr == NULL`. More...

static exprt	make_sizeof_expr (const exprt &expr, const namespacet &)
	Returns the expression `sizeof(expr)`. More...

static void	inline_function (goto_modelt &goto_model, const irep_idt &function_id, message_handlert &message_handler)
	Inlines the given function, aborts on recursive calls during inlining. More...

static void	inline_function (goto_modelt &goto_model, const irep_idt &function_id, std::set< irep_idt > &no_body, std::set< irep_idt > &recursive_call, std::set< irep_idt > &missing_function, std::set< irep_idt > &not_enough_arguments, message_handlert &message_handler)
	Inlines the given function, and returns function symbols that caused warnings. More...

static void	inline_program (goto_modelt &goto_model, goto_programt &goto_program, std::set< irep_idt > &no_body, std::set< irep_idt > &recursive_call, std::set< irep_idt > &missing_function, std::set< irep_idt > &not_enough_arguments, message_handlert &message_handler)
	Inlines the given program, and returns function symbols that caused warnings. More...

Detailed Description

Definition at line 27 of file dfcc_utils.h.

Member Function Documentation

◆ add_parameter() [1/2]

const symbolt & dfcc_utilst::add_parameter	(	goto_modelt &	goto_model,
		const irep_idt &	function_id,
		const std::string &	base_name,
		const typet &	type
	)

static

Adds a parameter with given base_name and type to the given function_id.

Both the symbol and the goto_function are updated.

Definition at line 170 of file dfcc_utils.cpp.

◆ add_parameter() [2/2]

void dfcc_utilst::add_parameter	(	goto_modelt &	goto_model,
		const symbolt &	symbol,
		const irep_idt &	function_id
	)

static

Adds the given symbol as parameter to the function symbol's code_type.

Also adds the corresponding parameter to its goto_function if it exists in the function map of the goto model.

Definition at line 156 of file dfcc_utils.cpp.

◆ clone_and_rename_function()

const symbolt & dfcc_utilst::clone_and_rename_function	(	goto_modelt &	goto_model,
		const irep_idt &	function_id,
		const irep_idt &	new_function_id,
		std::optional< typet >	new_return_type = `{}`
	)

static

Creates a new function symbol and goto_function entry in the goto_functions_map by cloning the given function_id.

The cloned function symbol has new_function_id as name The cloned parameters symbols have new_function_id::name as name Returns the new function symbol

Definition at line 300 of file dfcc_utils.cpp.

◆ create_new_parameter_symbol()

const symbolt & dfcc_utilst::create_new_parameter_symbol	(	symbol_table_baset &	symbol_table,
		const irep_idt &	function_id,
		const std::string &	base_name,
		const typet &	type
	)

static

Creates a new parameter symbol for the given function_id.

Definition at line 124 of file dfcc_utils.cpp.

◆ create_static_symbol()

const symbolt & dfcc_utilst::create_static_symbol	(	symbol_table_baset &	symbol_table,
		const typet &	type,
		const std::string &	prefix,
		const std::string &	base_name,
		const source_locationt &	source_location,
		const irep_idt &	mode,
		const irep_idt &	module,
		const exprt &	initial_value,
		const bool	no_nondet_initialization = `true`
	)

static

Adds a new static symbol named prefix::base_name of type type with value initial_value in the symbol table, returns the created symbol.

If a symbol of the same name already exists the name will be decorated with a unique suffix. By default the symbol is be protected against nondet initialisation by tagging the its value field with a ID_C_no_nondet_initialization attribute as understood by nondet_static. This is because the static instrumentation variables are meant to keep their initial values for the instrumentation to work as intended. To allow nondet-initialisation of the symbol, just set no_nondet_initialization to false when calling the method.

Definition at line 103 of file dfcc_utils.cpp.

◆ create_symbol()

symbol_exprt dfcc_utilst::create_symbol	(	symbol_table_baset &	symbol_table,
		const typet &	type,
		const irep_idt &	function_id,
		const std::string &	base_name,
		const source_locationt &	source_location
	)

static

Adds a new symbol named function_id::base_name of type type with given attributes in the symbol table, and returns a symbol expression for the created symbol.

If a symbol of the same name already exists the name will be decorated with a unique suffix.

Definition at line 81 of file dfcc_utils.cpp.

◆ function_symbol_exists()

bool dfcc_utilst::function_symbol_exists	(	const goto_modelt &	goto_model,
		const irep_idt &	function_id
	)

static

Returns true iff the given symbol exists and satisfies requirements.

Definition at line 58 of file dfcc_utils.cpp.

◆ function_symbol_with_body_exists()

bool dfcc_utilst::function_symbol_with_body_exists	(	const goto_modelt &	goto_model,
		const irep_idt &	function_id
	)

static

Definition at line 65 of file dfcc_utils.cpp.

◆ get_function_symbol()

symbolt & dfcc_utilst::get_function_symbol	(	symbol_table_baset &	symbol_table,
		const irep_idt &	function_id
	)

static

Returns the symbolt for function_id.

Definition at line 72 of file dfcc_utils.cpp.

◆ inline_function() [1/2]

void dfcc_utilst::inline_function	(	goto_modelt &	goto_model,
		const irep_idt &	function_id,
		message_handlert &	message_handler
	)

static

Inlines the given function, aborts on recursive calls during inlining.

Definition at line 443 of file dfcc_utils.cpp.

◆ inline_function() [2/2]

void dfcc_utilst::inline_function	(	goto_modelt &	goto_model,
		const irep_idt &	function_id,
		std::set< irep_idt > &	no_body,
		std::set< irep_idt > &	recursive_call,
		std::set< irep_idt > &	missing_function,
		std::set< irep_idt > &	not_enough_arguments,
		message_handlert &	message_handler
	)

static

Inlines the given function, and returns function symbols that caused warnings.

Definition at line 460 of file dfcc_utils.cpp.

◆ inline_program()

void dfcc_utilst::inline_program	(	goto_modelt &	goto_model,
		goto_programt &	goto_program,
		std::set< irep_idt > &	no_body,
		std::set< irep_idt > &	recursive_call,
		std::set< irep_idt > &	missing_function,
		std::set< irep_idt > &	not_enough_arguments,
		message_handlert &	message_handler
	)

static

Inlines the given program, and returns function symbols that caused warnings.

Definition at line 487 of file dfcc_utils.cpp.

◆ make_null_check_expr()

const exprt dfcc_utilst::make_null_check_expr ( const exprt & ptr )

static

Returns the expression expr == NULL.

Definition at line 406 of file dfcc_utils.cpp.

◆ make_sizeof_expr()

exprt dfcc_utilst::make_sizeof_expr	(	const exprt &	expr,
		const namespacet &	ns
	)

static

Returns the expression sizeof(expr).

Definition at line 411 of file dfcc_utils.cpp.

◆ wrap_function()

void dfcc_utilst::wrap_function	(	goto_modelt &	goto_model,
		const irep_idt &	function_id,
		const irep_idt &	wrapped_function_id
	)

static

Given a function to wrap foo and a new name wrapped_foo

ret_t foo(x_t foo::x, y_t foo::y) { foo_body; }

This method creates a new entry in the symbol_table for wrapped_foo and moves the body of the original function, foo_body, under wrapped_foo in function_map.

The parameter symbols of wrapped_foo remain the same as in foo:

ret_t wrapped_foo(x_t foo::x, y_t foo::y) { foo_body; }

The parameters of the original foo get renamed to make sure they are distinct from that of wrapped_foo, and a new empty body is generated for foo:

ret_t foo(x_t foo::x_wrapped, y_t foo::y_wrapped) { };

Any other goto_function calling foo still calls foo which has become a wrapper for wrapped_foo.

By generating a new body for foo, one can implement contract checking logic, contract replacement logic, etc.

Definition at line 324 of file dfcc_utils.cpp.

The documentation for this struct was generated from the following files:

/home/runner/work/cbmc/cbmc/src/goto-instrument/contracts/dynamic-frames/dfcc_utils.h
/home/runner/work/cbmc/cbmc/src/goto-instrument/contracts/dynamic-frames/dfcc_utils.cpp

Static Public Member Functions

Detailed Description

Member Function Documentation

◆ add_parameter() [1/2]

◆ add_parameter() [2/2]

◆ clone_and_rename_function()

◆ create_new_parameter_symbol()

◆ create_static_symbol()

◆ create_symbol()

◆ function_symbol_exists()

◆ function_symbol_with_body_exists()

◆ get_function_symbol()

◆ inline_function() [1/2]

◆ inline_function() [2/2]

◆ inline_program()

◆ make_null_check_expr()

◆ make_sizeof_expr()

◆ wrap_function()