Updates requsted in the PR: mostly rename 'size -> length'.

Author: marek-trtik

cbmc/src/util/file_util.cpp

@@ -161,11 +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.
-/// \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.
+/// \param max_length: The maximum length for the file name. If the name is
+///                    longer, then its length will be cut to the max_length.
 std::string make_valid_filename(
   std::string file_name,
-  const std::size_t max_size)
+  const std::size_t max_length)
 {
   std::replace(file_name.begin(), file_name.end(), '#', '_');
   std::replace(file_name.begin(), file_name.end(), '$', '_');
@@ -174,7 +174,7 @@ std::string make_valid_filename(
   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);
+  if(file_name.size() > max_length)
+    file_name.resize(max_length);
   return file_name;
 }

cbmc/src/util/file_util.h

@@ -12,11 +12,11 @@ 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
+/// This constant defines the maximum name length of any file created by
+/// any module of the CProver. The value of the constant was derived
 /// from the most restrictive file system we use on our workstations:
 /// 'ecryptfs'.
-const std::size_t MAX_FILE_NAME_SIZE = 140;
+const std::size_t MAX_FILE_NAME_LENGTH = 140;
 
 void delete_directory(const std::string &path);
 
@@ -27,6 +27,6 @@ std::string concat_dir_file(const std::string &directory,
 
 std::string make_valid_filename(
   std::string filename,
-  const std::size_t max_size = MAX_FILE_NAME_SIZE);
+  const std::size_t max_length = MAX_FILE_NAME_LENGTH);
 
 #endif // CPROVER_UTIL_FILE_UTIL_H

src/util/json_map_serializer.h

@@ -255,9 +255,9 @@ class json_map_serializert:public virtual_map_iterated_by_keyt<keyt, valuet>
     else
     {
       const std::size_t max_size =
-        MAX_FILE_NAME_SIZE // The general size limit.
+        MAX_FILE_NAME_LENGTH // The general length limit.
         - 15 // Save space for unique ID integer.
-        - std::string(suffix).size(); // Save space for '.json' extension
+        - std::strlen(suffix); // Save space for '.json' extension
       std::string file_name =
         make_valid_filename(key_converter(key), max_size);
       unsigned long uniqueness=file_name==index_file_name ? 1 : 0;