cprover
remove_java_newt Class Reference
Inheritance diagram for remove_java_newt:
[legend]
Collaboration diagram for remove_java_newt:
[legend]

Public Member Functions

 remove_java_newt (symbol_table_baset &symbol_table, message_handlert &_message_handler)
 
bool lower_java_new (goto_programt &)
 Replace every java_new or java_new_array by a malloc side-effect and zero initialization. More...
 
goto_programt::targett lower_java_new (goto_programt &, goto_programt::targett)
 Replace every java_new or java_new_array by a malloc side-effect and zero initialization. More...
 
- Public Member Functions inherited from messaget
virtual void set_message_handler (message_handlert &_message_handler)
 
message_handlertget_message_handler ()
 
 messaget ()
 
 messaget (const messaget &other)
 
messagetoperator= (const messaget &other)
 
 messaget (message_handlert &_message_handler)
 
virtual ~messaget ()
 
mstreamtget_mstream (unsigned message_level) const
 
mstreamterror () const
 
mstreamtwarning () const
 
mstreamtresult () const
 
mstreamtstatus () const
 
mstreamtstatistics () const
 
mstreamtprogress () const
 
mstreamtdebug () const
 
void conditional_output (mstreamt &mstream, const std::function< void(mstreamt &)> &output_generator) const
 Generate output to mstream using output_generator if the configured verbosity is at least as high as that of mstream. More...
 

Protected Member Functions

goto_programt::targett lower_java_new (exprt lhs, 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 (exprt lhs, side_effect_exprt rhs, goto_programt &, goto_programt::targett)
 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
 
- Protected Attributes inherited from messaget
message_handlertmessage_handler
 
mstreamt mstream
 

Additional Inherited Members

- Public Types inherited from messaget
enum  message_levelt {
  M_ERROR =1, M_WARNING =2, M_RESULT =4, M_STATUS =6,
  M_STATISTICS =8, M_PROGRESS =9, M_DEBUG =10
}
 
- Static Public Member Functions inherited from messaget
static unsigned eval_verbosity (const std::string &user_input, const message_levelt default_verbosity, message_handlert &dest)
 Parse a (user-)provided string as a verbosity level and set it as the verbosity of dest. More...
 
static mstreamteom (mstreamt &m)
 
static mstreamtendl (mstreamt &m)
 

Detailed Description

Definition at line 25 of file remove_java_new.cpp.

Constructor & Destructor Documentation

◆ remove_java_newt()

remove_java_newt::remove_java_newt ( symbol_table_baset symbol_table,
message_handlert _message_handler 
)
inline

Definition at line 28 of file remove_java_new.cpp.

Member Function Documentation

◆ lower_java_new() [1/3]

bool remove_java_newt::lower_java_new ( goto_programt goto_program)

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
goto_programThe function body to work on.
Returns
true if one or more java_new expressions have been replaced

Definition at line 358 of file remove_java_new.cpp.

References goto_program, goto_programt::instructions, and goto_programt::update().

Referenced by lower_java_new(), lower_java_new_array(), and remove_java_new().

◆ lower_java_new() [2/3]

goto_programt::targett remove_java_newt::lower_java_new ( goto_programt goto_program,
goto_programt::targett  target 
)

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

Parameters
goto_programprogram to process
targetinstruction to check for java_new expressions
Returns
true if a replacement has been made

Definition at line 327 of file remove_java_new.cpp.

References expr_try_dynamic_cast(), irept::get(), goto_program, irept::id(), lower_java_new(), lower_java_new_array(), and to_side_effect_expr().

◆ lower_java_new() [3/3]

goto_programt::targett remove_java_newt::lower_java_new ( exprt  lhs,
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
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 70 of file remove_java_new.cpp.

References CHECK_RETURN, exprt::copy_to_operands(), messaget::get_message_handler(), irept::id(), goto_programt::insert_after(), irept::is_nil(), irept::is_not_nil(), ns, object_size(), exprt::operands(), PRECONDITION, set_class_identifier(), size_of_expr(), exprt::source_location(), typet::subtype(), to_struct_expr(), to_symbol_type(), exprt::type(), and zero_initializer().

◆ lower_java_new_array()

goto_programt::targett remove_java_newt::lower_java_new_array ( exprt  lhs,
side_effect_exprt  rhs,
goto_programt dest,
goto_programt::targett  target 
)
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
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 118 of file remove_java_new.cpp.

References exprt::add_source_location(), code_fort::body(), CHECK_RETURN, struct_union_typet::components(), code_fort::cond(), exprt::copy_to_operands(), goto_programt::destructive_insert(), irept::find(), namespace_baset::follow(), from_integer(), irept::get_bool(), get_fresh_aux_symbol(), messaget::get_message_handler(), goto_convert(), irept::id(), id2string(), code_fort::init(), goto_programt::insert_before(), goto_programt::instructions, irept::is_nil(), code_fort::iter(), lower_java_new(), ns, object_size(), exprt::op0(), exprt::op1(), exprt::operands(), pointer_type(), PRECONDITION, irept::set(), set_class_identifier(), size_of_expr(), exprt::source_location(), typet::subtype(), symbolt::symbol_expr(), symbol_table, to_struct_expr(), to_struct_type(), to_symbol_type(), exprt::type(), and zero_initializer().

Referenced by lower_java_new().

Member Data Documentation

◆ ns

namespacet remove_java_newt::ns
protected

Definition at line 44 of file remove_java_new.cpp.

Referenced by lower_java_new(), and lower_java_new_array().

◆ symbol_table

symbol_table_baset& remove_java_newt::symbol_table
protected

Definition at line 43 of file remove_java_new.cpp.

Referenced by lower_java_new_array().


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