cprover
|
Remove exception handling. More...
#include "remove_exceptions.h"
#include "remove_instanceof.h"
#include <stack>
#include <algorithm>
#include <util/c_types.h>
#include <util/std_expr.h>
#include <util/std_code.h>
#include <util/symbol_table.h>
#include <goto-programs/remove_skip.h>
#include <analyses/uncaught_exceptions_analysis.h>
Go to the source code of this file.
Classes | |
class | remove_exceptionst |
Lowers high-level exception descriptions into low-level operations suitable for symex and other analyses that don't understand the THROW or CATCH GOTO instructions. More... | |
Functions | |
void | remove_exceptions (symbol_table_baset &symbol_table, goto_functionst &goto_functions, message_handlert &message_handler, remove_exceptions_typest type) |
removes throws/CATCH-POP/CATCH-PUSH More... | |
void | remove_exceptions (goto_programt &goto_program, symbol_table_baset &symbol_table, message_handlert &message_handler, remove_exceptions_typest type) |
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, message_handlert &message_handler, remove_exceptions_typest type) |
removes throws/CATCH-POP/CATCH-PUSH More... | |
Remove exception handling.
Definition in file remove_exceptions.cpp.
void remove_exceptions | ( | symbol_table_baset & | symbol_table, |
goto_functionst & | goto_functions, | ||
message_handlert & | message_handler, | ||
remove_exceptions_typest | type | ||
) |
removes throws/CATCH-POP/CATCH-PUSH
Definition at line 577 of file remove_exceptions.cpp.
References message_handler, REMOVE_ADDED_INSTANCEOF, and uncaught_exceptions().
Referenced by jbmc_parse_optionst::process_goto_function(), jbmc_parse_optionst::process_goto_functions(), jdiff_parse_optionst::process_goto_program(), janalyzer_parse_optionst::process_goto_program(), and remove_exceptions().
void remove_exceptions | ( | goto_programt & | goto_program, |
symbol_table_baset & | symbol_table, | ||
message_handlert & | message_handler, | ||
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. |
message_handler | logging output |
type | specifies whether instanceof operations generated by this pass should be lowered to class-identifier comparisons (using remove_instanceof). |
Definition at line 612 of file remove_exceptions.cpp.
References goto_program, message_handler, REMOVE_ADDED_INSTANCEOF, and remove_exceptions().
void remove_exceptions | ( | goto_modelt & | goto_model, |
message_handlert & | message_handler, | ||
remove_exceptions_typest | type | ||
) |
removes throws/CATCH-POP/CATCH-PUSH
Definition at line 630 of file remove_exceptions.cpp.
References goto_modelt::goto_functions, message_handler, remove_exceptions(), and goto_modelt::symbol_table.