Merge pull request #329 from smowton/fix_dup2

Fix dup2, pop2 et al operating on pointers

Author: Daniel Kroening

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,15 +1189,15 @@ 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);
 
       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")