Skip to content

Commit c4ae7de

Browse files
committed
String library preprocessor: use tag types, not expanded structs
Without these we get assignments whose types match according to base_type_eq, but not operator==.
1 parent e3ff246 commit c4ae7de

File tree

1 file changed

+5
-6
lines changed

1 file changed

+5
-6
lines changed

jbmc/src/java_bytecode/java_string_library_preprocess.cpp

Lines changed: 5 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -775,11 +775,11 @@ codet java_string_library_preprocesst::code_assign_components_to_java_string(
775775
if(is_constructor)
776776
{
777777
// A String has a field Object with @clsid = String
778-
const symbolt &jlo_symbol = *symbol_table.lookup("java::java.lang.Object");
779-
const struct_typet &jlo_struct = to_struct_type(jlo_symbol.type);
780-
struct_exprt jlo_init({}, jlo_struct);
778+
struct_tag_typet jlo_tag("java::java.lang.Object");
779+
struct_exprt jlo_init({}, jlo_tag);
781780
irep_idt clsid = get_tag(lhs.type().subtype());
782-
java_root_class_init(jlo_init, jlo_struct, clsid);
781+
namespacet ns(symbol_table);
782+
java_root_class_init(jlo_init, ns.follow_tag(jlo_tag), clsid);
783783

784784
struct_exprt struct_rhs({jlo_init, rhs_length, rhs_array}, deref.type());
785785
return code_assignt(
@@ -1455,8 +1455,7 @@ code_blockt java_string_library_preprocesst::make_object_get_class_code(
14551455
code_blockt code;
14561456

14571457
// > Class class1;
1458-
const pointer_typet class_type =
1459-
java_reference_type(symbol_table.lookup_ref("java::java.lang.Class").type);
1458+
const pointer_typet &class_type = to_pointer_type(type.return_type());
14601459
const symbolt &class1_sym = fresh_java_symbol(
14611460
class_type, "class_symbol", loc, function_id, symbol_table);
14621461
const symbol_exprt class1 = class1_sym.symbol_expr();

0 commit comments

Comments
 (0)