Skip to content

Commit e738f98

Browse files
Improve code and error message in infer_opaque_type_fields
1 parent 73c66c0 commit e738f98

File tree

1 file changed

+14
-12
lines changed

1 file changed

+14
-12
lines changed

src/java_bytecode/java_bytecode_language.cpp

+14-12
Original file line numberDiff line numberDiff line change
@@ -229,13 +229,13 @@ static void infer_opaque_type_fields(
229229
instruction.statement == "putfield")
230230
{
231231
const exprt &fieldref = instruction.args[0];
232-
const symbolt *class_symbol =
233-
symbol_table.lookup(fieldref.get(ID_class));
232+
irep_idt class_symbol_id = fieldref.get(ID_class);
233+
const symbolt *class_symbol = symbol_table.lookup(class_symbol_id);
234234
INVARIANT(
235-
class_symbol != nullptr, "all field types should have been loaded");
235+
class_symbol != nullptr,
236+
"all types containing fields should have been loaded");
236237

237238
const class_typet *class_type = &to_class_type(class_symbol->type);
238-
irep_idt class_symbol_id = fieldref.get(ID_class);
239239
const irep_idt &component_name = fieldref.get(ID_component_name);
240240
while(!class_type->has_component(component_name))
241241
{
@@ -244,22 +244,24 @@ static void infer_opaque_type_fields(
244244
// Accessing a field of an incomplete (opaque) type.
245245
symbolt &writable_class_symbol =
246246
symbol_table.get_writeable_ref(class_symbol_id);
247-
auto &add_to_components =
247+
auto &components =
248248
to_struct_type(writable_class_symbol.type).components();
249-
add_to_components.push_back(
250-
struct_typet::componentt(component_name, fieldref.type()));
251-
add_to_components.back().set_base_name(component_name);
252-
add_to_components.back().set_pretty_name(component_name);
249+
components.emplace_back(component_name, fieldref.type());
250+
components.back().set_base_name(component_name);
251+
components.back().set_pretty_name(component_name);
253252
break;
254253
}
255254
else
256255
{
257256
// Not present here: check the superclass.
258257
INVARIANT(
259-
class_type->bases().size() != 0,
260-
"class missing an expected field should have a superclass");
258+
!class_type->bases().empty(),
259+
"class '" + id2string(class_symbol->name)
260+
+ "' (which was missing a field '" + id2string(component_name)
261+
+ "' referenced from method '" + id2string(method.name)
262+
+ "') should have an opaque superclass");
261263
const symbol_typet &superclass_type =
262-
to_symbol_type(class_type->bases()[0].type());
264+
to_symbol_type(class_type->bases().front().type());
263265
class_symbol_id = superclass_type.get_identifier();
264266
class_type = &to_class_type(ns.follow(superclass_type));
265267
}

0 commit comments

Comments
 (0)