remove_java_new.h File Reference

#include <goto-programs/goto_functions.h>

Include dependency graph for remove_java_new.h:

This graph shows which files directly or indirectly include this file:

Go to the source code of this file.

Functions
void	remove_java_new (const irep_idt &function_identifier, goto_programt::targett target, goto_programt &goto_program, symbol_table_baset &symbol_table, message_handlert &_message_handler)
	Replace every java_new or java_new_array by a malloc side-effect and zero initialization. More...
void	remove_java_new (const irep_idt &function_identifier, goto_functionst::goto_functiont &function, symbol_table_baset &symbol_table, message_handlert &_message_handler)
	Replace every java_new or java_new_array by a malloc side-effect and zero initialization. More...
void	remove_java_new (goto_functionst &goto_functions, symbol_table_baset &symbol_table, message_handlert &_message_handler)
	Replace every java_new or java_new_array by a malloc side-effect and zero initialization. More...
void	remove_java_new (goto_modelt &model, message_handlert &_message_handler)
	Replace every java_new or java_new_array by a malloc side-effect and zero initialization. More...

Detailed Description

Remove Java New Operators

Definition in file remove_java_new.h.

Function Documentation

remove_java_new() [1/4]

void remove_java_new	(	const irep_idt &	function_identifier,
		goto_functionst::goto_functiont &	function,
		symbol_table_baset &	symbol_table,
		message_handlert &	message_handler
	)

Replace every java_new or java_new_array by a malloc side-effect and zero initialization.

Remarks

Extra auxiliary variables may be introduced into symbol_table.

Parameters

function_identifier	Name of the function function.
function	The function to work on.
symbol_table	The symbol table to add symbols to.
message_handler	a message handler

Definition at line 456 of file remove_java_new.cpp.

remove_java_new() [2/4]

void remove_java_new	(	const irep_idt &	function_identifier,
		goto_programt::targett	target,
		goto_programt &	goto_program,
		symbol_table_baset &	symbol_table,
		message_handlert &	message_handler
	)

Replace every java_new or java_new_array by a malloc side-effect and zero initialization.

Remarks

Extra auxiliary variables may be introduced into symbol_table.

Parameters

function_identifier	Name of the function containing target.
target	The instruction to work on.
goto_program	The function body containing the instruction.
symbol_table	The symbol table to add symbols to.
message_handler	a message handler

Definition at line 437 of file remove_java_new.cpp.

remove_java_new() [3/4]

void remove_java_new	(	goto_functionst &	goto_functions,
		symbol_table_baset &	symbol_table,
		message_handlert &	message_handler
	)

Replace every java_new or java_new_array by a malloc side-effect and zero initialization.

Remarks

Extra auxiliary variables may be introduced into symbol_table.

Parameters

goto_functions	The functions to work on.
symbol_table	The symbol table to add symbols to.
message_handler	a message handler

Definition at line 472 of file remove_java_new.cpp.

remove_java_new() [4/4]

void remove_java_new	(	goto_modelt &	goto_model,
		message_handlert &	message_handler
	)

Replace every java_new or java_new_array by a malloc side-effect and zero initialization.

Remarks

Extra auxiliary variables may be introduced into symbol_table.

Parameters

goto_model	The functions to work on and the symbol table to add symbols to.
message_handler	a message handler

Definition at line 492 of file remove_java_new.cpp.