cprover
rebuild_goto_start_function.h
Go to the documentation of this file.
1 /*******************************************************************\
2  Module: Goto Programs
3  Author: Thomas Kiley, thomas@diffblue.com
4 \*******************************************************************/
5 
8 
9 #ifndef CPROVER_GOTO_PROGRAMS_REBUILD_GOTO_START_FUNCTION_H
10 #define CPROVER_GOTO_PROGRAMS_REBUILD_GOTO_START_FUNCTION_H
11 
12 #include <util/message.h>
13 class optionst;
14 
15 #include "lazy_goto_model.h"
16 
17 
18 class symbol_tablet;
19 class goto_functionst;
20 
21 #define OPT_FUNCTIONS \
22  "(function):"
23 
24 #define HELP_FUNCTIONS \
25  " --function name set main function name\n"
26 
27 template<typename maybe_lazy_goto_modelt>
29 {
30 public:
32  const optionst &options,
33  maybe_lazy_goto_modelt &goto_model,
35 
36  bool operator()();
37 
38 private:
40 
42 
43  const optionst &options;
44  maybe_lazy_goto_modelt &goto_model;
45 };
46 
47 // NOLINTNEXTLINE(readability/namespace) using required for templates
50 
51 // NOLINTNEXTLINE(readability/namespace) using required for templates
54 
55 #endif // CPROVER_GOTO_PROGRAMS_REBUILD_GOTO_START_FUNCTION_H
messaget
Class that provides messages with a built-in verbosity 'level'.
Definition: message.h:144
dstringt
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:35
symbol_tablet
The symbol table.
Definition: symbol_table.h:19
optionst
Definition: options.h:22
rebuild_goto_start_function_baset::options
const optionst & options
Definition: rebuild_goto_start_function.h:43
lazy_goto_model.h
Author: Diffblue Ltd.
rebuild_goto_start_function_baset::rebuild_goto_start_function_baset
rebuild_goto_start_function_baset(const optionst &options, maybe_lazy_goto_modelt &goto_model, message_handlert &message_handler)
To rebuild the _start function in the event the program was compiled into GOTO with a different entry...
Definition: rebuild_goto_start_function.cpp:30
rebuild_goto_start_function_baset::operator()
bool operator()()
To rebuild the _start function in the event the program was compiled into GOTO with a different entry...
Definition: rebuild_goto_start_function.cpp:45
message_handlert
Definition: message.h:24
rebuild_goto_start_function_baset::goto_model
maybe_lazy_goto_modelt & goto_model
Definition: rebuild_goto_start_function.h:44
goto_functionst
A collection of goto functions.
Definition: goto_functions.h:22
messaget::message_handler
message_handlert * message_handler
Definition: message.h:426
rebuild_goto_start_function_baset::remove_existing_entry_point
void remove_existing_entry_point()
Eliminate the existing entry point function symbol and any symbols created in that scope from the sym...
Definition: rebuild_goto_start_function.cpp:85
message.h
rebuild_goto_start_function_baset::get_entry_point_mode
irep_idt get_entry_point_mode() const
Find out the mode of the current entry point to determine the mode of the replacement entry point.
Definition: rebuild_goto_start_function.cpp:74
rebuild_goto_start_function_baset
Definition: rebuild_goto_start_function.h:28