Go to the documentation of this file.
9 #ifndef CPROVER_GOTO_PROGRAMS_REBUILD_GOTO_START_FUNCTION_H
10 #define CPROVER_GOTO_PROGRAMS_REBUILD_GOTO_START_FUNCTION_H
21 #define OPT_FUNCTIONS \
24 #define HELP_FUNCTIONS \
25 " --function name set main function name\n"
27 template<
typename maybe_lazy_goto_modelt>
55 #endif // CPROVER_GOTO_PROGRAMS_REBUILD_GOTO_START_FUNCTION_H
Class that provides messages with a built-in verbosity 'level'.
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
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...
bool operator()()
To rebuild the _start function in the event the program was compiled into GOTO with a different entry...
maybe_lazy_goto_modelt & goto_model
A collection of goto functions.
message_handlert * message_handler
void remove_existing_entry_point()
Eliminate the existing entry point function symbol and any symbols created in that scope from the sym...
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.