cprover
|
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) | |
![]() | |
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... | |
virtual void | generate_function_body_impl (goto_functiont &function, symbol_tablet &symbol_table, const irep_idt &function_name) const =0 |
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 ¶m_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 |
Definition at line 152 of file generate_function_bodies.cpp.
|
inline |
Definition at line 155 of file generate_function_bodies.cpp.
|
inline |
Definition at line 168 of file generate_function_bodies.cpp.
|
inlineoverrideprotectedvirtual |
Produce a body for the passed function At this point the body of function is always empty, and all function parameters have identifiers.
function | whose body to generate |
symbol_table | of the current goto program |
function_name | Identifier of function |
Implements generate_function_bodiest.
Definition at line 237 of file generate_function_bodies.cpp.
|
inlineprivate |
Definition at line 182 of file generate_function_bodies.cpp.
|
inlineprivate |
Definition at line 218 of file generate_function_bodies.cpp.
|
private |
Definition at line 375 of file generate_function_bodies.cpp.
|
mutableprivate |
Definition at line 379 of file generate_function_bodies.cpp.
|
private |
Definition at line 378 of file generate_function_bodies.cpp.
|
private |
Definition at line 377 of file generate_function_bodies.cpp.
|
private |
Definition at line 376 of file generate_function_bodies.cpp.