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 cmdlinet;
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 cmdlinet &cmdline,
33  maybe_lazy_goto_modelt &goto_model,
35 
36  bool operator()();
37 
38 private:
40 
42 
43  const cmdlinet &cmdline;
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
rebuild_goto_start_function_baset(const cmdlinet &cmdline, 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...
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...
The symbol table.
Definition: symbol_table.h:19
bool operator()()
To rebuild the _start function in the event the program was compiled into GOTO with a different entry...
Author: Diffblue Ltd.
void remove_existing_entry_point()
Eliminate the existing entry point function symbol and any symbols created in that scope from the sym...
message_handlert * message_handler
Definition: message.h:342