cprover
|
Remove function exceptional returns. More...
#include <goto-programs/goto_model.h>
Go to the source code of this file.
Macros | |
#define | INFLIGHT_EXCEPTION_VARIABLE_BASENAME "@inflight_exception" |
#define | INFLIGHT_EXCEPTION_VARIABLE_NAME "java::" INFLIGHT_EXCEPTION_VARIABLE_BASENAME |
Enumerations | |
enum | remove_exceptions_typest { remove_exceptions_typest::REMOVE_ADDED_INSTANCEOF, remove_exceptions_typest::DONT_REMOVE_INSTANCEOF } |
Functions | |
void | remove_exceptions (goto_programt &goto_program, symbol_table_baset &symbol_table, remove_exceptions_typest type=remove_exceptions_typest::DONT_REMOVE_INSTANCEOF) |
removes throws/CATCH-POP/CATCH-PUSH from a single GOTO program, replacing them with explicit exception propagation. More... | |
void | remove_exceptions (goto_modelt &goto_model, remove_exceptions_typest type=remove_exceptions_typest::DONT_REMOVE_INSTANCEOF) |
removes throws/CATCH-POP/CATCH-PUSH More... | |
Remove function exceptional returns.
Definition in file remove_exceptions.h.
#define INFLIGHT_EXCEPTION_VARIABLE_BASENAME "@inflight_exception" |
Definition at line 19 of file remove_exceptions.h.
Referenced by java_internal_additions().
#define INFLIGHT_EXCEPTION_VARIABLE_NAME "java::" INFLIGHT_EXCEPTION_VARIABLE_BASENAME |
Definition at line 20 of file remove_exceptions.h.
Referenced by remove_exceptionst::get_inflight_exception_global(), java_internal_additions(), and ci_lazy_methodst::operator()().
|
strong |
Enumerator | |
---|---|
REMOVE_ADDED_INSTANCEOF | |
DONT_REMOVE_INSTANCEOF |
Definition at line 26 of file remove_exceptions.h.
void remove_exceptions | ( | goto_programt & | goto_program, |
symbol_table_baset & | symbol_table, | ||
remove_exceptions_typest | type | ||
) |
removes throws/CATCH-POP/CATCH-PUSH from a single GOTO program, replacing them with explicit exception propagation.
Note this is somewhat less accurate than the whole-goto-model version, because we can't inspect other functions to determine whether they throw or not, and therefore must assume they do and always introduce post-call exception dispatch.
goto_program | program to remove exceptions from |
symbol_table | global symbol table. The @inflight_exception global may be added if not already present. It will not be initialised; that is the caller's responsibility. |
type | specifies whether instanceof operations generated by this pass should be lowered to class-identifier comparisons (using remove_instanceof). |
Definition at line 606 of file remove_exceptions.cpp.
References goto_program, REMOVE_ADDED_INSTANCEOF, and remove_exceptions().
void remove_exceptions | ( | goto_modelt & | goto_model, |
remove_exceptions_typest | type = remove_exceptions_typest::DONT_REMOVE_INSTANCEOF |
||
) |
removes throws/CATCH-POP/CATCH-PUSH
Definition at line 622 of file remove_exceptions.cpp.
References goto_modelt::goto_functions, remove_exceptions(), and goto_modelt::symbol_table.