CBMC
Public Member Functions | Protected Member Functions | Private Member Functions | Private Attributes | List of all members
havoc_generate_function_bodiest Class Reference
+ Inheritance diagram for havoc_generate_function_bodiest:
+ Collaboration diagram for havoc_generate_function_bodiest:

Public Member Functions

 havoc_generate_function_bodiest (std::vector< irep_idt > globals_to_havoc, std::regex parameters_to_havoc, const c_object_factory_parameterst &object_factory_parameters, message_handlert &message_handler)
 
 havoc_generate_function_bodiest (std::vector< irep_idt > globals_to_havoc, std::vector< std::size_t > param_numbers_to_havoc, const c_object_factory_parameterst &object_factory_parameters, message_handlert &message_handler)
 
- Public Member Functions inherited from generate_function_bodiest
virtual ~generate_function_bodiest ()=default
 
void generate_function_body (goto_functiont &function, symbol_tablet &symbol_table, const irep_idt &function_name) const
 Replace the function body with one based on the replace_function_body class being used. More...
 

Protected Member Functions

void generate_function_body_impl (goto_functiont &function, symbol_tablet &symbol_table, const irep_idt &function_name) const override
 Produce a body for the passed function At this point the body of function is always empty, and all function parameters have identifiers. More...
 

Private Member Functions

void havoc_expr_rec (const exprt &lhs, const std::size_t initial_depth, const source_locationt &source_location, const irep_idt &function_id, symbol_tablet &symbol_table, goto_programt &dest) const
 
bool should_havoc_param (const std::string &param_name, std::size_t param_number) const
 

Private Attributes

const std::vector< irep_idt > globals_to_havoc
 
optionalt< std::regex > parameters_to_havoc
 
optionalt< std::vector< std::size_t > > param_numbers_to_havoc
 
const c_object_factory_parameterst & object_factory_parameters
 
messaget message
 

Detailed Description

Definition at line 144 of file generate_function_bodies.cpp.

Constructor & Destructor Documentation

◆ havoc_generate_function_bodiest() [1/2]

havoc_generate_function_bodiest::havoc_generate_function_bodiest ( std::vector< irep_idt >  globals_to_havoc,
std::regex  parameters_to_havoc,
const c_object_factory_parameterst &  object_factory_parameters,
message_handlert &  message_handler 
)
inline

Definition at line 147 of file generate_function_bodies.cpp.

◆ havoc_generate_function_bodiest() [2/2]

havoc_generate_function_bodiest::havoc_generate_function_bodiest ( std::vector< irep_idt >  globals_to_havoc,
std::vector< std::size_t >  param_numbers_to_havoc,
const c_object_factory_parameterst &  object_factory_parameters,
message_handlert &  message_handler 
)
inline

Definition at line 160 of file generate_function_bodies.cpp.

Member Function Documentation

◆ generate_function_body_impl()

void havoc_generate_function_bodiest::generate_function_body_impl ( goto_functiont &  function,
symbol_tablet &  symbol_table,
const irep_idt &  function_name 
) const
inlineoverrideprotectedvirtual

Produce a body for the passed function At this point the body of function is always empty, and all function parameters have identifiers.

Parameters
functionwhose body to generate
symbol_tableof the current goto program
function_nameIdentifier of function

Implements generate_function_bodiest.

Definition at line 229 of file generate_function_bodies.cpp.

◆ havoc_expr_rec()

void havoc_generate_function_bodiest::havoc_expr_rec ( const exprt &  lhs,
const std::size_t  initial_depth,
const source_locationt &  source_location,
const irep_idt &  function_id,
symbol_tablet &  symbol_table,
goto_programt &  dest 
) const
inlineprivate

Definition at line 174 of file generate_function_bodies.cpp.

◆ should_havoc_param()

bool havoc_generate_function_bodiest::should_havoc_param ( const std::string &  param_name,
std::size_t  param_number 
) const
inlineprivate

Definition at line 210 of file generate_function_bodies.cpp.

Member Data Documentation

◆ globals_to_havoc

const std::vector<irep_idt> havoc_generate_function_bodiest::globals_to_havoc
private

Definition at line 367 of file generate_function_bodies.cpp.

◆ message

messaget havoc_generate_function_bodiest::message
mutableprivate

Definition at line 371 of file generate_function_bodies.cpp.

◆ object_factory_parameters

const c_object_factory_parameterst& havoc_generate_function_bodiest::object_factory_parameters
private

Definition at line 370 of file generate_function_bodies.cpp.

◆ param_numbers_to_havoc

optionalt<std::vector<std::size_t> > havoc_generate_function_bodiest::param_numbers_to_havoc
private

Definition at line 369 of file generate_function_bodies.cpp.

◆ parameters_to_havoc

optionalt<std::regex> havoc_generate_function_bodiest::parameters_to_havoc
private

Definition at line 368 of file generate_function_bodies.cpp.

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