Introducing MAX_FILE_NAME_SIZE constant.

Author: marek-trtik

src/util/file_util.cpp

@@ -161,7 +161,11 @@ std::string concat_dir_file(
 /// This is not designed to operate on path names and will replace folder
 /// seperator characters.
 /// \param file_name: The file name to sanitize.
-std::string make_valid_filename(std::string file_name)
+/// \param max_size: The maximum size for the file name. If the name is longer,
+///                  then its size will be cut to the max_size.
+std::string make_valid_filename(
+  std::string file_name,
+  const std::size_t max_size)
 {
   std::replace(file_name.begin(), file_name.end(), '#', '_');
   std::replace(file_name.begin(), file_name.end(), '$', '_');
@@ -170,5 +174,7 @@ 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(), '>', ']');
+  if(file_name.size() > max_size)
+    file_name.resize(max_size);
   return file_name;
 }

src/util/file_util.h

@@ -12,13 +12,21 @@ Author: Daniel Kroening, [email protected]
 
 #include <string>
 
+/// This constant defines a maximum name length of any file created by
+/// any module of the CProver. The value of the constant was inferred
+/// from the most restrictive file system we use on our workstations:
+/// 'ecryptfs'.
+const std::size_t MAX_FILE_NAME_SIZE = 140;
+
 void delete_directory(const std::string &path);
 
 std::string get_current_working_directory();
 
 std::string concat_dir_file(const std::string &directory,
                             const std::string &file_name);
 
-std::string make_valid_filename(std::string filename);
+std::string make_valid_filename(
+  std::string filename,
+  const std::size_t max_size = MAX_FILE_NAME_SIZE);
 
 #endif // CPROVER_UTIL_FILE_UTIL_H