diff --git a/jbmc/src/java_bytecode/java_bytecode_parser.cpp b/jbmc/src/java_bytecode/java_bytecode_parser.cpp index 71307324aed..571bffd031b 100644 --- a/jbmc/src/java_bytecode/java_bytecode_parser.cpp +++ b/jbmc/src/java_bytecode/java_bytecode_parser.cpp @@ -621,8 +621,8 @@ void java_bytecode_parsert::get_class_refs_rec(const typet &src) irep_idt name=src.get(ID_C_base_name); if(has_prefix(id2string(name), "array[")) { - const typet &element_type= - static_cast(src.find(ID_C_element_type)); + const typet &element_type = + static_cast(src.find(ID_element_type)); get_class_refs_rec(element_type); } else diff --git a/jbmc/src/java_bytecode/java_object_factory.cpp b/jbmc/src/java_bytecode/java_object_factory.cpp index 565a4b59f97..22740f55d91 100644 --- a/jbmc/src/java_bytecode/java_object_factory.cpp +++ b/jbmc/src/java_bytecode/java_object_factory.cpp @@ -1253,7 +1253,7 @@ void java_object_factoryt::allocate_nondet_length_array( side_effect_exprt java_new_array(ID_java_new_array, lhs.type()); java_new_array.copy_to_operands(length_sym_expr); java_new_array.set(ID_length_upper_bound, max_length_expr); - java_new_array.type().subtype().set(ID_C_element_type, element_type); + java_new_array.type().subtype().set(ID_element_type, element_type); code_assignt assign(lhs, java_new_array); assign.add_source_location()=loc; assignments.copy_to_operands(assign); @@ -1277,8 +1277,8 @@ void java_object_factoryt::gen_nondet_array_init( const typet &type=ns.follow(expr.type().subtype()); const struct_typet &struct_type=to_struct_type(type); - const typet &element_type= - static_cast(expr.type().subtype().find(ID_C_element_type)); + const typet &element_type = + static_cast(expr.type().subtype().find(ID_element_type)); auto max_length_expr=from_integer( object_factory_parameters.max_nondet_array_length, java_int_type()); diff --git a/jbmc/src/java_bytecode/java_types.cpp b/jbmc/src/java_bytecode/java_types.cpp index ef8a36b9a4e..67e3a27e971 100644 --- a/jbmc/src/java_bytecode/java_types.cpp +++ b/jbmc/src/java_bytecode/java_types.cpp @@ -88,7 +88,7 @@ reference_typet java_lang_object_type() } /// Construct an array pointer type. It is a pointer to a symbol with identifier -/// java::array[]. Its ID_C_element_type is set to the corresponding primitive +/// java::array[]. Its ID_element_type is set to the corresponding primitive /// type, or void* for arrays of references. /// \param subtype Character indicating the type of array reference_typet java_array_type(const char subtype) @@ -119,7 +119,7 @@ reference_typet java_array_type(const char subtype) symbol_typet symbol_type("java::"+id2string(class_name)); symbol_type.set(ID_C_base_name, class_name); - symbol_type.set(ID_C_element_type, java_type_from_char(subtype)); + symbol_type.set(ID_element_type, java_type_from_char(subtype)); return java_reference_type(symbol_type); } @@ -131,7 +131,7 @@ const typet &java_array_element_type(const symbol_typet &array_symbol) DATA_INVARIANT( is_java_array_tag(array_symbol.get_identifier()), "Symbol should have array tag"); - return array_symbol.find_type(ID_C_element_type); + return array_symbol.find_type(ID_element_type); } /// Return a non-const reference to the element type of a given java array type @@ -141,7 +141,7 @@ typet &java_array_element_type(symbol_typet &array_symbol) DATA_INVARIANT( is_java_array_tag(array_symbol.get_identifier()), "Symbol should have array tag"); - return array_symbol.add_type(ID_C_element_type); + return array_symbol.add_type(ID_element_type); } /// Checks whether the given type is an array pointer type @@ -555,7 +555,7 @@ typet java_type_from_string( case '[': // array type { // If this is a reference array, we generate a plain array[reference] - // with void* members, but note the real type in ID_C_element_type. + // with void* members, but note the real type in ID_element_type. if(src.size()<=1) return nil_typet(); char subtype_letter=src[1]; @@ -567,7 +567,7 @@ typet java_type_from_string( subtype_letter=='T') // Array of generic types subtype_letter='A'; typet tmp=java_array_type(std::tolower(subtype_letter)); - tmp.subtype().set(ID_C_element_type, subtype); + tmp.subtype().set(ID_element_type, subtype); return tmp; } diff --git a/jbmc/src/java_bytecode/remove_java_new.cpp b/jbmc/src/java_bytecode/remove_java_new.cpp index d6676d678dd..e2b4bfacd5f 100644 --- a/jbmc/src/java_bytecode/remove_java_new.cpp +++ b/jbmc/src/java_bytecode/remove_java_new.cpp @@ -177,7 +177,7 @@ goto_programt::targett remove_java_newt::lower_java_new_array( struct_type.components()[2].type()); // Allocate a (struct realtype**) instead of a (void**) if possible. - const irept &given_element_type = object_type.find(ID_C_element_type); + const irept &given_element_type = object_type.find(ID_element_type); typet allocate_data_type; if(given_element_type.is_not_nil()) { @@ -272,7 +272,7 @@ goto_programt::targett remove_java_newt::lower_java_new_array( // we already know that rhs has pointer type typet sub_type = - static_cast(rhs.type().subtype().find("#element_type")); + static_cast(rhs.type().subtype().find(ID_element_type)); CHECK_RETURN(sub_type.id() == ID_pointer); sub_java_new.type() = sub_type; diff --git a/jbmc/src/java_bytecode/select_pointer_type.cpp b/jbmc/src/java_bytecode/select_pointer_type.cpp index ed657af0384..b94fdfe1f7a 100644 --- a/jbmc/src/java_bytecode/select_pointer_type.cpp +++ b/jbmc/src/java_bytecode/select_pointer_type.cpp @@ -122,7 +122,7 @@ pointer_typet select_pointer_typet::specialize_generics( visited_nodes); pointer_typet replacement_array_type = java_array_type('a'); - replacement_array_type.subtype().set(ID_C_element_type, new_array_type); + replacement_array_type.subtype().set(ID_element_type, new_array_type); return replacement_array_type; } } diff --git a/jbmc/unit/java-testing-utils/require_type.cpp b/jbmc/unit/java-testing-utils/require_type.cpp index b405cf25bd4..77d09d02bc8 100644 --- a/jbmc/unit/java-testing-utils/require_type.cpp +++ b/jbmc/unit/java-testing-utils/require_type.cpp @@ -10,6 +10,8 @@ #include #include +#include +#include /// Checks a type is a pointer type optionally with a specific subtype /// \param type: The type to check @@ -25,8 +27,8 @@ pointer_typet require_type::require_pointer( if(subtype) { - // TODO: use base_type_eq - REQUIRE(pointer.subtype() == subtype.value()); + namespacet ns{symbol_tablet{}}; + base_type_eq(pointer.subtype(), subtype.value(), ns); } return pointer; } diff --git a/src/util/irep_ids.def b/src/util/irep_ids.def index fcda57ce383..4d6118068ba 100644 --- a/src/util/irep_ids.def +++ b/src/util/irep_ids.def @@ -571,7 +571,7 @@ IREP_ID_TWO(C_spec_loop_invariant, #spec_loop_invariant) IREP_ID_TWO(C_spec_requires, #spec_requires) IREP_ID_TWO(C_spec_ensures, #spec_ensures) IREP_ID_ONE(virtual_function) -IREP_ID_TWO(C_element_type, #element_type) +IREP_ID_TWO(element_type, element_type) IREP_ID_ONE(working_directory) IREP_ID_ONE(section) IREP_ID_ONE(bswap)