Use id_usett consistently

Author: NathanJPhillips

src/analyses/dirty.h

@@ -130,7 +130,7 @@ class incremental_dirtyt
 
 private:
   dirtyt dirty;
-  std::unordered_set<irep_idt, irep_id_hash> dirty_processed_functions;
+  unordered_id_sett dirty_processed_functions;
 };
 
 #endif // CPROVER_ANALYSES_DIRTY_H

src/ansi-c/c_typecheck_type.cpp

@@ -877,7 +877,7 @@ void c_typecheck_baset::typecheck_compound_body(
   // scan for duplicate members
 
   {
-    std::unordered_set<irep_idt, irep_id_hash> members;
+    unordered_id_sett members;
 
     for(struct_union_typet::componentst::iterator
         it=components.begin();

src/ansi-c/expr2c_class.h

@@ -64,9 +64,7 @@ class expr2ct
 
   static std::string indent_str(unsigned indent);
 
-  std::unordered_map<irep_idt,
-                std::unordered_set<irep_idt, irep_id_hash>,
-                irep_id_hash> ns_collision;
+  std::unordered_map<irep_idt, unordered_id_sett, irep_id_hash> ns_collision;
   std::unordered_map<irep_idt, irep_idt, irep_id_hash> shorthands;
 
   unsigned sizeof_nesting;

src/cbmc/symex_bmc.h

@@ -147,7 +147,7 @@ class symex_bmct: public goto_symext
 
   virtual void no_body(const irep_idt &identifier);
 
-  std::unordered_set<irep_idt, irep_id_hash> body_warnings;
+  unordered_id_sett body_warnings;
 
   symex_coveraget symex_coverage;
 };

src/goto-instrument/count_eloc.cpp

@@ -21,7 +21,7 @@ Date: December 2012
 
 #include <goto-programs/cfg.h>
 
-typedef std::unordered_set<irep_idt, irep_id_hash> linest;
+typedef unordered_id_sett linest;
 typedef std::unordered_map<irep_idt, linest, irep_id_hash> filest;
 typedef std::unordered_map<irep_idt, filest, irep_id_hash> working_dirst;
 

src/goto-instrument/dump_c.cpp

@@ -613,7 +613,7 @@ void dump_ct::cleanup_decl(
 
   tmp.add_instruction(END_FUNCTION);
 
-  std::unordered_set<irep_idt, irep_id_hash> typedef_names;
+  unordered_id_sett typedef_names;
   for(const auto &td : typedef_map)
     typedef_names.insert(td.first);
 
@@ -640,7 +640,7 @@ void dump_ct::cleanup_decl(
 ///   function declarations or struct definitions
 void dump_ct::collect_typedefs(const typet &type, bool early)
 {
-  std::unordered_set<irep_idt, irep_id_hash> deps;
+  unordered_id_sett deps;
   collect_typedefs_rec(type, early, deps);
 }
 
@@ -654,12 +654,12 @@ void dump_ct::collect_typedefs(const typet &type, bool early)
 void dump_ct::collect_typedefs_rec(
   const typet &type,
   bool early,
-  std::unordered_set<irep_idt, irep_id_hash> &dependencies)
+  unordered_id_sett &dependencies)
 {
   if(system_symbols.is_type_internal(type, system_headers))
     return;
 
-  std::unordered_set<irep_idt, irep_id_hash> local_deps;
+  unordered_id_sett local_deps;
 
   if(type.id()==ID_code)
   {
@@ -986,7 +986,7 @@ void dump_ct::convert_function_declaration(
     code_blockt b;
     std::list<irep_idt> type_decls, local_static;
 
-    std::unordered_set<irep_idt, irep_id_hash> typedef_names;
+    unordered_id_sett typedef_names;
     for(const auto &td : typedef_map)
       typedef_names.insert(td.first);
 

src/goto-instrument/dump_c_class.h

@@ -52,7 +52,7 @@ class dump_ct
   std::unique_ptr<languaget> language;
   const bool harness;
 
-  typedef std::unordered_set<irep_idt, irep_id_hash> convertedt;
+  typedef unordered_id_sett convertedt;
   convertedt converted_compound, converted_global, converted_enum;
 
   std::set<std::string> system_headers;
@@ -68,7 +68,7 @@ class dump_ct
     irep_idt typedef_name;
     std::string type_decl_str;
     bool early;
-    std::unordered_set<irep_idt, irep_id_hash> dependencies;
+    unordered_id_sett dependencies;
 
     explicit typedef_infot(const irep_idt &name):
       typedef_name(name),
@@ -108,7 +108,7 @@ class dump_ct
   void collect_typedefs_rec(
     const typet &type,
     bool early,
-    std::unordered_set<irep_idt, irep_id_hash> &dependencies);
+    unordered_id_sett &dependencies);
   void gather_global_typedefs();
   void dump_typedefs(std::ostream &os) const;
 

src/goto-programs/goto_inline_class.h

@@ -193,13 +193,13 @@ class goto_inlinet:public messaget
   typedef goto_functionst::function_mapt cachet;
   cachet cache;
 
-  typedef std::unordered_set<irep_idt, irep_id_hash> finished_sett;
+  typedef unordered_id_sett finished_sett;
   finished_sett finished_set;
 
-  typedef std::unordered_set<irep_idt, irep_id_hash> recursion_sett;
+  typedef unordered_id_sett recursion_sett;
   recursion_sett recursion_set;
 
-  typedef std::unordered_set<irep_idt, irep_id_hash> no_body_sett;
+  typedef unordered_id_sett no_body_sett;
   no_body_sett no_body_set;
 };
 

src/goto-programs/lazy_goto_functions_map.h

@@ -61,7 +61,7 @@ class lazy_goto_functions_mapt final
   /// Names of functions that are already fully available in the programt state.
   /// \remarks These functions do not need processing before being returned
   /// whenever they are requested
-  mutable std::unordered_set<irep_idt, irep_id_hash> processed_functions;
+  mutable unordered_id_sett processed_functions;
 
   language_filest &language_files;
   symbol_tablet &symbol_table;

src/goto-programs/link_goto_model.cpp

@@ -47,7 +47,7 @@ static bool link_functions(
   const symbol_tablet &src_symbol_table,
   goto_functionst &src_functions,
   const rename_symbolt &rename_symbol,
-  const std::unordered_set<irep_idt, irep_id_hash> &weak_symbols,
+  const unordered_id_sett &weak_symbols,
   const replace_symbolt &object_type_updates)
 {
   namespacet ns(dest_symbol_table);

src/goto-programs/set_properties.cpp

@@ -16,7 +16,7 @@ Author: Daniel Kroening, [email protected]
 
 void set_properties(
   goto_programt &goto_program,
-  std::unordered_set<irep_idt, irep_id_hash> &property_set)
+  unordered_id_sett &property_set)
 {
   for(goto_programt::instructionst::iterator
       it=goto_program.instructions.begin();
@@ -28,8 +28,7 @@ void set_properties(
 
     irep_idt property_id=it->source_location.get_property_id();
 
-    std::unordered_set<irep_idt, irep_id_hash>::iterator
-      c_it=property_set.find(property_id);
+    unordered_id_sett::iterator c_it = property_set.find(property_id);
 
     if(c_it==property_set.end())
       it->type=SKIP;
@@ -102,7 +101,7 @@ void set_properties(
   goto_functionst &goto_functions,
   const std::list<std::string> &properties)
 {
-  std::unordered_set<irep_idt, irep_id_hash> property_set;
+  unordered_id_sett property_set;
 
   property_set.insert(properties.begin(), properties.end());
 

src/goto-symex/partial_order_concurrency.cpp

@@ -28,7 +28,7 @@ partial_order_concurrencyt::~partial_order_concurrencyt()
 void partial_order_concurrencyt::add_init_writes(
   symex_target_equationt &equation)
 {
-  std::unordered_set<irep_idt, irep_id_hash> init_done;
+  unordered_id_sett init_done;
   bool spawn_seen=false;
 
   symex_target_equationt::SSA_stepst init_steps;

src/goto-symex/postcondition.cpp

@@ -175,7 +175,7 @@ bool postconditiont::is_used(
 
     value_setst::valuest expr_set;
     value_set.get_value_set(expr.op0(), expr_set, ns);
-    std::unordered_set<irep_idt, irep_id_hash> symbols;
+    unordered_id_sett symbols;
 
     for(value_setst::valuest::const_iterator
         it=expr_set.begin();

src/goto-symex/precondition.cpp

@@ -117,7 +117,7 @@ void preconditiont::compute_rec(exprt &dest)
 
     value_setst::valuest expr_set;
     value_sets.get_values(target, dest.op0(), expr_set);
-    std::unordered_set<irep_idt, irep_id_hash> symbols;
+    unordered_id_sett symbols;
 
     for(value_setst::valuest::const_iterator
         it=expr_set.begin();

src/goto-symex/slice.h

@@ -29,7 +29,7 @@ void slice(
 
 // Collects "open" variables that are used but not assigned
 
-typedef std::unordered_set<irep_idt, irep_id_hash> symbol_sett;
+typedef unordered_id_sett symbol_sett;
 
 void collect_open_variables(
   const symex_target_equationt &equation,

src/java_bytecode/java_object_factory.cpp

@@ -67,7 +67,7 @@ class java_object_factoryt
   /// non-det generator visits a type, the type is added to this set. We forbid
   /// the non-det initialization when we see the type for the second time in
   /// this set AND the tree depth becomes >= than the maximum value above.
-  std::unordered_set<irep_idt, irep_id_hash> recursion_set;
+  unordered_id_sett recursion_set;
 
   /// Every time the non-det generator visits a type and the type is generic
   /// (either a struct or a pointer), the following map is used to store and
@@ -465,16 +465,15 @@ void java_object_factoryt::gen_pointer_target_init(
 class recursion_set_entryt
 {
   /// Recursion set to modify
-  std::unordered_set<irep_idt, irep_id_hash> &recursion_set;
+  unordered_id_sett &recursion_set;
   /// Entry to erase on destruction, if non-empty
   irep_idt erase_entry;
 
 public:
   /// Initialize a recursion-set entry owner operating on a given set.
   /// Initially it does not own any set entry.
   /// \param _recursion_set: set to operate on.
-  explicit recursion_set_entryt(
-    std::unordered_set<irep_idt, irep_id_hash> &_recursion_set)
+  explicit recursion_set_entryt(unordered_id_sett &_recursion_set)
     : recursion_set(_recursion_set)
   { }
 

src/java_bytecode/java_static_initializers.cpp

@@ -264,7 +264,7 @@ static itertype advance_to_next_key(itertype in, itertype end)
 ///   when it is required.
 void stub_global_initializer_factoryt::create_stub_global_initializer_symbols(
   symbol_tablet &symbol_table,
-  const std::unordered_set<irep_idt, irep_id_hash> &stub_globals_set,
+  const unordered_id_sett &stub_globals_set,
   synthetic_methods_mapt &synthetic_methods)
 {
   // Populate map from class id -> stub globals:

src/java_bytecode/java_static_initializers.h

@@ -38,7 +38,7 @@ class stub_global_initializer_factoryt
 public:
   void create_stub_global_initializer_symbols(
     symbol_tablet &symbol_table,
-    const std::unordered_set<irep_idt, irep_id_hash> &stub_globals_set,
+    const unordered_id_sett &stub_globals_set,
     synthetic_methods_mapt &synthetic_methods);
 
   codet get_stub_initializer_body(
@@ -50,7 +50,7 @@ class stub_global_initializer_factoryt
 
 void create_stub_global_initializers(
   symbol_tablet &symbol_table,
-  const std::unordered_set<irep_idt, irep_id_hash> &stub_globals_set,
+  const unordered_id_sett &stub_globals_set,
   const object_factory_parameterst &object_factory_parameters,
   const select_pointer_typet &pointer_type_selector);
 

src/java_bytecode/java_string_library_preprocess.cpp

@@ -1893,11 +1893,14 @@ bool java_string_library_preprocesst::is_known_string_type(
 
 void java_string_library_preprocesst::initialize_known_type_table()
 {
-  string_types=
-    std::unordered_set<irep_idt, irep_id_hash>{"java.lang.String",
-                                               "java.lang.StringBuilder",
-                                               "java.lang.CharSequence",
-                                               "java.lang.StringBuffer"};
+  string_types =
+    unordered_id_sett
+    {
+      "java.lang.String",
+      "java.lang.StringBuilder",
+      "java.lang.CharSequence",
+      "java.lang.StringBuffer"
+    };
 }
 
 /// fill maps with correspondence from java method names to conversion functions

src/java_bytecode/java_string_library_preprocess.h

@@ -141,7 +141,7 @@ class java_string_library_preprocesst:public messaget
     };
 
   // A set tells us what java types should be considered as string objects
-  std::unordered_set<irep_idt, irep_id_hash> string_types;
+  unordered_id_sett string_types;
 
   codet make_equals_function_code(
     const code_typet &type,

src/java_bytecode/java_utils.cpp

@@ -420,11 +420,11 @@ resolve_inherited_componentt::inherited_componentt get_inherited_component(
 /// \return true if this static field is known never to be null
 bool is_non_null_library_global(const irep_idt &symbolid)
 {
-  static const std::unordered_set<irep_idt, irep_id_hash> non_null_globals =
-  {
-    "java::java.lang.System.out",
-    "java::java.lang.System.err",
-    "java::java.lang.System.in"
-  };
+  static const unordered_id_sett non_null_globals =
+    {
+      "java::java.lang.System.out",
+      "java::java.lang.System.err",
+      "java::java.lang.System.in"
+    };
   return non_null_globals.count(symbolid);
 }

src/jsil/jsil_typecheck.h

@@ -94,7 +94,7 @@ class jsil_typecheckt:public typecheckt
   virtual std::string to_string(const exprt &expr);
   virtual std::string to_string(const typet &type);
 
-  std::unordered_set<irep_idt, irep_id_hash> already_typechecked;
+  unordered_id_sett already_typechecked;
 };
 
 #endif // CPROVER_JSIL_JSIL_TYPECHECK_H

src/solvers/cvc/cvc_conv.cpp

@@ -1157,7 +1157,7 @@ void cvc_convt::set_to(const exprt &expr, bool value)
 
       if(id.type.is_nil())
       {
-        std::unordered_set<irep_idt, irep_id_hash> s_set;
+        unordered_id_sett s_set;
 
         ::find_symbols(expr.op1(), s_set);
 

src/util/find_macros.h

@@ -17,7 +17,7 @@ Author: Daniel Kroening, [email protected]
 class exprt;
 class namespacet;
 
-typedef std::unordered_set<irep_idt, irep_id_hash> find_macros_sett;
+typedef unordered_id_sett find_macros_sett;
 
 void find_macros(
   const exprt &src,

src/util/find_symbols.h

@@ -19,7 +19,7 @@ class exprt;
 class symbol_exprt;
 class typet;
 
-typedef std::unordered_set<irep_idt, irep_id_hash> find_symbols_sett;
+typedef unordered_id_sett find_symbols_sett;
 
 void find_symbols(
   const exprt &src,

src/util/journalling_symbol_table.h

@@ -34,7 +34,7 @@
 class journalling_symbol_tablet : public symbol_table_baset
 {
 public:
-  typedef std::unordered_set<irep_idt, irep_id_hash> changesett;
+  typedef unordered_id_sett changesett;
 
 private:
   symbol_table_baset &base_symbol_table;