@@ -201,6 +201,97 @@ std::string gather_full_class_name(const std::string &src)
201
201
std::replace (class_name.begin (), class_name.end (), ' /' , ' .' );
202
202
return class_name;
203
203
}
204
+
205
+ reference_typet
206
+ build_class_name (const std::string src, const std::string &class_name_prefix)
207
+ {
208
+ PRECONDITION (src[0 ] == ' L' );
209
+ // ends on ;
210
+ if (src[src.size () - 1 ] != ' ;' )
211
+ throw " invalid string for reference type" ;
212
+
213
+ std::string container_class = gather_full_class_name (src);
214
+ std::string identifier = " java::" + container_class;
215
+ symbol_typet symbol_type (identifier);
216
+ symbol_type.set (ID_C_base_name, container_class);
217
+
218
+ // TODO(tkiley): The below code only parses the first generic argument list
219
+
220
+ std::size_t f_pos = src.find (' <' , 1 );
221
+ // get generic type information
222
+ if (f_pos != std::string::npos)
223
+ {
224
+ std::size_t e_pos = find_closing_delimiter (src, f_pos, ' <' , ' >' );
225
+ if (e_pos == std::string::npos)
226
+ throw unsupported_java_class_signature_exceptiont (" recursive generic" );
227
+
228
+ // What needs to happen is the symbol_typet needs to use all parts
229
+ // of the name and all generic parts of the child names
230
+ // For now it might be sufficient to parse the rest of the name
231
+
232
+ java_generic_typet result (symbol_type);
233
+
234
+ #ifdef DEBUG
235
+ std::cout << " INFO: found generic type "
236
+ << src.substr (f_pos + 1 , e_pos - f_pos - 1 ) << " in " << src
237
+ << " with container " << generic_container_class << " \n " ;
238
+ #endif
239
+
240
+ // parse contained types, can be either type variables, starting with T
241
+ // or instantiated types
242
+ size_t curr_start = f_pos + 1 ;
243
+ size_t curr_end;
244
+ do
245
+ {
246
+ // find next end of type name
247
+ curr_end = src.find (' ;' , curr_start);
248
+ INVARIANT (
249
+ curr_end != std::string::npos, " Type not terminated with \' ;\' " );
250
+ const size_t end = curr_end - curr_start + 1 ;
251
+ const typet &t =
252
+ java_type_from_string (src.substr (curr_start, end), class_name_prefix);
253
+ #ifdef DEBUG
254
+ std::cout << " INFO: getting type " << src.substr (curr_start, end) << " \n "
255
+ << " INFO: type id " << id2string (t.id ()) << " \n "
256
+ << " curr_start " << curr_start << " curr_end " << curr_end
257
+ << " e_pos " << e_pos << " src " << src << " \n " ;
258
+ #endif
259
+ // is an uninstantiated (pure) generic type
260
+ if (is_java_generic_parameter (t))
261
+ {
262
+ const java_generic_parametert &gen_type = to_java_generic_parameter (t);
263
+ #ifdef DEBUG
264
+ std::cout << " generic type var " << gen_type.id () << " bound "
265
+ << to_symbol_type (gen_type.subtype ()).get_identifier ()
266
+ << " \n " ;
267
+ #endif
268
+ result.generic_type_variables ().push_back (gen_type);
269
+ }
270
+
271
+ // / TODO(mgudemann): implement / test the case of iterated generic
272
+ // / types
273
+
274
+ // is a concrete type, i.e., instantiation of a generic type of the
275
+ // current type
276
+ else
277
+ {
278
+ java_generic_inst_parametert inst_type (to_symbol_type (t.subtype ()));
279
+ #ifdef DEBUG
280
+ std::cout << " instantiation of generic type var "
281
+ << to_symbol_type (t.subtype ()).get_identifier () << " \n " ;
282
+ #endif
283
+ result.generic_type_variables ().push_back (inst_type);
284
+ }
285
+
286
+ curr_start = curr_end + 1 ;
287
+ } while (curr_start < e_pos);
288
+
289
+ return result;
290
+ }
291
+
292
+ return java_reference_type (symbol_type);
293
+ }
294
+
204
295
// / Transforms a string representation of a Java type into an internal type
205
296
// / representation thereof.
206
297
// /
@@ -361,108 +452,7 @@ typet java_type_from_string(
361
452
}
362
453
case ' L' :
363
454
{
364
- // ends on ;
365
- if (src[src.size ()-1 ]!=' ;' )
366
- return nil_typet ();
367
-
368
- std::size_t f_pos=src.find (' <' , 1 );
369
- // get generic type information
370
- if (f_pos!=std::string::npos)
371
- {
372
- std::size_t e_pos=find_closing_delimiter (src, f_pos, ' <' , ' >' );
373
- if (e_pos==std::string::npos)
374
- throw unsupported_java_class_signature_exceptiont (
375
- " recursive generic" );
376
-
377
- // construct container type
378
- std::string generic_container_class=src.substr (1 , f_pos-1 );
379
-
380
- for (unsigned i=0 ; i<generic_container_class.size (); i++)
381
- {
382
- if (generic_container_class[i]==' /' )
383
- generic_container_class[i]=' .' ;
384
- }
385
-
386
- java_generic_typet result (
387
- symbol_typet (" java::" +generic_container_class));
388
-
389
- #ifdef DEBUG
390
- std::cout << " INFO: found generic type "
391
- << src.substr (f_pos+1 , e_pos-f_pos-1 )
392
- << " in " << src
393
- << " with container " << generic_container_class << " \n " ;
394
- #endif
395
-
396
- // parse contained types, can be either type variables, starting with T
397
- // or instantiated types
398
- size_t curr_start=f_pos+1 ;
399
- size_t curr_end;
400
- do
401
- {
402
- // find next end of type name
403
- curr_end=src.find (' ;' , curr_start);
404
- INVARIANT (
405
- curr_end!=std::string::npos,
406
- " Type not terminated with \' ;\' " );
407
- const size_t end=curr_end-curr_start+1 ;
408
- const typet &t=
409
- java_type_from_string (src.substr (curr_start, end),
410
- class_name_prefix);
411
- #ifdef DEBUG
412
- std::cout << " INFO: getting type "
413
- << src.substr (curr_start, end) << " \n "
414
- << " INFO: type id " << id2string (t.id ()) << " \n "
415
- << " curr_start " << curr_start
416
- << " curr_end " << curr_end
417
- << " e_pos " << e_pos
418
- << " src " << src << " \n " ;
419
- #endif
420
- // is an uninstantiated (pure) generic type
421
- if (is_java_generic_parameter (t))
422
- {
423
- const java_generic_parametert &gen_type=
424
- to_java_generic_parameter (t);
425
- #ifdef DEBUG
426
- std::cout << " generic type var " << gen_type.id () << " bound "
427
- << to_symbol_type (gen_type.subtype ()).get_identifier ()
428
- << " \n " ;
429
- #endif
430
- result.generic_type_variables ().push_back (gen_type);
431
- }
432
-
433
- // / TODO(mgudemann): implement / test the case of iterated generic
434
- // / types
435
-
436
- // is a concrete type, i.e., instantiation of a generic type of the
437
- // current type
438
- else
439
- {
440
- java_generic_inst_parametert inst_type (
441
- to_symbol_type (t.subtype ()));
442
- #ifdef DEBUG
443
- std::cout << " instantiation of generic type var "
444
- << to_symbol_type (t.subtype ()).get_identifier () << " \n " ;
445
- #endif
446
- result.generic_type_variables ().push_back (inst_type);
447
- }
448
-
449
- curr_start=curr_end+1 ;
450
- }
451
- while (curr_start<e_pos);
452
-
453
-
454
- return result;
455
- }
456
- std::string class_name=src.substr (1 , src.size ()-2 );
457
- for (auto &letter : class_name)
458
- if (letter==' /' )
459
- letter=' .' ;
460
-
461
- std::string identifier=" java::" +class_name;
462
- symbol_typet symbol_type (identifier);
463
- symbol_type.set (ID_C_base_name, class_name);
464
-
465
- return java_reference_type (symbol_type);
455
+ return build_class_name (src, class_name_prefix);
466
456
}
467
457
case ' *' :
468
458
case ' +' :
0 commit comments