cprover
|
#include <rebuild_goto_start_function.h>
Public Member Functions | |
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 function selected. More... | |
bool | operator() () |
To rebuild the _start function in the event the program was compiled into GOTO with a different entry function selected. More... | |
Private Member Functions | |
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. More... | |
void | remove_existing_entry_point () |
Eliminate the existing entry point function symbol and any symbols created in that scope from the symbol table. More... | |
Private Attributes | |
const cmdlinet & | cmdline |
maybe_lazy_goto_modelt & | goto_model |
Additional Inherited Members |
Definition at line 28 of file rebuild_goto_start_function.h.
rebuild_goto_start_function_baset< maybe_lazy_goto_modelt >::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 function selected.
goto_model | The goto functions (to replace the body of the _start function) and symbol table (to replace the _start function symbol) of the program. |
_message_handler | The message handler to report any messages with |
Definition at line 29 of file rebuild_goto_start_function.cpp.
|
private |
Find out the mode of the current entry point to determine the mode of the replacement entry point.
Definition at line 77 of file rebuild_goto_start_function.cpp.
References goto_functionst::entry_point(), and symbolt::mode.
bool rebuild_goto_start_function_baset< maybe_lazy_goto_modelt >::operator() | ( | void | ) |
To rebuild the _start function in the event the program was compiled into GOTO with a different entry function selected.
It works by discarding the _start symbol and GOTO function and calling on the relevant languaget to generate the _start function again.
entry_function | The name of the entry function that should be called from _start |
Definition at line 48 of file rebuild_goto_start_function.cpp.
References goto_functionst::entry_point(), languaget::generate_support_functions(), get_language_from_mode(), languaget::get_language_options(), id2string(), INVARIANT, and messaget::set_message_handler().
|
private |
Eliminate the existing entry point function symbol and any symbols created in that scope from the symbol table.
Definition at line 88 of file rebuild_goto_start_function.cpp.
References goto_functionst::entry_point(), has_prefix(), and id2string().
|
private |
Definition at line 43 of file rebuild_goto_start_function.h.
|
private |
Definition at line 44 of file rebuild_goto_start_function.h.