@@ -2096,15 +2096,15 @@ exprt::operandst &java_bytecode_convert_methodt::convert_const(
2096
2096
void java_bytecode_convert_methodt::convert_invoke (
2097
2097
source_locationt location,
2098
2098
const irep_idt &statement,
2099
- exprt &arg0 ,
2099
+ exprt &invoke_statement ,
2100
2100
codet &c,
2101
2101
exprt::operandst &results)
2102
2102
{
2103
2103
const bool use_this (statement != " invokestatic" );
2104
2104
const bool is_virtual (
2105
2105
statement == " invokevirtual" || statement == " invokeinterface" );
2106
2106
2107
- code_typet &code_type = to_code_type (arg0 .type ());
2107
+ code_typet &code_type = to_code_type (invoke_statement .type ());
2108
2108
code_typet::parameterst ¶meters (code_type.parameters ());
2109
2109
2110
2110
const std::string full_method_name = id2string (method_id);
@@ -2117,22 +2117,18 @@ void java_bytecode_convert_methodt::convert_invoke(
2117
2117
std::string class_type_name = calling_class_name.substr (6 );
2118
2118
std::replace (class_type_name.begin (), class_type_name.end (), ' .' , ' /' );
2119
2119
const auto &enum_clone_symbol = symbol_table.lookup_ref (calling_class_name);
2120
- const bool is_enum_values_clone_call =
2121
- enum_clone_symbol.type .get_bool (ID_enumeration) &&
2122
- (full_method_name ==
2123
- (calling_class_name + " .values:()[L" + class_type_name + " ;" ));
2124
2120
2125
2121
if (use_this)
2126
2122
{
2127
2123
if (parameters.empty () || !parameters[0 ].get_this ())
2128
2124
{
2129
- irep_idt classname = arg0 .get (ID_C_class);
2125
+ irep_idt classname = invoke_statement .get (ID_C_class);
2130
2126
typet thistype = symbol_typet (classname);
2131
2127
// Note invokespecial is used for super-method calls as well as
2132
2128
// constructors.
2133
2129
if (statement == " invokespecial" )
2134
2130
{
2135
- if (is_constructor (arg0 .get (ID_identifier)))
2131
+ if (is_constructor (invoke_statement .get (ID_identifier)))
2136
2132
{
2137
2133
if (needed_lazy_methods)
2138
2134
needed_lazy_methods->add_needed_class (classname);
@@ -2195,7 +2191,9 @@ void java_bytecode_convert_methodt::convert_invoke(
2195
2191
results[0 ] = promoted;
2196
2192
}
2197
2193
2198
- assert (arg0.id () == ID_virtual_function);
2194
+ DATA_INVARIANT (
2195
+ invoke_statement.id () == ID_virtual_function,
2196
+ " argument to invoke bytecode must be virtual function here" );
2199
2197
2200
2198
// If we don't have a definition for the called symbol, and we won't
2201
2199
// inherit a definition from a super-class, we create a new symbol and
@@ -2213,18 +2211,19 @@ void java_bytecode_convert_methodt::convert_invoke(
2213
2211
// generate code that may wrongly assume that such a method is
2214
2212
// accessible if we assume that its access attribute is "more
2215
2213
// accessible" than it actually is.
2216
- const irep_idt id = arg0 .get (ID_identifier);
2214
+ const irep_idt & id = invoke_statement .get (ID_identifier);
2217
2215
if (
2218
2216
symbol_table.symbols .find (id) == symbol_table.symbols .end () &&
2219
- !(is_virtual &&
2220
- is_method_inherited (arg0.get (ID_C_class), arg0.get (ID_component_name))))
2217
+ !(is_virtual && is_method_inherited (
2218
+ invoke_statement.get (ID_C_class),
2219
+ invoke_statement.get (ID_component_name))))
2221
2220
{
2222
2221
symbolt symbol;
2223
2222
symbol.name = id;
2224
- symbol.base_name = arg0 .get (ID_C_base_name);
2225
- symbol.pretty_name = id2string (arg0 .get (ID_C_class)).substr (6 ) + " . " +
2226
- id2string (symbol.base_name ) + " ()" ;
2227
- symbol.type = arg0 .type ();
2223
+ symbol.base_name = invoke_statement .get (ID_C_base_name);
2224
+ symbol.pretty_name = id2string (invoke_statement .get (ID_C_class)).substr (6 ) +
2225
+ " . " + id2string (symbol.base_name ) + " ()" ;
2226
+ symbol.type = invoke_statement .type ();
2228
2227
symbol.type .set (ID_access, ID_public);
2229
2228
symbol.value .make_nil ();
2230
2229
symbol.mode = ID_java;
@@ -2236,30 +2235,37 @@ void java_bytecode_convert_methodt::convert_invoke(
2236
2235
symbol_table.add (symbol);
2237
2236
}
2238
2237
2238
+ const bool is_enum_values_clone_call =
2239
+ enum_clone_symbol.type .get_bool (ID_enumeration) &&
2240
+ (full_method_name ==
2241
+ (calling_class_name + " .values:()[L" + class_type_name + " ;" ));
2242
+
2239
2243
if (is_enum_values_clone_call)
2240
2244
{
2241
- const std::string clone_name =
2242
- " java::array[" + calling_class_name + " ].clone:()Ljava/lang/Object;" ;
2243
- call.function () = symbol_exprt (clone_name, arg0 .type ());
2245
+ const irep_idt clone_name =
2246
+ " java::array[" + class_type_name + " ].clone:()Ljava/lang/Object;" ;
2247
+ call.function () = symbol_exprt (clone_name, invoke_statement .type ());
2244
2248
}
2245
2249
else if (is_virtual)
2246
2250
{
2247
2251
// dynamic binding
2248
2252
assert (use_this);
2249
2253
assert (!call.arguments ().empty ());
2250
- call.function () = arg0 ;
2254
+ call.function () = invoke_statement ;
2251
2255
// Populate needed methods later,
2252
2256
// once we know what object types can exist.
2253
2257
}
2254
2258
else
2255
2259
{
2256
2260
// static binding
2257
- call.function () = symbol_exprt (arg0.get (ID_identifier), arg0.type ());
2261
+ call.function () = symbol_exprt (
2262
+ invoke_statement.get (ID_identifier), invoke_statement.type ());
2258
2263
if (needed_lazy_methods)
2259
2264
{
2260
- needed_lazy_methods->add_needed_method (arg0.get (ID_identifier));
2265
+ needed_lazy_methods->add_needed_method (
2266
+ invoke_statement.get (ID_identifier));
2261
2267
// Calling a static method causes static initialization:
2262
- needed_lazy_methods->add_needed_class (arg0 .get (ID_C_class));
2268
+ needed_lazy_methods->add_needed_class (invoke_statement .get (ID_C_class));
2263
2269
}
2264
2270
}
2265
2271
@@ -2271,7 +2277,7 @@ void java_bytecode_convert_methodt::convert_invoke(
2271
2277
2272
2278
if (!use_this)
2273
2279
{
2274
- codet clinit_call = get_clinit_call (arg0 .get (ID_C_class));
2280
+ codet clinit_call = get_clinit_call (invoke_statement .get (ID_C_class));
2275
2281
if (clinit_call.get_statement () != ID_skip)
2276
2282
{
2277
2283
code_blockt ret_block;
0 commit comments