CBMC
|
Base class for replace_function_body implementations. More...
#include <generate_function_bodies.h>
Public Member Functions | |
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 | |
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 | generate_parameter_names (goto_functiont &function, symbol_tablet &symbol_table, const irep_idt &function_name) const |
Generate parameter names for unnamed parameters. More... | |
Base class for replace_function_body implementations.
Definition at line 24 of file generate_function_bodies.h.
|
virtualdefault |
void generate_function_bodiest::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.
function | whose body to replace |
symbol_table | of the current goto program |
function_name | Identifier of function |
Definition at line 24 of file generate_function_bodies.cpp.
|
protectedpure virtual |
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 |
Implemented in havoc_generate_function_bodiest, assert_false_then_assume_false_generate_function_bodiest, assert_false_generate_function_bodiest, and assume_false_generate_function_bodiest.
|
private |
Generate parameter names for unnamed parameters.
CBMC expect functions to have parameter names if they are called and have a body
Definition at line 34 of file generate_function_bodies.cpp.