Enable goto_modelt move assignment

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

@@ -66,18 +66,29 @@ class goto_function_templatet
     parameter_identifiers.swap(other.parameter_identifiers);
   }
 
-  void copy_from(const goto_function_templatet<bodyT> &other)
+  void copy_from(const goto_function_templatet &other)
   {
     body.copy_from(other.body);
     type=other.type;
     parameter_identifiers=other.parameter_identifiers;
   }
 
-  goto_function_templatet(const goto_function_templatet<bodyT> &src):
-    type(src.type),
-    parameter_identifiers(src.parameter_identifiers)
+  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)),
+    type(std::move(other.type)),
+    parameter_identifiers(std::move(other.parameter_identifiers))
+  {
+  }
+
+  goto_function_templatet &operator=(goto_function_templatet &&other)
   {
-    body.copy_from(src.body);
+    body=std::move(other.body);
+    type=std::move(other.type);
+    parameter_identifiers=std::move(other.parameter_identifiers);
+    return *this;
   }
 };
 
@@ -93,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()

src/goto-programs/goto_model.h

@@ -38,14 +38,28 @@ class goto_modelt
   {
   }
 
-  goto_modelt(goto_modelt &&other)
+  // Copying is normally too expensive
+  goto_modelt(const goto_modelt &)=delete;
+  goto_modelt &operator=(const goto_modelt &)=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_modelt(goto_modelt &&other):
+    symbol_table(std::move(other.symbol_table)),
+    goto_functions(std::move(other.goto_functions))
   {
-    symbol_table.swap(other.symbol_table);
-    goto_functions.swap(other.goto_functions);
   }
 
-  // copying is likely too expensive
-  goto_modelt(const goto_modelt &) = delete;
+  goto_modelt &operator=(goto_modelt &&other)
+  {
+    symbol_table=std::move(other.symbol_table);
+    goto_functions=std::move(other.goto_functions);
+    return *this;
+  }
 };
 
 #endif // CPROVER_GOTO_PROGRAMS_GOTO_MODEL_H

src/goto-programs/goto_program.h

@@ -15,7 +15,7 @@ Author: Daniel Kroening, [email protected]
 
 #include "goto_program_template.h"
 
-/*! \brief A specialization of goto_program_templatet do
+/*! \brief A specialization of goto_program_templatet over
            goto programs in which instructions have codet type.
     \ingroup gr_goto_programs
 */
@@ -36,6 +36,28 @@ class goto_programt:public goto_program_templatet<codet, exprt>
 
   goto_programt() { }
 
+  // Copying is unavailable as base class copy is deleted
+  // MSVC is unable to automatically determine this
+  goto_programt(const goto_programt &)=delete;
+  goto_programt &operator=(const goto_programt &)=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_programt(goto_programt &&other):
+    goto_program_templatet(std::move(other))
+  {
+  }
+
+  goto_programt &operator=(goto_programt &&other)
+  {
+    goto_program_templatet::operator=(std::move(other));
+    return *this;
+  }
+
   // get the variables in decl statements
   typedef std::set<irep_idt> decl_identifierst;
   void get_decl_identifiers(decl_identifierst &decl_identifiers) const;

src/goto-programs/goto_program_template.h

@@ -56,17 +56,26 @@ template <class codeT, class guardT>
 class goto_program_templatet
 {
 public:
-  /*! \brief copy constructor
-      \param[in] src an empty goto program
-      \remark Use copy_from to copy non-empty goto-programs
-  */
-  goto_program_templatet(const goto_program_templatet &src)=delete;
+  // Copying is deleted as this class contains pointers that cannot be copied
+  goto_program_templatet(const goto_program_templatet &)=delete;
+  goto_program_templatet &operator=(const goto_program_templatet &)=delete;
 
-  /*! \brief assignment operator
-      \param[in] src an empty goto program
-      \remark Use copy_from to copy non-empty goto-programs
-  */
-  goto_program_templatet &operator=(const goto_program_templatet &src)=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_program_templatet(goto_program_templatet &&other):
+    instructions(std::move(other.instructions))
+  {
+  }
+
+  goto_program_templatet &operator=(goto_program_templatet &&other)
+  {
+    instructions=std::move(other.instructions);
+    return *this;
+  }
 
   /*! \brief Container for an instruction of the goto-program
   */