cprover
generate_function_bodies.h
Go to the documentation of this file.
1/*******************************************************************\
2
3Module: Replace bodies of goto functions
4
5Author: Diffblue Ltd.
6
7\*******************************************************************/
8
9#ifndef CPROVER_GOTO_PROGRAMS_GENERATE_FUNCTION_BODIES_H
10#define CPROVER_GOTO_PROGRAMS_GENERATE_FUNCTION_BODIES_H
11
12#include <memory>
13#include <regex>
14
15#include <util/irep.h>
16
17class goto_functiont;
18class goto_modelt;
20class symbol_tablet;
22
25{
26protected:
34 goto_functiont &function,
35 symbol_tablet &symbol_table,
36 const irep_idt &function_name) const = 0;
37
38public:
39 virtual ~generate_function_bodiest() = default;
40
47 goto_functiont &function,
48 symbol_tablet &symbol_table,
49 const irep_idt &function_name) const;
50
51private:
56 goto_functiont &function,
57 symbol_tablet &symbol_table,
58 const irep_idt &function_name) const;
59};
60
61std::unique_ptr<generate_function_bodiest> generate_function_bodies_factory(
62 const std::string &options,
63 const c_object_factory_parameterst &object_factory_parameters,
64 const symbol_tablet &symbol_table,
65 message_handlert &message_handler);
66
68 const std::regex &functions_regex,
69 const generate_function_bodiest &generate_function_body,
70 goto_modelt &model,
71 message_handlert &message_handler);
72
81 const std::string &function_name,
82 const std::string &call_site_id,
83 const generate_function_bodiest &generate_function_body,
84 goto_modelt &model,
85 message_handlert &message_handler);
86
87// clang-format off
88#define OPT_REPLACE_FUNCTION_BODY \
89 "(generate-function-body):" \
90 "(generate-havocing-body):" \
91 "(generate-function-body-options):"
92
93#define HELP_REPLACE_FUNCTION_BODY \
94 " --generate-function-body <regex>\n" \
95 /* NOLINTNEXTLINE(whitespace/line_length) */ \
96 " Generate bodies for functions matching regex\n" \
97 " --generate-havocing-body <option>\n" \
98 /* NOLINTNEXTLINE(whitespace/line_length) */ \
99 " <fun_name>,params:<p_n1;p_n2;..>\n" \
100 " or\n" \
101 /* NOLINTNEXTLINE(whitespace/line_length) */ \
102 " <fun_name>[,<call-site-id>,params:<p_n1;p_n2;..>]+\n" \
103 " --generate-function-body-options <option>\n" \
104 " One of assert-false, assume-false,\n" \
105 /* NOLINTNEXTLINE(whitespace/line_length) */ \
106 " nondet-return, assert-false-assume-false and\n" \
107 " havoc[,params:<regex>][,globals:<regex>]\n" \
108 " [,params:<p_n1;p_n2;..>]\n" \
109 " (default: nondet-return)\n"
110// clang-format on
111
112#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.
Definition: dstring.h:37
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...
Definition: goto_function.h:24
The symbol table.
Definition: symbol_table.h:14
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)
Generate function bodies with some default behavior: assert-false, assume-false, assert-false-assume-...