cprover
remove_exceptions.h File Reference

Remove function exceptional returns. More...

Include dependency graph for remove_exceptions.h:
This graph shows which files directly or indirectly include this file:

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, message_handlert &message_handler, 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, message_handlert &message_handler, remove_exceptions_typest type=remove_exceptions_typest::DONT_REMOVE_INSTANCEOF)
 removes throws/CATCH-POP/CATCH-PUSH More...
 

Detailed Description

Remove function exceptional returns.

Definition in file remove_exceptions.h.

Macro Definition Documentation

◆ INFLIGHT_EXCEPTION_VARIABLE_BASENAME

#define INFLIGHT_EXCEPTION_VARIABLE_BASENAME   "@inflight_exception"

Definition at line 21 of file remove_exceptions.h.

Referenced by java_internal_additions().

◆ INFLIGHT_EXCEPTION_VARIABLE_NAME

#define INFLIGHT_EXCEPTION_VARIABLE_NAME   "java::" INFLIGHT_EXCEPTION_VARIABLE_BASENAME

Enumeration Type Documentation

◆ remove_exceptions_typest

Enumerator
REMOVE_ADDED_INSTANCEOF 
DONT_REMOVE_INSTANCEOF 

Definition at line 28 of file remove_exceptions.h.

Function Documentation

◆ remove_exceptions() [1/2]

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.

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.
message_handlerlogging output
typespecifies 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().

◆ remove_exceptions() [2/2]

void remove_exceptions ( goto_modelt goto_model,
message_handlert message_handler,
remove_exceptions_typest  type = remove_exceptions_typest::DONT_REMOVE_INSTANCEOF 
)

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.