@@ -175,11 +175,11 @@ exprt java_bytecode_promotion(const exprt &expr)
175
175
// / "Ljava/util/List<T>;" or "Ljava/util/List<Integer>;"
176
176
// /
177
177
// / \param src: the string representation as used in the class file
178
- // / \param class_name : name of class to append to generic type variables
178
+ // / \param class_name_prefix : name of class to append to generic type variables
179
179
// / \returns internal type representation for GOTO programs
180
180
typet java_type_from_string (
181
181
const std::string &src,
182
- const std::string &class_name )
182
+ const std::string &class_name_prefix )
183
183
{
184
184
if (src.empty ())
185
185
return nil_typet ();
@@ -210,7 +210,7 @@ typet java_type_from_string(
210
210
// (TT;TU;I)V
211
211
size_t closing_generic=find_closing_delimiter (src, 0 , ' <' , ' >' );
212
212
const typet &method_type=java_type_from_string (
213
- src.substr (closing_generic+1 , std::string::npos), class_name );
213
+ src.substr (closing_generic+1 , std::string::npos), class_name_prefix );
214
214
215
215
// This invariant being violated means that tkiley has not understood
216
216
// part of the signature spec.
@@ -233,7 +233,7 @@ typet java_type_from_string(
233
233
result.return_type ()=
234
234
java_type_from_string (
235
235
std::string (src, e_pos+1 , std::string::npos),
236
- class_name );
236
+ class_name_prefix );
237
237
238
238
for (std::size_t i=1 ; i<src.size () && src[i]!=' )' ; i++)
239
239
{
@@ -271,7 +271,7 @@ typet java_type_from_string(
271
271
}
272
272
273
273
std::string sub_str=src.substr (start, i-start+1 );
274
- param.type ()=java_type_from_string (sub_str, class_name );
274
+ param.type ()=java_type_from_string (sub_str, class_name_prefix );
275
275
276
276
if (param.type ().id ()==ID_symbol)
277
277
param.type ()=java_reference_type (param.type ());
@@ -290,7 +290,8 @@ typet java_type_from_string(
290
290
return nil_typet ();
291
291
char subtype_letter=src[1 ];
292
292
const typet subtype=
293
- java_type_from_string (src.substr (1 , std::string::npos), class_name);
293
+ java_type_from_string (src.substr (1 , std::string::npos),
294
+ class_name_prefix);
294
295
if (subtype_letter==' L' || // [L denotes a reference array of some sort.
295
296
subtype_letter==' [' || // Array-of-arrays
296
297
subtype_letter==' T' ) // Array of generic types
@@ -313,8 +314,8 @@ typet java_type_from_string(
313
314
{
314
315
// parse name of type variable
315
316
INVARIANT (src[src.size ()-1 ]==' ;' , " Generic type name must end on ';'." );
316
- PRECONDITION (!class_name .empty ());
317
- irep_idt type_var_name (class_name +" ::" +src.substr (1 , src.size ()-2 ));
317
+ PRECONDITION (!class_name_prefix .empty ());
318
+ irep_idt type_var_name (class_name_prefix +" ::" +src.substr (1 , src.size ()-2 ));
318
319
return java_generic_parametert (
319
320
type_var_name,
320
321
java_type_from_string (" Ljava/lang/Object;" ).subtype ());
@@ -324,7 +325,6 @@ typet java_type_from_string(
324
325
// ends on ;
325
326
if (src[src.size ()-1 ]!=' ;' )
326
327
return nil_typet ();
327
- std::string class_name=src.substr (1 , src.size ()-2 );
328
328
329
329
std::size_t f_pos=src.find (' <' , 1 );
330
330
// get generic type information
@@ -367,7 +367,8 @@ typet java_type_from_string(
367
367
" Type not terminated with \' ;\' " );
368
368
const size_t end=curr_end-curr_start+1 ;
369
369
const typet &t=
370
- java_type_from_string (src.substr (curr_start, end), class_name);
370
+ java_type_from_string (src.substr (curr_start, end),
371
+ class_name_prefix);
371
372
#ifdef DEBUG
372
373
std::cout << " INFO: getting type "
373
374
<< src.substr (curr_start, end) << " \n "
@@ -412,6 +413,7 @@ typet java_type_from_string(
412
413
413
414
return result;
414
415
}
416
+ std::string class_name=src.substr (1 , src.size ()-2 );
415
417
for (auto &letter : class_name)
416
418
if (letter==' /' )
417
419
letter=' .' ;
@@ -427,7 +429,7 @@ typet java_type_from_string(
427
429
case ' -' :
428
430
{
429
431
#ifdef DEBUG
430
- std::cout << class_name << std::endl;
432
+ std::cout << class_name_prefix << std::endl;
431
433
#endif
432
434
throw unsupported_java_class_siganture_exceptiont (" wild card generic" );
433
435
}
0 commit comments