@@ -120,13 +120,9 @@ static bool operator==(const irep_idt &what, const patternt &pattern)
120
120
return pattern==what;
121
121
}
122
122
123
- // name contains <init> or <clinit>
124
- bool java_bytecode_convert_methodt::is_constructor (
125
- const class_typet::methodt &method)
123
+ static bool is_constructor (const irep_idt &method_name)
126
124
{
127
- const std::string &name (id2string (method.get_name ()));
128
- const std::string::size_type &npos (std::string::npos);
129
- return npos!=name.find (" <init>" ) || npos!=name.find (" <clinit>" );
125
+ return id2string (method_name).find (" <init>" ) != std::string::npos;
130
126
}
131
127
132
128
exprt::operandst java_bytecode_convert_methodt::pop (std::size_t n)
@@ -256,11 +252,12 @@ const exprt java_bytecode_convert_methodt::variable(
256
252
// / message handler to collect warnings
257
253
// / \return
258
254
// / the constructed member type
259
- typet member_type_lazy (const std::string &descriptor,
260
- const optionalt<std::string> &signature,
261
- const std::string &class_name,
262
- const std::string &method_name,
263
- message_handlert &message_handler)
255
+ code_typet member_type_lazy (
256
+ const std::string &descriptor,
257
+ const optionalt<std::string> &signature,
258
+ const std::string &class_name,
259
+ const std::string &method_name,
260
+ message_handlert &message_handler)
264
261
{
265
262
// In order to construct the method type, we can either use signature or
266
263
// descriptor. Since only signature contains the generics info, we want to
@@ -285,7 +282,7 @@ typet member_type_lazy(const std::string &descriptor,
285
282
if (to_code_type (member_type_from_signature).parameters ().size ()==
286
283
to_code_type (member_type_from_descriptor).parameters ().size ())
287
284
{
288
- return member_type_from_signature;
285
+ return to_code_type ( member_type_from_signature) ;
289
286
}
290
287
else
291
288
{
@@ -303,7 +300,7 @@ typet member_type_lazy(const std::string &descriptor,
303
300
<< descriptor << message.eom ;
304
301
}
305
302
}
306
- return member_type_from_descriptor;
303
+ return to_code_type ( member_type_from_descriptor) ;
307
304
}
308
305
309
306
// / This creates a method symbol in the symtab, but doesn't actually perform
@@ -324,7 +321,7 @@ void java_bytecode_convert_method_lazy(
324
321
{
325
322
symbolt method_symbol;
326
323
327
- typet member_type= member_type_lazy (
324
+ code_typet member_type = member_type_lazy (
328
325
m.descriptor ,
329
326
m.signature ,
330
327
id2string (class_symbol.name ),
@@ -337,20 +334,20 @@ void java_bytecode_convert_method_lazy(
337
334
method_symbol.location =m.source_location ;
338
335
method_symbol.location .set_function (method_identifier);
339
336
if (m.is_public )
340
- member_type.set (ID_access, ID_public);
337
+ member_type.set_access ( ID_public);
341
338
else if (m.is_protected )
342
- member_type.set (ID_access, ID_protected);
339
+ member_type.set_access ( ID_protected);
343
340
else if (m.is_private )
344
- member_type.set (ID_access, ID_private);
341
+ member_type.set_access ( ID_private);
345
342
else
346
- member_type.set (ID_access, ID_default);
343
+ member_type.set_access ( ID_default);
347
344
348
- if (method_symbol.base_name == " <init> " )
345
+ if (is_constructor ( method_symbol.base_name ) )
349
346
{
350
347
method_symbol.pretty_name =
351
348
id2string (class_symbol.pretty_name )+" ." +
352
349
id2string (class_symbol.base_name )+" ()" ;
353
- member_type.set (ID_constructor, true );
350
+ member_type.set_is_constructor ( );
354
351
}
355
352
else
356
353
method_symbol.pretty_name =
@@ -360,8 +357,7 @@ void java_bytecode_convert_method_lazy(
360
357
// do we need to add 'this' as a parameter?
361
358
if (!m.is_static )
362
359
{
363
- code_typet &code_type=to_code_type (member_type);
364
- code_typet::parameterst ¶meters=code_type.parameters ();
360
+ code_typet::parameterst ¶meters = member_type.parameters ();
365
361
code_typet::parametert this_p;
366
362
const reference_typet object_ref_type=
367
363
java_reference_type (symbol_typet (class_symbol.name ));
@@ -390,9 +386,8 @@ void java_bytecode_convert_methodt::convert(
390
386
391
387
// Obtain a std::vector of code_typet::parametert objects from the
392
388
// (function) type of the symbol
393
- typet member_type=method_symbol.type ;
394
- member_type.set (ID_C_class, class_symbol.name );
395
- code_typet &code_type=to_code_type (member_type);
389
+ code_typet code_type = to_code_type (method_symbol.type );
390
+ code_type.set (ID_C_class, class_symbol.name );
396
391
method_return_type=code_type.return_type ();
397
392
code_typet::parameterst ¶meters=code_type.parameters ();
398
393
@@ -519,25 +514,12 @@ void java_bytecode_convert_methodt::convert(
519
514
param_index==slots_for_parameters,
520
515
" java_parameter_count and local computation must agree" );
521
516
522
- const bool is_virtual=!m.is_static && !m.is_final ;
523
-
524
- // Construct a methodt, which lives within the class type; this object is
525
- // never used for anything useful and could be removed
526
- class_typet::methodt method;
527
- method.set_base_name (m.base_name );
528
- method.set_name (method_identifier);
529
- method.set (ID_abstract, m.is_abstract );
530
- method.set (ID_is_virtual, is_virtual);
531
- method.type ()=member_type;
532
- if (is_constructor (method))
533
- method.set (ID_constructor, true );
534
-
535
517
// Check the fields that can't change are valid
536
518
INVARIANT (
537
- method_symbol.name ==method. get_name () ,
519
+ method_symbol.name == method_identifier ,
538
520
" Name of method symbol shouldn't change" );
539
521
INVARIANT (
540
- method_symbol.base_name ==method. get_base_name () ,
522
+ method_symbol.base_name == m. base_name ,
541
523
" Base name of method symbol shouldn't change" );
542
524
INVARIANT (
543
525
method_symbol.module .empty (),
@@ -551,16 +533,21 @@ void java_bytecode_convert_methodt::convert(
551
533
// The pretty name of a constructor includes the base name of the class
552
534
// instead of the internal method name "<init>". For regular methods, it's
553
535
// just the base name of the method.
554
- if (method.get_base_name ()==" <init>" )
555
- method_symbol.pretty_name =id2string (class_symbol.pretty_name )+" ." +
556
- id2string (class_symbol.base_name )+" ()" ;
536
+ if (is_constructor (method_symbol.base_name ))
537
+ {
538
+ method_symbol.pretty_name = id2string (class_symbol.pretty_name ) + " ." +
539
+ id2string (class_symbol.base_name ) + " ()" ;
540
+ INVARIANT (
541
+ code_type.get_is_constructor (),
542
+ " Member type should have already been marked as a constructor" );
543
+ }
557
544
else
558
- method_symbol.pretty_name =id2string (class_symbol.pretty_name )+" ." +
559
- id2string (method.get_base_name ())+" ()" ;
545
+ {
546
+ method_symbol.pretty_name = id2string (class_symbol.pretty_name ) + " ." +
547
+ id2string (method_symbol.base_name ) + " ()" ;
548
+ }
560
549
561
- method_symbol.type =member_type;
562
- if (is_constructor (method))
563
- method_symbol.type .set (ID_constructor, true );
550
+ method_symbol.type = code_type;
564
551
565
552
current_method=method_symbol.name ;
566
553
method_has_this=code_type.has_this ();
@@ -1280,13 +1267,11 @@ codet java_bytecode_convert_methodt::convert_instructions(
1280
1267
// constructors.
1281
1268
if (statement==" invokespecial" )
1282
1269
{
1283
- if (
1284
- id2string (arg0.get (ID_identifier)).find (" <init>" ) !=
1285
- std::string::npos)
1270
+ if (is_constructor (arg0.get (ID_identifier)))
1286
1271
{
1287
1272
if (needed_lazy_methods)
1288
1273
needed_lazy_methods->add_needed_class (classname);
1289
- code_type.set (ID_constructor, true );
1274
+ code_type.set_is_constructor ( );
1290
1275
}
1291
1276
else
1292
1277
code_type.set (ID_java_super_method_call, true );
0 commit comments