remove_java_newt Class Reference

Collaboration diagram for remove_java_newt:

Public Member Functions
	remove_java_newt (symbol_table_baset &symbol_table)
bool	lower_java_new (const irep_idt &function_identifier, goto_programt &, message_handlert &)
	Replace every java_new or java_new_array by a malloc side-effect and zero initialization.
goto_programt::targett	lower_java_new (const irep_idt &function_identifier, goto_programt &, goto_programt::targett, message_handlert &)
	Replace every java_new or java_new_array by a malloc side-effect and zero initialization.

Protected Member Functions
goto_programt::targett	lower_java_new (const irep_idt &function_identifier, const exprt &lhs, const side_effect_exprt &rhs, goto_programt &, goto_programt::targett)
	Replaces the instruction lhs = new java_type by two instructions: lhs = ALLOCATE(java_type) *lhs = { zero-initialized java_type }.
goto_programt::targett	lower_java_new_array (const irep_idt &function_identifier, const exprt &lhs, const side_effect_exprt &rhs, goto_programt &, goto_programt::targett, message_handlert &)
	Replaces the instruction lhs = new java_array_type by the following code: lhs = ALLOCATE(java_type) loops to initialize the elements (including multi-dimensional arrays).

Protected Attributes
symbol_table_baset &	symbol_table
namespacet	ns

Detailed Description

Definition at line 29 of file remove_java_new.cpp.

Constructor & Destructor Documentation

remove_java_newt()

remove_java_newt::remove_java_newt ( symbol_table_baset & symbol_table )

inlineexplicit

Definition at line 32 of file remove_java_new.cpp.

Member Function Documentation

lower_java_new() [1/3]

goto_programt::targett remove_java_newt::lower_java_new ( const irep_idt & function_identifier, const exprt & lhs, const side_effect_exprt & rhs, goto_programt & dest, goto_programt::targett target )

protected

Replaces the instruction lhs = new java_type by two instructions: lhs = ALLOCATE(java_type) *lhs = { zero-initialized java_type }.

Parameters

function_identifier	Name of the function containing target.
lhs	the lhs
rhs	the rhs
dest	the goto program to modify
target	the goto instruction to replace

Returns

the iterator advanced to the last of the inserted instructions Note: we have to take a copy of lhs and rhs since they would suffer destruction when replacing the instruction.

Definition at line 82 of file remove_java_new.cpp.

lower_java_new() [2/3]

goto_programt::targett remove_java_newt::lower_java_new	(	const irep_idt &	function_identifier,
		goto_programt &	goto_program,
		goto_programt::targett	target,
		message_handlert &	message_handler )

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

Parameters

function_identifier	Name of the function containing target.
goto_program	program to process
target	instruction to check for java_new expressions
message_handler	message handler

Returns

true if a replacement has been made

Definition at line 362 of file remove_java_new.cpp.

lower_java_new() [3/3]

bool remove_java_newt::lower_java_new	(	const irep_idt &	function_identifier,
		goto_programt &	goto_program,
		message_handlert &	message_handler )

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

Extra auxiliary variables may be introduced into symbol_table.

Parameters

function_identifier	Name of the function goto_program.
goto_program	The function body to work on.
message_handler	message handler

Returns

true if one or more java_new expressions have been replaced

Definition at line 408 of file remove_java_new.cpp.

lower_java_new_array()

goto_programt::targett remove_java_newt::lower_java_new_array ( const irep_idt & function_identifier, const exprt & lhs, const side_effect_exprt & rhs, goto_programt & dest, goto_programt::targett target, message_handlert & message_handler )

protected

Replaces the instruction lhs = new java_array_type by the following code: lhs = ALLOCATE(java_type) loops to initialize the elements (including multi-dimensional arrays).

Parameters

function_identifier	Name of the function containing target.
lhs	the lhs
rhs	the rhs
dest	the goto program to modify
target	the goto instruction to replace
message_handler	message handler

Returns

the iterator advanced to the last of the inserted instructions Note: we have to take a copy of lhs and rhs since they would suffer destruction when replacing the instruction.

Definition at line 132 of file remove_java_new.cpp.

Member Data Documentation

ns

namespacet remove_java_newt::ns

protected

Definition at line 52 of file remove_java_new.cpp.

symbol_table

symbol_table_baset& remove_java_newt::symbol_table

protected

Definition at line 51 of file remove_java_new.cpp.

---

The documentation for this class was generated from the following file:

• /builddir/build/BUILD/cbmc-6.9.0-build/cbmc-cbmc-6.9.0/jbmc/src/java_bytecode/remove_java_new.cpp