9#ifndef CPROVER_GOTO_PROGRAMS_GENERATE_FUNCTION_BODIES_H
10#define CPROVER_GOTO_PROGRAMS_GENERATE_FUNCTION_BODIES_H
36 const irep_idt &function_name)
const = 0;
49 const irep_idt &function_name)
const;
58 const irep_idt &function_name)
const;
62 const std::string &options,
82 const std::string &function_name,
88#define OPT_REPLACE_FUNCTION_BODY \
89 "(generate-function-body):" \
90 "(generate-havocing-body):" \
91 "(generate-function-body-options):"
93#define HELP_REPLACE_FUNCTION_BODY \
94 " {y--generate-function-body} {uregex} \t " \
95 "generate bodies for functions matching {uregex}\n" \
96 " {y--generate-havocing-body} <option> " \
97 "{ufun_name},{yparams}:{up1};{up2};.. \t " \
98 "generate havocing body\n" \
99 " {y--generate-havocing-body} <option> " \
100 "{ufun_name}[,{ucall-site-id},{yparams}:{up1};{up2};..]+ \t " \
101 "generate havocing body\n" \
102 " {y--generate-function-body-options} {uoption} \t " \
103 "One of {yassert-false}, {yassume-false}, {ynondet-return}, " \
104 "{yassert-false-assume-false} and " \
105 "{yhavoc}[,{yparams}:{uregex}][,{yglobals}:{uregex}]" \
106 "[,{yparams}:{up1};{up2};..] (default: {ynondet-return})\n"
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Base class for replace_function_body implementations.
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.
void generate_parameter_names(goto_functiont &function, symbol_tablet &symbol_table, const irep_idt &function_name) const
Generate parameter names for unnamed parameters.
virtual ~generate_function_bodiest()=default
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,...
A goto function, consisting of function body (see body) and parameter identifiers (see parameter_iden...
std::unique_ptr< generate_function_bodiest > generate_function_bodies_factory(const std::string &options, const c_object_factory_parameterst &object_factory_parameters, const symbol_tablet &symbol_table, message_handlert &message_handler)
Create the type that actually generates the functions.
void generate_function_bodies(const std::regex &functions_regex, const generate_function_bodiest &generate_function_body, goto_modelt &model, message_handlert &message_handler, bool ignore_no_match)
Generate function bodies with some default behavior: assert-false, assume-false, assert-false-assume-...