Change return value of get_children_trans to set

The disjuncts created by instanceof removal depended
on the class loading order, causing goto-diff to think that
there was a change in the classes.

Author: peterschrammel

src/analyses/uncaught_exceptions_analysis.cpp

@@ -77,7 +77,7 @@ void uncaught_exceptions_domaint::transform(
       join(type_id);
       // we must consider all the subtypes given that
       // the runtime type is a subtype of the static type
-      std::vector<irep_idt> subtypes=
+      class_hierarchyt::idst subtypes =
         class_hierarchy.get_children_trans(type_id);
       join(subtypes);
     }
@@ -98,7 +98,7 @@ void uncaught_exceptions_domaint::transform(
         for(const auto &exc : exception_list)
         {
           last_caught.insert(exc.id());
-          std::vector<irep_idt> subtypes=
+          class_hierarchyt::idst subtypes =
             class_hierarchy.get_children_trans(exc.id());
           last_caught.insert(subtypes.begin(), subtypes.end());
         }

src/goto-programs/class_hierarchy.cpp

@@ -39,8 +39,8 @@ void class_hierarchyt::operator()(const symbol_tablet &symbol_table)
         if(parent.empty())
           continue;
 
-        class_map[parent].children.push_back(symbol_pair.first);
-        class_map[symbol_pair.first].parents.push_back(parent);
+        class_map[parent].children.insert(symbol_pair.first);
+        class_map[symbol_pair.first].parents.insert(parent);
       }
     }
   }
@@ -94,7 +94,7 @@ void class_hierarchyt::get_children_trans_rec(
   const entryt &entry=it->second;
 
   for(const auto &child : entry.children)
-    dest.push_back(child);
+    dest.insert(child);
 
   // recursive calls
   for(const auto &child : entry.children)
@@ -116,7 +116,7 @@ void class_hierarchyt::get_parents_trans_rec(
   const entryt &entry=it->second;
 
   for(const auto &child : entry.parents)
-    dest.push_back(child);
+    dest.insert(child);
 
   // recursive calls
   for(const auto &child : entry.parents)

src/goto-programs/class_hierarchy.h

@@ -16,6 +16,7 @@ Date: April 2016
 
 #include <iosfwd>
 #include <map>
+#include <set>
 #include <unordered_map>
 
 #include <util/graph.h>
@@ -24,7 +25,7 @@ Date: April 2016
 class class_hierarchyt
 {
 public:
-  typedef std::vector<irep_idt> idst;
+  typedef std::set<irep_idt> idst;
 
   class entryt
   {

src/goto-programs/remove_instanceof.cpp

@@ -84,9 +84,9 @@ std::size_t remove_instanceoft::lower_instanceof(
     "instanceof second operand should have a simple type");
   const irep_idt &target_name=
     to_symbol_type(target_type).get_identifier();
-  std::vector<irep_idt> children=
+  class_hierarchyt::idst children =
     class_hierarchy.get_children_trans(target_name);
-  children.push_back(target_name);
+  children.insert(target_name);
 
   // Insert an instruction before the new check that assigns the clsid we're
   // checking for to a temporary, as GOTO program if-expressions should

src/goto-programs/resolve_inherited_component.cpp

@@ -78,7 +78,7 @@ resolve_inherited_componentt::inherited_componentt
     else
     {
       if(!parents.empty())
-        classes_to_visit.push_back(parents.front());
+        classes_to_visit.push_back(*parents.begin());
     }
   }
 

unit/java_bytecode/java_bytecode_convert_method/convert_invoke_dynamic.cpp

@@ -92,20 +92,12 @@ void validate_lambda_assignment(
   class_hierarchy(symbol_table);
 
   const auto &parents = class_hierarchy.get_parents_trans(tmp_class_identifier);
-  REQUIRE_THAT(
-    parents,
-    // NOLINTNEXTLINE(whitespace/braces)
-    Catch::Matchers::Vector::ContainsElementMatcher<irep_idt>{
-      test_data.lambda_interface});
+  REQUIRE(parents.count(test_data.lambda_interface) > 0);
 
   const auto &interface_children =
     class_hierarchy.get_children_trans(test_data.lambda_interface);
 
-  REQUIRE_THAT(
-    interface_children,
-    // NOLINTNEXTLINE(whitespace/braces)
-    Catch::Matchers::Vector::ContainsElementMatcher<irep_idt>{
-      tmp_class_identifier});
+  REQUIRE(interface_children.count(tmp_class_identifier) > 0);
 
   const java_class_typet::componentt super_class_component =
     require_type::require_component(tmp_lambda_class_type, "@java.lang.Object");