Added serialization of irept and dstringt

src/config.inc

@@ -9,7 +9,7 @@ BUILD_ENV = AUTO
 
 # Select optimisation or debug info
 #CXXFLAGS += -O2 -DNDEBUG
-#CXXFLAGS += -O0 -g
+CXXFLAGS += -O0 -g
 
 ifeq ($(shell uname),Linux)
   CXXFLAGS += -DUSE_BOOST

src/util/dstring.cpp

@@ -7,3 +7,33 @@ Author: Daniel Kroening, [email protected]
 \*******************************************************************/
 
 #include "dstring.h"
+#include "serializer.h"
+
+
+/*******************************************************************\
+
+  Function: dstring::serialize
+
+  Inputs:
+    serializer: The serializer to read from/write to
+
+  Outputs:
+
+  Purpose:
+    Serializes this instance to/from the given serializer.
+
+\*******************************************************************/
+void dstringt::serialize(serializert &serializer)
+{
+  if(serializer.is_for_reading())
+  {
+    std::string str;
+    serializer.serialize("dstring", str);
+    no=string_container[str];
+  }
+  else
+  {
+    std::string str=as_string();
+    serializer.serialize("dstring", str);
+  }
+}

src/util/dstring.h

@@ -13,6 +13,9 @@ Author: Daniel Kroening, [email protected]
 
 #include "string_container.h"
 
+class serializert;
+
+
 class dstringt
 {
 public:
@@ -123,6 +126,8 @@ class dstringt
     return out << as_string();
   }
 
+  void serialize(serializert &serializer);
+
   // non-standard
 
   unsigned get_no() const

src/util/file_util.cpp

@@ -371,3 +371,31 @@ std::string fileutl_get_relative_path(
   std::string const result = fileutl_join_path_parts(split1);
   return result;
 }
+
+/*******************************************************************\
+
+  Function: make_valid_filename
+
+  Inputs:
+    file_name: The file name to sanitize.
+
+  Outputs:
+
+  Purpose:
+    Replaces invalid characters in a file name using a hard-coded list of
+    replacements.
+    This is not designed to operate on path names and will replace folder
+    seperator characters.
+
+\*******************************************************************/
+std::string make_valid_filename(std::string file_name)
+{
+  std::replace(file_name.begin(), file_name.end(), '#', '_');
+  std::replace(file_name.begin(), file_name.end(), '$', '_');
+  std::replace(file_name.begin(), file_name.end(), ':', '.');
+  std::replace(file_name.begin(), file_name.end(), '/', '.');
+  std::replace(file_name.begin(), file_name.end(), '\\', '.');
+  std::replace(file_name.begin(), file_name.end(), '<', '[');
+  std::replace(file_name.begin(), file_name.end(), '>', ']');
+  return file_name;
+}

src/util/file_util.h

@@ -62,4 +62,6 @@ std::string fileutl_get_relative_path(
   std::string const &pathname,
   std::string const &directory);
 
+std::string make_valid_filename(std::string filename);
+
 #endif // CPROVER_UTIL_FILE_UTIL_H

src/util/irep.cpp

@@ -12,6 +12,7 @@ Author: Daniel Kroening, [email protected]
 #include "string2int.h"
 #include "irep.h"
 #include "string_hash.h"
+#include "serializer.h"
 #include "irep_hash.h"
 
 #ifdef SUB_IS_LIST
@@ -1003,3 +1004,24 @@ std::string irept::pretty(unsigned indent, unsigned max_indent) const
 
   return result;
 }
+
+/*******************************************************************\
+
+  Function: irept::serialize
+
+  Inputs:
+    serializer: The serializer to read from/write to
+
+  Outputs:
+
+  Purpose:
+    Serializes this instance to/from the given serializer.
+
+\*******************************************************************/
+void irept::serialize(serializert &serializer)
+{
+  serializer.serialize("id", write().data);
+  serializer.serialize("subs", get_sub());
+  serializer.serialize("named_subs", get_named_sub());
+  serializer.serialize("comments", get_comments());
+}

src/util/irep.h

@@ -45,6 +45,9 @@ typedef std::string irep_namet;
 typedef string_hash irep_id_hash;
 #endif
 
+class serializert;
+
+
 inline const std::string &id2string(const irep_idt &d)
 {
   #ifdef USE_DSTRING
@@ -257,6 +260,8 @@ class irept
 
   std::string pretty(unsigned indent=0, unsigned max_indent=0) const;
 
+  void serialize(serializert &serializer);
+
 protected:
   static bool is_comment(const irep_namet &name)
   { return !name.empty() && name[0]=='#'; }