@@ -1592,16 +1592,7 @@ codet java_bytecode_convert_methodt::convert_instructions(
1592
1592
}
1593
1593
else if (statement==" pop" || statement==" pop2" )
1594
1594
{
1595
- // these are skips
1596
- c=code_skipt ();
1597
-
1598
- // pop2 removes two single-word items from the stack (e.g. two
1599
- // integers, or an integer and an object reference) or one
1600
- // two-word item (i.e. a double or a long).
1601
- // http://cs.au.dk/~mis/dOvs/jvmspec/ref-pop2.html
1602
- if (statement==" pop2" &&
1603
- get_bytecode_type_width (op[0 ].type ())==32 )
1604
- pop (1 );
1595
+ c = convert_pop (statement, op);
1605
1596
}
1606
1597
else if (statement==" instanceof" )
1607
1598
{
@@ -1871,6 +1862,22 @@ codet java_bytecode_convert_methodt::convert_instructions(
1871
1862
return code;
1872
1863
}
1873
1864
1865
+ codet java_bytecode_convert_methodt::convert_pop (
1866
+ const irep_idt &statement,
1867
+ const exprt::operandst &op)
1868
+ {
1869
+ // these are skips
1870
+ codet c = code_skipt ();
1871
+
1872
+ // pop2 removes two single-word items from the stack (e.g. two
1873
+ // integers, or an integer and an object reference) or one
1874
+ // two-word item (i.e. a double or a long).
1875
+ // http://cs.au.dk/~mis/dOvs/jvmspec/ref-pop2.html
1876
+ if (statement == " pop2" && get_bytecode_type_width (op[0 ].type ()) == 32 )
1877
+ pop (1 );
1878
+ return c;
1879
+ }
1880
+
1874
1881
codet java_bytecode_convert_methodt::convert_switch (
1875
1882
java_bytecode_convert_methodt::address_mapt &address_map,
1876
1883
const std::vector<java_bytecode_parse_treet::instructiont>::const_iterator
0 commit comments