CONTRACTS: return set by value

Author: Remi Delmas

src/goto-instrument/contracts/dynamic-frames/dfcc_library.cpp

@@ -209,9 +209,9 @@ dfcc_libraryt::get_havoc_hook(const irep_idt &function_id) const
     return {};
 }
 
-void dfcc_libraryt::get_missing_funs(std::set<irep_idt> &missing)
+std::set<irep_idt> dfcc_libraryt::get_missing_funs()
 {
-  missing.clear();
+  std::set<irep_idt> missing;
 
   // add `malloc` since it is needed used by the `is_fresh` function
   missing.insert("malloc");
@@ -243,6 +243,7 @@ void dfcc_libraryt::get_missing_funs(std::set<irep_idt> &missing)
       missing.insert(pair.second);
     }
   }
+  return missing;
 }
 
 bool dfcc_libraryt::loaded = false;
@@ -283,8 +284,7 @@ void dfcc_libraryt::load(std::set<irep_idt> &to_instrument)
     to_load, tmp_symbol_table, message_handler);
 
   // compute missing library functions before modifying the symbol table
-  std::set<irep_idt> missing;
-  get_missing_funs(missing);
+  std::set<irep_idt> missing = get_missing_funs();
 
   // copy all loaded symbols to the main symbol table
   for(const auto &symbol_pair : tmp_symbol_table.symbols)

src/goto-instrument/contracts/dynamic-frames/dfcc_library.h

@@ -173,7 +173,7 @@ class dfcc_libraryt
 
   /// Collects the names of all library functions currently missing from the
   /// goto_model into `missing`.
-  void get_missing_funs(std::set<irep_idt> &missing);
+  std::set<irep_idt> get_missing_funs();
 
   /// Inlines library functions that need to be inlined before use
   void inline_functions();