cprover
generate_function_bodies.h
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: Replace bodies of goto functions
4 
5 Author: 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 
17 #include <util/cmdline.h>
18 #include <util/message.h>
19 #include <util/std_code.h>
20 #include <util/std_types.h>
21 
24 {
25 protected:
32  virtual void generate_function_body_impl(
33  goto_functiont &function,
34  const symbol_tablet &symbol_table,
35  const irep_idt &function_name) const = 0;
36 
37 public:
38  virtual ~generate_function_bodiest() = default;
39 
46  goto_functiont &function,
47  symbol_tablet &symbol_table,
48  const irep_idt &function_name) const;
49 
50 private:
55  goto_functiont &function,
56  symbol_tablet &symbol_table,
57  const irep_idt &function_name) const;
58 };
59 
60 std::unique_ptr<generate_function_bodiest> generate_function_bodies_factory(
61  const std::string &options,
62  const symbol_tablet &symbol_table,
63  message_handlert &message_handler);
64 
66  const std::regex &functions_regex,
67  const generate_function_bodiest &generate_function_body,
68  goto_modelt &model,
69  message_handlert &message_handler);
70 
71 // clang-format off
72 #define OPT_REPLACE_FUNCTION_BODY \
73  "(generate-function-body):" \
74  "(generate-function-body-options):"
75 
76 #define HELP_REPLACE_FUNCTION_BODY \
77  " --generate-function-body <regex>\n" \
78  /* NOLINTNEXTLINE(whitespace/line_length) */ \
79  " Generate bodies for functions matching regex\n" \
80  " --generate-function-body-options <option>\n" \
81  " One of assert-false, assume-false,\n" \
82  /* NOLINTNEXTLINE(whitespace/line_length) */ \
83  " nondet-return, assert-false-assume-false and\n" \
84  " havoc[,params:<regex>][,globals:<regex>]\n" \
85  " (default: nondet-return)"
86 // clang-format on
87 
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.
Symbol Table + CFG.
The symbol table.
Definition: symbol_table.h:19
dstringt has one field, an unsigned integer no which is an index into a static table of strings...
Definition: dstring.h:35
A goto function, consisting of function type (see type), function body (see body), and parameter identifiers (see parameter_identifiers).
Definition: goto_function.h:26
Pre-defined types.
Goto Function.
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