remove_exceptions.h File Reference

Remove function exceptional returns. More...

#include <util/irep.h>

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 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.

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.

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.

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.

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.