Removed copy constructor from goto_function_templatet

Rather than telling people not to use the copy constructor, actually don't use it

Author: NathanJPhillips

src/goto-instrument/wmm/goto2graph.cpp

@@ -1532,13 +1532,12 @@ bool instrumentert::is_cfg_spurious(const event_grapht::critical_cyclet &cyc)
     }
 
   /* now test whether this part of the code can exist */
+  goto_functionst::function_mapt map;
   goto_function_templatet<goto_programt> one_interleaving;
   one_interleaving.body.copy_from(interleaving);
-
-  std::pair<irep_idt, goto_function_templatet<goto_programt> > p(
-    goto_functionst::entry_point(), one_interleaving);
-  goto_functionst::function_mapt map;
-  map.insert(p);
+  map.insert(std::make_pair(
+    goto_functionst::entry_point(),
+    std::move(one_interleaving)));
 
   goto_functionst this_interleaving;
   this_interleaving.function_map=std::move(map);

src/goto-programs/goto_functions.h

@@ -17,6 +17,29 @@ Date: June 2003
 class goto_functionst:public goto_functions_templatet<goto_programt>
 {
 public:
+  goto_functionst()=default;
+
+  // Copying is unavailable as base class copy is deleted
+  // MSVC is unable to automatically determine this
+  goto_functionst(const goto_functionst &)=delete;
+  goto_functionst &operator=(const goto_functionst &)=delete;
+
+  // Move operations need to be explicitly enabled as they are deleted with the
+  // copy operations
+  // default for move operations isn't available on Windows yet, so define
+  //  explicitly (see https://msdn.microsoft.com/en-us/library/hh567368.aspx
+  //  under "Defaulted and Deleted Functions")
+
+  goto_functionst(goto_functionst &&other):
+    goto_functions_templatet(std::move(other))
+  {
+  }
+
+  goto_functionst &operator=(goto_functionst &&other)
+  {
+    goto_functions_templatet::operator=(std::move(other));
+    return *this;
+  }
 };
 
 #define Forall_goto_functions(it, functions) \

src/goto-programs/goto_functions_template.h

@@ -73,12 +73,8 @@ class goto_function_templatet
     parameter_identifiers=other.parameter_identifiers;
   }
 
-  goto_function_templatet(const goto_function_templatet &other)
-    : type(other.type),
-      parameter_identifiers(other.parameter_identifiers)
-  {
-    body.copy_from(other.body);
-  }
+  goto_function_templatet(const goto_function_templatet &)=delete;
+  goto_function_templatet &operator=(const goto_function_templatet &)=delete;
 
   goto_function_templatet(goto_function_templatet &&other):
     body(std::move(other.body)),
@@ -108,10 +104,18 @@ class goto_functions_templatet
   {
   }
 
-  // copy constructor, don't use me!
-  goto_functions_templatet(const goto_functions_templatet<bodyT> &src)
+  goto_functions_templatet(const goto_functions_templatet &)=delete;
+  goto_functions_templatet &operator=(const goto_functions_templatet &)=delete;
+
+  goto_functions_templatet(goto_functions_templatet &&other):
+    function_map(std::move(other.function_map))
+  {
+  }
+
+  goto_functions_templatet &operator=(goto_functions_templatet &&other)
   {
-    assert(src.function_map.empty());
+    function_map=std::move(other.function_map);
+    return *this;
   }
 
   void clear()