cprover
|
Public Member Functions | |
havoc_generate_function_bodiest (std::vector< irep_idt > globals_to_havoc, std::regex parameters_to_havoc, 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, const 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 namespacet &ns, const std::function< goto_programt::targett(void)> &add_instruction, const irep_idt &function_name) const |
Private Attributes | |
const std::vector< irep_idt > | globals_to_havoc |
std::regex | parameters_to_havoc |
Additional Inherited Members |
Definition at line 149 of file generate_function_bodies.cpp.
|
inline |
Definition at line 153 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 255 of file generate_function_bodies.cpp.
References globals_to_havoc, havoc_expr_rec(), id2string(), symbol_table_baset::lookup_ref(), parameters_to_havoc, remove_skip(), typet::subtype(), to_pointer_type(), and exprt::type().
|
inlineprivate |
Definition at line 165 of file generate_function_bodies.cpp.
References messaget::eom(), namespace_baset::follow(), format(), from_integer(), INVARIANT, numeric_cast(), exprt::source_location(), to_array_type(), to_struct_union_type(), exprt::type(), and messaget::warning().
Referenced by generate_function_body_impl().
|
private |
Definition at line 319 of file generate_function_bodies.cpp.
Referenced by generate_function_body_impl().
|
private |
Definition at line 320 of file generate_function_bodies.cpp.
Referenced by generate_function_body_impl().