cprover
|
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... | |
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_baset & | symbol_table |
namespacet | ns |
Additional Inherited Members |
Definition at line 25 of file remove_java_new.cpp.
|
inline |
Definition at line 28 of file remove_java_new.cpp.
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.
goto_program | The function body to work on. |
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().
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.
goto_program | program to process |
target | instruction to check for java_new expressions |
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().
|
protected |
Replaces the instruction lhs = new java_type
by two instructions: lhs = ALLOCATE(java_type) *lhs = { zero-initialized java_type }.
lhs | the lhs |
rhs | the rhs |
dest | the goto program to modify |
target | the goto instruction to replace |
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().
|
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)
lhs | the lhs |
rhs | the rhs |
dest | the goto program to modify |
target | the goto instruction to replace |
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().
|
protected |
Definition at line 44 of file remove_java_new.cpp.
Referenced by lower_java_new(), and lower_java_new_array().
|
protected |
Definition at line 43 of file remove_java_new.cpp.
Referenced by lower_java_new_array().