From c07e6ca715a47653ec7273d05ba78daa57cd9d35 Mon Sep 17 00:00:00 2001 From: svorenova Date: Thu, 12 Apr 2018 15:54:28 +0100 Subject: [PATCH 1/3] Update generic specialization map when replacing pointers When initiliazing a pointer and it is replaced by a different pointer due to inheritence make sure that the generic parameter specialization map is updated too. --- src/java_bytecode/java_object_factory.cpp | 7 +++++++ 1 file changed, 7 insertions(+) diff --git a/src/java_bytecode/java_object_factory.cpp b/src/java_bytecode/java_object_factory.cpp index 713ffd88566..138033676b0 100644 --- a/src/java_bytecode/java_object_factory.cpp +++ b/src/java_bytecode/java_object_factory.cpp @@ -766,6 +766,13 @@ void java_object_factoryt::gen_nondet_pointer_init( // for java types, technical debt TG-2707 if(!equal_java_types(replacement_pointer_type, pointer_type)) { + // update generic_parameter_specialization_map for the new pointer + generic_parameter_specialization_map_keyst + generic_parameter_specialization_map_keys( + generic_parameter_specialization_map); + generic_parameter_specialization_map_keys.insert_pairs_for_pointer( + replacement_pointer_type, ns.follow(replacement_pointer_type.subtype())); + const symbol_exprt real_pointer_symbol = gen_nondet_subtype_pointer_init( assignments, alloc_type, replacement_pointer_type, depth); From 617d388baca3178e952b66277f0c546b22b91c73 Mon Sep 17 00:00:00 2001 From: svorenova Date: Thu, 12 Apr 2018 15:55:49 +0100 Subject: [PATCH 2/3] Utility functions for generic types These will be used in test generator to convert generic pointer types. --- src/java_bytecode/java_types.h | 13 +++++++++++++ src/util/std_types.h | 13 +++++++++++++ 2 files changed, 26 insertions(+) diff --git a/src/java_bytecode/java_types.h b/src/java_bytecode/java_types.h index e731915e64a..0e47a33a218 100644 --- a/src/java_bytecode/java_types.h +++ b/src/java_bytecode/java_types.h @@ -604,6 +604,19 @@ class java_generic_symbol_typet : public symbol_typet { return (generic_typest &)(add(ID_generic_types).get_sub()); } + + /// Check if this symbol has the given generic type. If yes, return its index + /// in the vector of generic types. + /// \param type The type we are looking for. + /// \return The index of the type in the vector of generic types. + optionalt generic_type_index(const reference_typet &type) const + { + const auto &type_pointer = + std::find(generic_types().begin(), generic_types().end(), type); + if(type_pointer != generic_types().end()) + return type_pointer - generic_types().begin(); + return {}; + } }; /// \param type: the type to check diff --git a/src/util/std_types.h b/src/util/std_types.h index f7e6189245f..22daee44476 100644 --- a/src/util/std_types.h +++ b/src/util/std_types.h @@ -407,6 +407,19 @@ class class_typet:public struct_typet return false; } + /// Return the base with the given name, if exists. + /// \param id The name of the base we are looking for. + /// \return The base if exists. + optionalt get_base(const irep_idt &id) const + { + for(const auto &b : bases()) + { + if(to_symbol_type(b.type()).get_identifier() == id) + return b; + } + return {}; + } + bool is_abstract() const { return get_bool(ID_abstract); From 506faf022d35afc411351f86b6e5121fe783d3c6 Mon Sep 17 00:00:00 2001 From: svorenova Date: Mon, 16 Apr 2018 12:09:48 +0100 Subject: [PATCH 3/3] Refactor a function for base existence Now simply calls a function for base retrieval --- src/util/std_types.h | 16 +++++----------- 1 file changed, 5 insertions(+), 11 deletions(-) diff --git a/src/util/std_types.h b/src/util/std_types.h index 22daee44476..877a8a54774 100644 --- a/src/util/std_types.h +++ b/src/util/std_types.h @@ -396,17 +396,6 @@ class class_typet:public struct_typet bases().push_back(baset(base)); } - bool has_base(const irep_idt &id) const - { - for(const auto &b : bases()) - { - if(to_symbol_type(b.type()).get(ID_identifier)==id) - return true; - } - - return false; - } - /// Return the base with the given name, if exists. /// \param id The name of the base we are looking for. /// \return The base if exists. @@ -420,6 +409,11 @@ class class_typet:public struct_typet return {}; } + bool has_base(const irep_idt &id) const + { + return get_base(id).has_value(); + } + bool is_abstract() const { return get_bool(ID_abstract);