File tree 1 file changed +13
-4
lines changed
1 file changed +13
-4
lines changed Original file line number Diff line number Diff line change @@ -749,7 +749,6 @@ void java_bytecode_parsert::rbytecode(
749
749
instruction.args .push_back (from_integer (c, signedbv_typet (8 )));
750
750
}
751
751
address+=1 ;
752
-
753
752
break ;
754
753
755
754
case ' o' : // two byte branch offset, signed
@@ -776,10 +775,20 @@ void java_bytecode_parsert::rbytecode(
776
775
777
776
case ' v' : // local variable index (one byte)
778
777
{
779
- u1 v=read_u1 ();
780
- instruction.args .push_back (from_integer (v, unsignedbv_typet (8 )));
778
+ if (wide_instruction)
779
+ {
780
+ u2 v = read_u2 ();
781
+ instruction.args .push_back (from_integer (v, unsignedbv_typet (16 )));
782
+ address += 2 ;
783
+ }
784
+ else
785
+ {
786
+ u1 v = read_u1 ();
787
+ instruction.args .push_back (from_integer (v, unsignedbv_typet (8 )));
788
+ address += 1 ;
789
+ }
781
790
}
782
- address+= 1 ;
791
+
783
792
break ;
784
793
785
794
case ' V' :
You can’t perform that action at this time.
0 commit comments