CBMC
rebuild_goto_start_function.h
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: Goto Programs
4 
5 Author: Thomas Kiley, thomas@diffblue.com
6 
7 \*******************************************************************/
8 
11 
12 #ifndef CPROVER_GOTO_PROGRAMS_REBUILD_GOTO_START_FUNCTION_H
13 #define CPROVER_GOTO_PROGRAMS_REBUILD_GOTO_START_FUNCTION_H
14 
15 #include <memory>
16 
17 #include <util/irep.h>
18 
19 class languaget;
20 class message_handlert;
21 class optionst;
22 class symbol_table_baset;
23 
26 void remove_existing_entry_point(symbol_table_baset &);
27 
31 const irep_idt &get_entry_point_mode(const symbol_table_baset &);
32 
37 std::unique_ptr<languaget> get_entry_point_language(
38  const symbol_table_baset &symbol_table,
39  const optionst &options,
40  message_handlert &message_handler);
41 
42 #endif // CPROVER_GOTO_PROGRAMS_REBUILD_GOTO_START_FUNCTION_H
dstringt
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:38
message_handlert
Definition: message.h:27
symbol_table_baset
The symbol table base class interface.
Definition: symbol_table_base.h:23
get_entry_point_language
std::unique_ptr< languaget > get_entry_point_language(const symbol_table_baset &symbol_table, const optionst &options, message_handlert &message_handler)
Find the language corresponding to the __CPROVER_start function.
Definition: rebuild_goto_start_function.cpp:24
remove_existing_entry_point
void remove_existing_entry_point(symbol_table_baset &)
Eliminate the existing entry point function symbol and any symbols created in that scope from the sym...
Definition: rebuild_goto_start_function.cpp:46
get_entry_point_mode
const irep_idt & get_entry_point_mode(const symbol_table_baset &)
Find out the mode of the current entry point to determine the mode of the replacement entry point.
Definition: rebuild_goto_start_function.cpp:39