CBMC
function_call_harness_generatort::implt Struct Reference

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 symboltlookup_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_idtmap_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_handlertmessage_handler
 
irep_idt function
 
irep_idt harness_function_name
 
symbol_tabletsymbol_table
 
goto_functionstgoto_functions
 
bool nondet_globals = false
 
recursive_initialization_configt recursive_initialization_config
 
std::unique_ptr< recursive_initializationtrecursive_initialization
 
std::set< irep_idtfunction_parameters_to_treat_as_arrays
 
std::set< irep_idtfunction_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_idtfunction_parameters_to_treat_as_cstrings
 
std::set< irep_idtfunction_arguments_to_treat_as_cstrings
 
std::map< irep_idt, irep_idtfunction_argument_to_associated_array_size
 
std::map< irep_idt, irep_idtfunction_parameter_to_associated_array_size
 
std::set< symbol_exprtglobal_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 
)

◆ 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.

Member Data Documentation

◆ function

irep_idt function_call_harness_generatort::implt::function

Definition at line 40 of file function_call_harness_generator.cpp.

◆ function_argument_to_associated_array_size

std::map<irep_idt, irep_idt> function_call_harness_generatort::implt::function_argument_to_associated_array_size

Definition at line 58 of file function_call_harness_generator.cpp.

◆ function_arguments_to_treat_as_arrays

std::set<irep_idt> function_call_harness_generatort::implt::function_arguments_to_treat_as_arrays

Definition at line 50 of file function_call_harness_generator.cpp.

◆ function_arguments_to_treat_as_cstrings

std::set<irep_idt> function_call_harness_generatort::implt::function_arguments_to_treat_as_cstrings

Definition at line 56 of file function_call_harness_generator.cpp.

◆ function_arguments_to_treat_equal

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

Definition at line 53 of file function_call_harness_generator.cpp.

◆ function_parameter_to_associated_array_size

std::map<irep_idt, irep_idt> function_call_harness_generatort::implt::function_parameter_to_associated_array_size

Definition at line 59 of file function_call_harness_generator.cpp.

◆ function_parameters_to_treat_as_arrays

std::set<irep_idt> function_call_harness_generatort::implt::function_parameters_to_treat_as_arrays

Definition at line 49 of file function_call_harness_generator.cpp.

◆ function_parameters_to_treat_as_cstrings

std::set<irep_idt> function_call_harness_generatort::implt::function_parameters_to_treat_as_cstrings

Definition at line 55 of file function_call_harness_generator.cpp.

◆ function_parameters_to_treat_equal

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

Definition at line 52 of file function_call_harness_generator.cpp.

◆ global_pointers

std::set<symbol_exprt> function_call_harness_generatort::implt::global_pointers

Definition at line 61 of file function_call_harness_generator.cpp.

◆ goto_functions

goto_functionst* function_call_harness_generatort::implt::goto_functions

Definition at line 43 of file function_call_harness_generator.cpp.

◆ harness_function_name

irep_idt function_call_harness_generatort::implt::harness_function_name

Definition at line 41 of file function_call_harness_generator.cpp.

◆ message_handler

ui_message_handlert* function_call_harness_generatort::implt::message_handler

Definition at line 39 of file function_call_harness_generator.cpp.

◆ nondet_globals

bool function_call_harness_generatort::implt::nondet_globals = false

Definition at line 44 of file function_call_harness_generator.cpp.

◆ recursive_initialization

std::unique_ptr<recursive_initializationt> function_call_harness_generatort::implt::recursive_initialization

Definition at line 47 of file function_call_harness_generator.cpp.

◆ recursive_initialization_config

recursive_initialization_configt function_call_harness_generatort::implt::recursive_initialization_config

Definition at line 46 of file function_call_harness_generator.cpp.

◆ symbol_table

symbol_tablet* function_call_harness_generatort::implt::symbol_table

Definition at line 42 of file function_call_harness_generator.cpp.


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