@@ -119,7 +119,18 @@ class java_bytecode_convert_methodt:public messaget
119
119
}
120
120
121
121
// JVM local variables
122
- const exprt variable (const exprt &arg, char type_char, size_t address, instruction_sizet inst_size)
122
+ enum variable_cast_argumentt
123
+ {
124
+ CAST_AS_NEEDED,
125
+ NO_CAST
126
+ };
127
+
128
+ const exprt variable (
129
+ const exprt &arg,
130
+ char type_char,
131
+ size_t address,
132
+ instruction_sizet inst_size,
133
+ variable_cast_argumentt do_cast)
123
134
{
124
135
irep_idt number=to_constant_expr (arg).get_value ();
125
136
@@ -145,7 +156,7 @@ class java_bytecode_convert_methodt:public messaget
145
156
else
146
157
{
147
158
exprt result=var.symbol_expr ;
148
- if (t!=result.type ()) result=typecast_exprt (result, t);
159
+ if (do_cast==CAST_AS_NEEDED && t!=result.type ()) result=typecast_exprt (result, t);
149
160
return result;
150
161
}
151
162
}
@@ -829,7 +840,7 @@ codet java_bytecode_convert_methodt::convert_instructions(
829
840
// store value into some local variable
830
841
assert (op.size ()==1 && results.empty ());
831
842
832
- exprt var=variable (arg0, statement[0 ], i_it->address , INST_INDEX);
843
+ exprt var=variable (arg0, statement[0 ], i_it->address , INST_INDEX, NO_CAST );
833
844
834
845
const bool is_array (' a' == statement[0 ]);
835
846
@@ -861,7 +872,7 @@ codet java_bytecode_convert_methodt::convert_instructions(
861
872
else if (statement==patternt (" ?load" ))
862
873
{
863
874
// load a value from a local variable
864
- results[0 ]=variable (arg0, statement[0 ], i_it->address , INST_INDEX);
875
+ results[0 ]=variable (arg0, statement[0 ], i_it->address , INST_INDEX, CAST_AS_NEEDED );
865
876
}
866
877
else if (statement==" ldc" || statement==" ldc_w" ||
867
878
statement==" ldc2" || statement==" ldc2_w" )
@@ -1023,10 +1034,10 @@ codet java_bytecode_convert_methodt::convert_instructions(
1023
1034
else if (statement==" iinc" )
1024
1035
{
1025
1036
code_assignt code_assign;
1026
- code_assign.lhs ()=variable (arg0, ' i' , i_it->address , INST_INDEX_CONST);
1037
+ code_assign.lhs ()=variable (arg0, ' i' , i_it->address , INST_INDEX_CONST, NO_CAST );
1027
1038
code_assign.rhs ()=plus_exprt (
1028
- variable (arg0, ' i' , i_it->address , INST_INDEX_CONST),
1029
- typecast_exprt (arg1, java_int_type ()));
1039
+ variable (arg0, ' i' , i_it->address , INST_INDEX_CONST, CAST_AS_NEEDED ),
1040
+ typecast_exprt (arg1, java_int_type ()));
1030
1041
c=code_assign;
1031
1042
}
1032
1043
else if (statement==patternt (" ?xor" ))
0 commit comments