diff --git a/src/java_bytecode/java_bytecode_convert_method.cpp b/src/java_bytecode/java_bytecode_convert_method.cpp index 73c1b6022c4..4fd33ae121a 100644 --- a/src/java_bytecode/java_bytecode_convert_method.cpp +++ b/src/java_bytecode/java_bytecode_convert_method.cpp @@ -493,6 +493,13 @@ Function: java_bytecode_convert_methodt::convert_instructions \*******************************************************************/ +static unsigned get_bytecode_type_width(const typet& ty) +{ + if(ty.id()==ID_pointer) + return 32; + return ty.get_unsigned_int(ID_width); +} + codet java_bytecode_convert_methodt::convert_instructions( const instructionst &instructions, const code_typet &method_type) @@ -1158,7 +1165,7 @@ codet java_bytecode_convert_methodt::convert_instructions( { assert(!stack.empty() && results.empty()); - if(stack.back().type().get_unsigned_int(ID_width)==32) + if(get_bytecode_type_width(stack.back().type())==32) op=pop(2); else op=pop(1); @@ -1170,7 +1177,7 @@ codet java_bytecode_convert_methodt::convert_instructions( { assert(!stack.empty() && results.empty()); - if(stack.back().type().get_unsigned_int(ID_width)==32) + if(get_bytecode_type_width(stack.back().type())==32) op=pop(3); else op=pop(2); @@ -1182,7 +1189,7 @@ codet java_bytecode_convert_methodt::convert_instructions( { assert(!stack.empty() && results.empty()); - if(stack.back().type().get_unsigned_int(ID_width)==32) + if(get_bytecode_type_width(stack.back().type())==32) op=pop(2); else op=pop(1); @@ -1190,7 +1197,7 @@ codet java_bytecode_convert_methodt::convert_instructions( assert(!stack.empty()); exprt::operandst op2; - if(stack.back().type().get_unsigned_int(ID_width)==32) + if(get_bytecode_type_width(stack.back().type())==32) op2=pop(2); else op2=pop(1); @@ -1387,7 +1394,7 @@ codet java_bytecode_convert_methodt::convert_instructions( // two-word item (i.e. a double or a long). // http://cs.au.dk/~mis/dOvs/jvmspec/ref-pop2.html if(statement=="pop2" && - op[0].type().get_unsigned_int(ID_width)==32) + get_bytecode_type_width(op[0].type())==32) pop(1); } else if(statement=="instanceof")