CBMC
Loading...
Searching...
No Matches
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 bool ignore_no_match);
73
82 const std::string &function_name,
83 const std::string &call_site_id,
84 const generate_function_bodiest &generate_function_body,
85 goto_modelt &model,
86 message_handlert &message_handler);
87
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 " {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"
107
108#endif // CPROVER_GOTO_PROGRAMS_GENERATE_FUNCTION_BODIES_H
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition ai.h:562
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition dstring.h:38
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...
The symbol table.
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-...