Skip to content

Commit e5f5e8b

Browse files
author
Matthias Güdemann
committed
Use optionalt for signature
1 parent f68e817 commit e5f5e8b

6 files changed

+35
-31
lines changed

src/java_bytecode/java_bytecode_convert_class.cpp

+9-5
Original file line numberDiff line numberDiff line change
@@ -102,16 +102,18 @@ void java_bytecode_convert_classt::convert(const classt &c)
102102
}
103103

104104
java_class_typet class_type;
105-
if(c.has_signature)
105+
if(c.signature.has_value())
106106
{
107107
java_generics_class_typet generic_class_type;
108108
#ifdef DEBUG
109109
std::cout << "INFO: found generic class signature "
110-
<< c.signature
110+
<< c.signature.value()
111111
<< " in parsed class "
112112
<< c.name << "\n";
113113
#endif
114-
for(auto t : java_generic_type_from_string(id2string(c.name), c.signature))
114+
for(auto t : java_generic_type_from_string(
115+
id2string(c.name),
116+
c.signature.value()))
115117
{
116118
generic_class_type.generic_types()
117119
.push_back(to_java_generic_parameter(t));
@@ -214,9 +216,11 @@ void java_bytecode_convert_classt::convert(
214216
const fieldt &f)
215217
{
216218
typet field_type;
217-
if(f.has_signature)
219+
if(f.signature.has_value())
218220
{
219-
field_type=java_type_from_string(f.signature, id2string(class_symbol.name));
221+
field_type=java_type_from_string(
222+
f.signature.value(),
223+
id2string(class_symbol.name));
220224

221225
/// this is for a free type variable, e.g., a field of the form `T f;`
222226
if(is_java_generic_parameter(field_type))

src/java_bytecode/java_bytecode_convert_method.cpp

+11-6
Original file line numberDiff line numberDiff line change
@@ -264,14 +264,15 @@ void java_bytecode_convert_method_lazy(
264264
{
265265
symbolt method_symbol;
266266
typet member_type;
267-
if(m.has_signature)
267+
if(m.signature.has_value())
268268
{
269269
#ifdef DEBUG
270270
std::cout << "method " << m.name
271-
<< " has signature " << m.signature << "\n";
271+
<< " has signature " << m.signature.value() << "\n";
272272
#endif
273-
member_type=
274-
java_type_from_string(m.signature, id2string(class_symbol.name));
273+
member_type=java_type_from_string(
274+
m.signature.value(),
275+
id2string(class_symbol.name));
275276
}
276277
else
277278
member_type=java_type_from_string(m.descriptor);
@@ -362,8 +363,12 @@ void java_bytecode_convert_methodt::convert(
362363
// e.g. my.package.ClassName.myMethodName:(II)I::anIntParam, and then a
363364
// symbol_exprt with the parameter and its type
364365
typet t;
365-
if(v.has_signature)
366-
t=java_type_from_string(v.signature, id2string(class_symbol.name));
366+
if(v.signature.has_value())
367+
{
368+
t=java_type_from_string(
369+
v.signature.value(),
370+
id2string(class_symbol.name));
371+
}
367372
else
368373
t=java_type_from_string(v.descriptor);
369374

src/java_bytecode/java_bytecode_parse_tree.cpp

-1
Original file line numberDiff line numberDiff line change
@@ -28,7 +28,6 @@ void java_bytecode_parse_treet::classt::swap(
2828
std::swap(other.is_public, is_public);
2929
std::swap(other.is_protected, is_protected);
3030
std::swap(other.is_private, is_private);
31-
std::swap(other.has_signature, has_signature);
3231
std::swap(other.signature, signature);
3332
other.implements.swap(implements);
3433
other.fields.swap(fields);

src/java_bytecode/java_bytecode_parse_tree.h

+5-7
Original file line numberDiff line numberDiff line change
@@ -12,6 +12,7 @@ Author: Daniel Kroening, [email protected]
1212

1313
#include <set>
1414

15+
#include <util/optional.h>
1516
#include <util/std_code.h>
1617
#include <util/std_types.h>
1718

@@ -55,16 +56,15 @@ class java_bytecode_parse_treet
5556
{
5657
public:
5758
std::string descriptor;
58-
bool has_signature;
59-
std::string signature;
59+
optionalt<std::string> signature;
6060
irep_idt name;
6161
bool is_public, is_protected, is_private, is_static, is_final;
6262
annotationst annotations;
6363

6464
virtual void output(std::ostream &out) const = 0;
6565

6666
membert():
67-
has_signature(false), is_public(false), is_protected(false),
67+
is_public(false), is_protected(false),
6868
is_private(false), is_static(false), is_final(false)
6969
{
7070
}
@@ -103,8 +103,7 @@ class java_bytecode_parse_treet
103103
public:
104104
irep_idt name;
105105
std::string descriptor;
106-
bool has_signature=false;
107-
std::string signature;
106+
optionalt<std::string> signature;
108107
std::size_t index;
109108
std::size_t start_pc;
110109
std::size_t length;
@@ -178,8 +177,7 @@ class java_bytecode_parse_treet
178177

179178
typedef std::list<irep_idt> implementst;
180179
implementst implements;
181-
bool has_signature=false;
182-
std::string signature;
180+
optionalt<std::string> signature;
183181
typedef std::list<fieldt> fieldst;
184182
typedef std::list<methodt> methodst;
185183
fieldst fields;

src/java_bytecode/java_bytecode_parser.cpp

+8-10
Original file line numberDiff line numberDiff line change
@@ -337,36 +337,38 @@ void java_bytecode_parsert::get_class_refs()
337337
for(const auto &field : parse_tree.parsed_class.fields)
338338
{
339339
typet field_type;
340-
if(field.has_signature)
340+
if(field.signature.has_value())
341341
{
342342
field_type=java_type_from_string(
343-
field.signature,
343+
field.signature.value(),
344344
"java::"+id2string(parse_tree.parsed_class.name));
345345
}
346346
else
347347
field_type=java_type_from_string(field.descriptor);
348+
348349
get_class_refs_rec(field_type);
349350
}
350351

351352
for(const auto &method : parse_tree.parsed_class.methods)
352353
{
353354
typet method_type;
354-
if(method.has_signature)
355+
if(method.signature.has_value())
355356
{
356357
method_type=java_type_from_string(
357-
method.signature,
358+
method.signature.value(),
358359
"java::"+id2string(parse_tree.parsed_class.name));
359360
}
360361
else
361362
method_type=java_type_from_string(method.descriptor);
363+
362364
get_class_refs_rec(method_type);
363365
for(const auto &var : method.local_variable_table)
364366
{
365367
typet var_type;
366-
if(var.has_signature)
368+
if(var.signature.has_value())
367369
{
368370
var_type=java_type_from_string(
369-
var.signature,
371+
var.signature.value(),
370372
"java::"+id2string(parse_tree.parsed_class.name));
371373
}
372374
else
@@ -973,7 +975,6 @@ void java_bytecode_parsert::rmethod_attribute(methodt &method)
973975
else if(attribute_name=="Signature")
974976
{
975977
u2 signature_index=read_u2();
976-
method.has_signature=true;
977978
method.signature=id2string(pool_entry(signature_index).s);
978979
}
979980
else if(attribute_name=="RuntimeInvisibleAnnotations" ||
@@ -995,7 +996,6 @@ void java_bytecode_parsert::rfield_attribute(fieldt &field)
995996
if(attribute_name=="Signature")
996997
{
997998
u2 signature_index=read_u2();
998-
field.has_signature=true;
999999
field.signature=id2string(pool_entry(signature_index).s);
10001000
}
10011001
else if(attribute_name=="RuntimeInvisibleAnnotations" ||
@@ -1352,7 +1352,6 @@ void java_bytecode_parsert::rclass_attribute(classt &parsed_class)
13521352
else if(attribute_name=="Signature")
13531353
{
13541354
u2 signature_index=read_u2();
1355-
parsed_class.has_signature=true;
13561355
parsed_class.signature=id2string(pool_entry(signature_index).s);
13571356
}
13581357
else if(attribute_name=="RuntimeInvisibleAnnotations" ||
@@ -1480,7 +1479,6 @@ void java_bytecode_parsert::parse_local_variable_type_table(methodt &method)
14801479
{
14811480
found=true;
14821481
lvar.signature=id2string(pool_entry(signature_index).s);
1483-
lvar.has_signature=true;
14841482
break;
14851483
}
14861484
}

src/java_bytecode/java_local_variable_table.cpp

+2-2
Original file line numberDiff line numberDiff line change
@@ -769,8 +769,8 @@ void java_bytecode_convert_methodt::setup_local_variables(
769769
<< v.var.descriptor << "' holes " << v.holes.size() << eom;
770770
#endif
771771
typet t;
772-
if(v.var.has_signature)
773-
t=java_type_from_string(v.var.signature);
772+
if(v.var.signature.has_value())
773+
t=java_type_from_string(v.var.signature.value());
774774
else
775775
t=java_type_from_string(v.var.descriptor);
776776

0 commit comments

Comments
 (0)