9 #ifndef CPROVER_GOTO_PROGRAMS_GENERATE_FUNCTION_BODIES_H 10 #define CPROVER_GOTO_PROGRAMS_GENERATE_FUNCTION_BODIES_H 35 const irep_idt &function_name)
const = 0;
48 const irep_idt &function_name)
const;
57 const irep_idt &function_name)
const;
61 const std::string &options,
66 const std::regex &functions_regex,
72 #define OPT_REPLACE_FUNCTION_BODY \ 73 "(generate-function-body):" \ 74 "(generate-function-body-options):" 76 #define HELP_REPLACE_FUNCTION_BODY \ 77 " --generate-function-body <regex>\n" \ 79 " Generate bodies for functions matching regex\n" \ 80 " --generate-function-body-options <option>\n" \ 81 " One of assert-false, assume-false,\n" \ 83 " nondet-return, assert-false-assume-false and\n" \ 84 " havoc[,params:<regex>][,globals:<regex>]\n" \ 85 " (default: nondet-return)" 88 #endif // CPROVER_GOTO_PROGRAMS_GENERATE_FUNCTION_BODIES_H std::unique_ptr< generate_function_bodiest > generate_function_bodies_factory(const std::string &options, const symbol_tablet &symbol_table, message_handlert &message_handler)
Create the type that actually generates the functions.
virtual void generate_function_body_impl(goto_functiont &function, const 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...
void generate_function_bodies(const std::regex &functions_regex, const generate_function_bodiest &generate_function_body, goto_modelt &model, message_handlert &message_handler)
Generate function bodies with some default behavior A list of currently accepted command line argumen...
Base class for replace_function_body implementations.
void generate_parameter_names(goto_functiont &function, symbol_tablet &symbol_table, const irep_idt &function_name) const
Generate parameter names for unnamed parameters.
dstringt has one field, an unsigned integer no which is an index into a static table of strings...
A goto function, consisting of function type (see type), function body (see body), and parameter identifiers (see parameter_identifiers).
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...
virtual ~generate_function_bodiest()=default