cprover
remove_exceptions.cpp File Reference

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>
Include dependency graph for remove_exceptions.cpp:

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, remove_exceptions_typest type)
 removes throws/CATCH-POP/CATCH-PUSH More...
 
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. More...
 
void remove_exceptions (goto_modelt &goto_model, remove_exceptions_typest type)
 removes throws/CATCH-POP/CATCH-PUSH More...
 

Detailed Description

Remove exception handling.

Definition in file remove_exceptions.cpp.

Function Documentation

◆ remove_exceptions() [1/3]

◆ remove_exceptions() [2/3]

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.

Parameters
goto_programprogram to remove exceptions from
symbol_tableglobal symbol table. The @inflight_exception global may be added if not already present. It will not be initialised; that is the caller's responsibility.
typespecifies 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().

◆ remove_exceptions() [3/3]

void remove_exceptions ( goto_modelt goto_model,
remove_exceptions_typest  type 
)

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.