This contains implementation details of function call harness generator to avoid leaking them out into the header. More...

Collaboration diagram for function_call_harness_generatort::implt:

Public Member Functions
void	generate (goto_modelt &goto_model, const irep_idt &harness_function_name)

void	generate_nondet_globals (code_blockt &function_body)
	Iterate over the symbol table and generate initialisation code for globals into the function body. More...

const symbolt &	lookup_function_to_call ()
	Return a reference to the entry function or throw if it doesn't exist. More...

void	generate_initialisation_code_for (code_blockt &block, const exprt &lhs)
	Generate initialisation code for one lvalue inside block. More...

void	ensure_harness_does_not_already_exist ()
	Throw if the harness function already exists in the symbol table. More...

void	add_harness_function_to_goto_model (code_blockt function_body)
	Update the goto-model with the new harness function. More...

code_function_callt::argumentst	declare_arguments (code_blockt &function_body)
	Declare local variables for each of the parameters of the entry function and return them. More...

void	call_function (const code_function_callt::argumentst &arguments, code_blockt &function_body)
	Write initialisation code for each of the arguments into function_body, then insert a call to the entry function with the arguments. More...

std::unordered_set< irep_idt >	map_function_parameters_to_function_argument_names ()
	For function parameters that are pointers to functions we want to be able to specify whether or not they can be NULL. More...

Public Attributes
ui_message_handlert *	message_handler

irep_idt	function

irep_idt	harness_function_name

symbol_tablet *	symbol_table

goto_functionst *	goto_functions

bool	nondet_globals = false

recursive_initialization_configt	recursive_initialization_config

std::unique_ptr< recursive_initializationt >	recursive_initialization

std::set< irep_idt >	function_parameters_to_treat_as_arrays

std::set< irep_idt >	function_arguments_to_treat_as_arrays

std::vector< std::set< irep_idt > >	function_parameters_to_treat_equal

std::vector< std::set< irep_idt > >	function_arguments_to_treat_equal

std::set< irep_idt >	function_parameters_to_treat_as_cstrings

std::set< irep_idt >	function_arguments_to_treat_as_cstrings

std::map< irep_idt, irep_idt >	function_argument_to_associated_array_size

std::map< irep_idt, irep_idt >	function_parameter_to_associated_array_size

std::set< symbol_exprt >	global_pointers

Detailed Description

This contains implementation details of function call harness generator to avoid leaking them out into the header.

Definition at line 37 of file function_call_harness_generator.cpp.

Member Function Documentation

◆ add_harness_function_to_goto_model()

void function_call_harness_generatort::implt::add_harness_function_to_goto_model ( code_blockt function_body )

Update the goto-model with the new harness function.

Definition at line 439 of file function_call_harness_generator.cpp.

◆ call_function()

void function_call_harness_generatort::implt::call_function	(	const code_function_callt::argumentst &	arguments,
		code_blockt &	function_body
	)

Write initialisation code for each of the arguments into function_body, then insert a call to the entry function with the arguments.

Definition at line 539 of file function_call_harness_generator.cpp.

◆ declare_arguments()

code_function_callt::argumentst function_call_harness_generatort::implt::declare_arguments ( code_blockt & function_body )

Declare local variables for each of the parameters of the entry function and return them.

Definition at line 460 of file function_call_harness_generator.cpp.

◆ ensure_harness_does_not_already_exist()

void function_call_harness_generatort::implt::ensure_harness_does_not_already_exist ( )

Throw if the harness function already exists in the symbol table.

Definition at line 428 of file function_call_harness_generator.cpp.

◆ generate()

void function_call_harness_generatort::implt::generate	(	goto_modelt &	goto_model,
		const irep_idt &	harness_function_name
	)

See also: goto_harness_generatort::generate

Definition at line 226 of file function_call_harness_generator.cpp.

◆ generate_initialisation_code_for()

void function_call_harness_generatort::implt::generate_initialisation_code_for	(	code_blockt &	block,
		const exprt &	lhs
	)

Generate initialisation code for one lvalue inside block.

Definition at line 297 of file function_call_harness_generator.cpp.

◆ generate_nondet_globals()

void function_call_harness_generatort::implt::generate_nondet_globals ( code_blockt & function_body )

Iterate over the symbol table and generate initialisation code for globals into the function body.

Definition at line 270 of file function_call_harness_generator.cpp.

◆ lookup_function_to_call()

const symbolt & function_call_harness_generatort::implt::lookup_function_to_call ( )

Return a reference to the entry function or throw if it doesn't exist.

Definition at line 414 of file function_call_harness_generator.cpp.

◆ map_function_parameters_to_function_argument_names()

std::unordered_set< irep_idt > function_call_harness_generatort::implt::map_function_parameters_to_function_argument_names ( )

For function parameters that are pointers to functions we want to be able to specify whether or not they can be NULL.

To disambiguate this specification from that for a global variable of the same name, we prepend the name of the function to the parameter name. However, what is actually being initialised in the implementation is not the parameter itself, but a corresponding function argument (local variable of the harness function). We need a mapping from function parameter name to function argument names, and this is what this function does.

Definition at line 557 of file function_call_harness_generator.cpp.