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
 

Functions

void remove_exceptions_using_instanceof (const irep_idt &function_identifier, goto_programt &, symbol_table_baset &, message_handlert &)
 Removes 'throw x' and CATCH-PUSH/CATCH-POP and adds the required instrumentation (GOTOs and assignments) This introduces instanceof expressions. More...
 
void remove_exceptions_using_instanceof (goto_modelt &, message_handlert &)
 Removes 'throw x' and CATCH-PUSH/CATCH-POP and adds the required instrumentation (GOTOs and assignments) This introduces instanceof expressions. More...
 
void remove_exceptions (const irep_idt &function_identifier, goto_programt &, symbol_table_baset &, const class_hierarchyt &, message_handlert &)
 Removes 'throw x' and CATCH-PUSH/CATCH-POP and adds the required instrumentation (GOTOs and assignments) This does not introduce instanceof expressions. More...
 
void remove_exceptions (goto_modelt &, const class_hierarchyt &, message_handlert &)
 Removes 'throw x' and CATCH-PUSH/CATCH-POP and adds the required instrumentation (GOTOs and assignments) This does not introduce instanceof expressions. 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 22 of file remove_exceptions.h.

◆ INFLIGHT_EXCEPTION_VARIABLE_NAME

#define INFLIGHT_EXCEPTION_VARIABLE_NAME   "java::" INFLIGHT_EXCEPTION_VARIABLE_BASENAME

Definition at line 23 of file remove_exceptions.h.

Function Documentation

◆ remove_exceptions() [1/2]

void remove_exceptions ( const irep_idt function_identifier,
goto_programt goto_program,
symbol_table_baset symbol_table,
const class_hierarchyt class_hierarchy,
message_handlert message_handler 
)

Removes 'throw x' and CATCH-PUSH/CATCH-POP and adds the required instrumentation (GOTOs and assignments) This does not introduce instanceof expressions.

Removes 'throw x' and CATCH-PUSH/CATCH-POP and adds the required instrumentation (GOTOs and assignments) This does not introduce instanceof expressions.

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
function_identifiername of the goto function being processed
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.
class_hierarchyclass hierarchy analysis of symbol_table. Only needed if type == REMOVE_ADDED_INSTANCEOF; otherwise may be null.
message_handlerlogging output

Definition at line 706 of file remove_exceptions.cpp.

◆ remove_exceptions() [2/2]

void remove_exceptions ( goto_modelt goto_model,
const class_hierarchyt class_hierarchy,
message_handlert message_handler 
)

Removes 'throw x' and CATCH-PUSH/CATCH-POP and adds the required instrumentation (GOTOs and assignments) This does not introduce instanceof expressions.

Removes 'throw x' and CATCH-PUSH/CATCH-POP and adds the required instrumentation (GOTOs and assignments) This does not introduce instanceof expressions.

Parameters
goto_modelmodel to remove exceptions from. The @inflight_exception global may be added to its symbol table if not already present. It will not be initialised; that is the caller's responsibility.
class_hierarchyclass hierarchy analysis of symbol_table. Only needed if type == REMOVE_ADDED_INSTANCEOF; otherwise may be null.
message_handlerlogging output

Definition at line 735 of file remove_exceptions.cpp.

◆ remove_exceptions_using_instanceof() [1/2]

void remove_exceptions_using_instanceof ( const irep_idt function_identifier,
goto_programt goto_program,
symbol_table_baset symbol_table,
message_handlert message_handler 
)

Removes 'throw x' and CATCH-PUSH/CATCH-POP and adds the required instrumentation (GOTOs and assignments) This introduces instanceof expressions.

Removes 'throw x' and CATCH-PUSH/CATCH-POP and adds the required instrumentation (GOTOs and assignments) This introduces instanceof expressions.

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
function_identifiername of the goto function being processed
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

Definition at line 639 of file remove_exceptions.cpp.

◆ remove_exceptions_using_instanceof() [2/2]

void remove_exceptions_using_instanceof ( goto_modelt goto_model,
message_handlert message_handler 
)

Removes 'throw x' and CATCH-PUSH/CATCH-POP and adds the required instrumentation (GOTOs and assignments) This introduces instanceof expressions.

Removes 'throw x' and CATCH-PUSH/CATCH-POP and adds the required instrumentation (GOTOs and assignments) This introduces instanceof expressions.

Parameters
goto_modelmodel to remove exceptions from. The @inflight_exception global may be added to its symbol table if not already present. It will not be initialised; that is the caller's responsibility.
message_handlerlogging output

Definition at line 661 of file remove_exceptions.cpp.