@@ -1484,22 +1484,7 @@ codet java_bytecode_convert_methodt::convert_instructions(
1484
1484
else if (statement==" dup2_x2" )
1485
1485
{
1486
1486
PRECONDITION (!stack.empty () && results.empty ());
1487
-
1488
- if (get_bytecode_type_width (stack.back ().type ())==32 )
1489
- op=pop (2 );
1490
- else
1491
- op=pop (1 );
1492
-
1493
- exprt::operandst op2;
1494
-
1495
- if (get_bytecode_type_width (stack.back ().type ())==32 )
1496
- op2=pop (2 );
1497
- else
1498
- op2=pop (1 );
1499
-
1500
- results.insert (results.end (), op.begin (), op.end ());
1501
- results.insert (results.end (), op2.begin (), op2.end ());
1502
- results.insert (results.end (), op.begin (), op.end ());
1487
+ convert_dup2_x2 (op, results);
1503
1488
}
1504
1489
else if (statement==" dconst" )
1505
1490
{
@@ -1955,6 +1940,27 @@ void java_bytecode_convert_methodt::convert_dup2_x1(
1955
1940
results.insert (results.end (), op.begin (), op.end ());
1956
1941
}
1957
1942
1943
+ void java_bytecode_convert_methodt::convert_dup2_x2 (
1944
+ exprt::operandst &op,
1945
+ exprt::operandst &results)
1946
+ {
1947
+ if (get_bytecode_type_width (stack.back ().type ()) == 32 )
1948
+ op = pop (2 );
1949
+ else
1950
+ op = pop (1 );
1951
+
1952
+ exprt::operandst op2;
1953
+
1954
+ if (get_bytecode_type_width (stack.back ().type ()) == 32 )
1955
+ op2 = pop (2 );
1956
+ else
1957
+ op2 = pop (1 );
1958
+
1959
+ results.insert (results.end (), op.begin (), op.end ());
1960
+ results.insert (results.end (), op2.begin (), op2.end ());
1961
+ results.insert (results.end (), op.begin (), op.end ());
1962
+ }
1963
+
1958
1964
exprt::operandst &java_bytecode_convert_methodt::convert_const (
1959
1965
const irep_idt &statement,
1960
1966
exprt &arg0,
0 commit comments