Skip to content

Commit dbc2f71

Browse files
Improve code and error message in infer_opaque_type_fields
1 parent 7c0ea4d commit dbc2f71

File tree

1 file changed

+14
-12
lines changed

1 file changed

+14
-12
lines changed

src/java_bytecode/java_bytecode_language.cpp

Lines changed: 14 additions & 12 deletions
Original file line numberDiff line numberDiff line change
@@ -234,13 +234,13 @@ static void infer_opaque_type_fields(
234234
instruction.statement == "putfield")
235235
{
236236
const exprt &fieldref = instruction.args[0];
237-
const symbolt *class_symbol =
238-
symbol_table.lookup(fieldref.get(ID_class));
237+
irep_idt class_symbol_id = fieldref.get(ID_class);
238+
const symbolt *class_symbol = symbol_table.lookup(class_symbol_id);
239239
INVARIANT(
240-
class_symbol != nullptr, "all field types should have been loaded");
240+
class_symbol != nullptr,
241+
"all types containing fields should have been loaded");
241242

242243
const class_typet *class_type = &to_class_type(class_symbol->type);
243-
irep_idt class_symbol_id = fieldref.get(ID_class);
244244
const irep_idt &component_name = fieldref.get(ID_component_name);
245245
while(!class_type->has_component(component_name))
246246
{
@@ -249,22 +249,24 @@ static void infer_opaque_type_fields(
249249
// Accessing a field of an incomplete (opaque) type.
250250
symbolt &writable_class_symbol =
251251
symbol_table.get_writeable_ref(class_symbol_id);
252-
auto &add_to_components =
252+
auto &components =
253253
to_struct_type(writable_class_symbol.type).components();
254-
add_to_components.push_back(
255-
struct_typet::componentt(component_name, fieldref.type()));
256-
add_to_components.back().set_base_name(component_name);
257-
add_to_components.back().set_pretty_name(component_name);
254+
components.emplace_back(component_name, fieldref.type());
255+
components.back().set_base_name(component_name);
256+
components.back().set_pretty_name(component_name);
258257
break;
259258
}
260259
else
261260
{
262261
// Not present here: check the superclass.
263262
INVARIANT(
264-
class_type->bases().size() != 0,
265-
"class missing an expected field should have a superclass");
263+
!class_type->bases().empty(),
264+
"class '" + id2string(class_symbol->name)
265+
+ "' (which was missing a field '" + id2string(component_name)
266+
+ "' referenced from method '" + id2string(method.name)
267+
+ "') should have an opaque superclass");
266268
const symbol_typet &superclass_type =
267-
to_symbol_type(class_type->bases()[0].type());
269+
to_symbol_type(class_type->bases().front().type());
268270
class_symbol_id = superclass_type.get_identifier();
269271
class_type = &to_class_type(ns.follow(superclass_type));
270272
}

0 commit comments

Comments
 (0)