Go to the documentation of this file.
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
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
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 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,...
Base class for replace_function_body implementations.
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 ~generate_function_bodiest()=default
A goto function, consisting of function type (see type), function body (see body),...
void generate_parameter_names(goto_functiont &function, symbol_tablet &symbol_table, const irep_idt &function_name) const
Generate parameter names for unnamed parameters.
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...