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

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 }. More...
 
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) More...
 

Protected Attributes

symbol_table_basetsymbol_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_identifierName of the function containing target.
lhsthe lhs
rhsthe rhs
destthe goto program to modify
targetthe 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_identifierName of the function containing target.
goto_programprogram to process
targetinstruction to check for java_new expressions
message_handlermessage 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_identifierName of the function goto_program.
goto_programThe function body to work on.
message_handlermessage 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_identifierName of the function containing target.
lhsthe lhs
rhsthe rhs
destthe goto program to modify
targetthe goto instruction to replace
message_handlermessage 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: