@@ -25,6 +25,7 @@ Author: Daniel Kroening, kroening@kroening.com
2525#include < util/arith_tools.h>
2626#include < util/c_types.h>
2727#include < util/expr_initializer.h>
28+ #include < util/expr_util.h>
2829#include < util/ieee_float.h>
2930#include < util/invariant.h>
3031#include < util/namespace.h>
@@ -3184,28 +3185,34 @@ void java_bytecode_convert_methodt::save_stack_entries(
31843185{
31853186 for (auto &stack_entry : stack)
31863187 {
3188+ // remove typecasts if existing
3189+ const auto &entry = skip_typecast (stack_entry);
3190+
31873191 // variables or static fields and symbol -> save symbols with same id
3188- if ((write_type==bytecode_write_typet::VARIABLE ||
3189- write_type==bytecode_write_typet::STATIC_FIELD) &&
3190- stack_entry.id ()==ID_symbol)
3192+ if (
3193+ (write_type == bytecode_write_typet::VARIABLE ||
3194+ write_type == bytecode_write_typet::STATIC_FIELD) &&
3195+ entry.id () == ID_symbol)
31913196 {
3192- const symbol_exprt &var=to_symbol_expr (stack_entry);
3193- if (var.get_identifier ()==identifier)
3197+ if (to_symbol_expr (entry).get_identifier () == identifier)
31943198 create_stack_tmp_var (tmp_var_prefix, tmp_var_type, block, stack_entry);
31953199 }
31963200
31973201 // array reference and dereference -> save all references on the stack
3198- else if (write_type==bytecode_write_typet::ARRAY_REF &&
3199- stack_entry.id ()==ID_dereference)
3202+ else if (
3203+ write_type == bytecode_write_typet::ARRAY_REF &&
3204+ entry.id () == ID_dereference)
3205+ {
32003206 create_stack_tmp_var (tmp_var_prefix, tmp_var_type, block, stack_entry);
3207+ }
32013208
32023209 // field and member access -> compare component name
3203- else if (write_type==bytecode_write_typet::FIELD &&
3204- stack_entry.id ()==ID_member)
3210+ else if (
3211+ write_type == bytecode_write_typet::FIELD &&
3212+ entry.id () == ID_member)
32053213 {
3206- const irep_idt &entry_id=
3207- to_member_expr (stack_entry).get_component_name ();
3208- if (entry_id==identifier)
3214+ const irep_idt &entry_id = to_member_expr (entry).get_component_name ();
3215+ if (entry_id == identifier)
32093216 create_stack_tmp_var (tmp_var_prefix, tmp_var_type, block, stack_entry);
32103217 }
32113218 }
0 commit comments