From e1c063740692a47ed1ecd4e75b8d61686a720848 Mon Sep 17 00:00:00 2001 From: Chris Smowton Date: Fri, 27 Jan 2017 16:57:47 +0000 Subject: [PATCH] Add implied fields to classes When dealing with opaque (unelaborated) classes, this infers that a particular class or superclass must have a particular field when the source program assumes their presence (i.e. when there is an ((A*)a)->x reference and we don't yet know that a field named 'x' exists). This feeds into opaque stub generation, which can use the inferred type descriptor to create appropriate object initialisers in stub functions. --- src/java_bytecode/java_bytecode_typecheck_expr.cpp | 10 +++++++--- 1 file changed, 7 insertions(+), 3 deletions(-) diff --git a/src/java_bytecode/java_bytecode_typecheck_expr.cpp b/src/java_bytecode/java_bytecode_typecheck_expr.cpp index 941871d5cd3..5cc8b6f9f50 100644 --- a/src/java_bytecode/java_bytecode_typecheck_expr.cpp +++ b/src/java_bytecode/java_bytecode_typecheck_expr.cpp @@ -254,10 +254,14 @@ void java_bytecode_typecheckt::typecheck_expr_member(member_exprt &expr) { // member doesn't exist. In this case struct_type should be an opaque // stub, and we'll add the member to it. - components + symbolt &symbol_table_type= + symbol_table.lookup("java::"+id2string(struct_type.get_tag())); + auto &add_to_components= + to_struct_type(symbol_table_type.type).components(); + add_to_components .push_back(struct_typet::componentt(component_name, expr.type())); - components.back().set_base_name(component_name); - components.back().set_pretty_name(component_name); + add_to_components.back().set_base_name(component_name); + add_to_components.back().set_pretty_name(component_name); return; }