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

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.

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 25 of file remove_exceptions.h.

◆ INFLIGHT_EXCEPTION_VARIABLE_NAME

#define INFLIGHT_EXCEPTION_VARIABLE_NAME "java::" INFLIGHT_EXCEPTION_VARIABLE_BASENAME

Definition at line 26 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.

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

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.

class_hierarchy class hierarchy analysis of symbol_table. Only needed if type == REMOVE_ADDED_INSTANCEOF; otherwise may be null.

message_handler logging output

Definition at line 723 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.

Parameters: goto_model model 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_hierarchy class hierarchy analysis of symbol_table. Only needed if type == REMOVE_ADDED_INSTANCEOF; otherwise may be null.

message_handler logging output

Definition at line 752 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.

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

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

Definition at line 656 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.

Parameters: goto_model model 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_handler logging output

Definition at line 678 of file remove_exceptions.cpp.