Extend memory-snapshot options

To handle treating pointers as arrays together with their sizes (similar to
function arguments in function-call harness).

Author: Petr Bauch

src/goto-harness/memory_snapshot_harness_generator.cpp

@@ -34,6 +34,46 @@ void memory_snapshot_harness_generatort::handle_option(
   if(recursive_initialization_config.handle_option(option, values))
   {
   }
+  else if(option == MEMORY_SNAPSHOT_HARNESS_TREAT_POINTER_AS_ARRAY_OPT)
+  {
+    recursive_initialization_config.pointers_to_treat_as_arrays.insert(
+      values.begin(), values.end());
+  }
+  else if(option == MEMORY_SNAPSHOT_HARNESS_ASSOCIATED_ARRAY_SIZE_OPT)
+  {
+    for(auto const &array_size_pair : values)
+    {
+      try
+      {
+        std::string array;
+        std::string size;
+        split_string(array_size_pair, ':', array, size);
+        // --associated-array-size implies --treat-pointer-as-array
+        // but it is not an error to specify both, so we don't check
+        // for duplicates here
+        recursive_initialization_config.pointers_to_treat_as_arrays.insert(
+          array);
+        auto const inserted =
+          recursive_initialization_config
+            .array_name_to_associated_array_size_variable.emplace(array, size);
+        if(!inserted.second)
+        {
+          throw invalid_command_line_argument_exceptiont{
+            "can not have two associated array sizes for one array",
+            "--" MEMORY_SNAPSHOT_HARNESS_ASSOCIATED_ARRAY_SIZE_OPT};
+        }
+      }
+      catch(const deserialization_exceptiont &)
+      {
+        throw invalid_command_line_argument_exceptiont{
+          "`" + array_size_pair +
+            "' is in an invalid format for array size pair",
+          "--" MEMORY_SNAPSHOT_HARNESS_ASSOCIATED_ARRAY_SIZE_OPT,
+          "array_name:size_name, where both are the names of global "
+          "variables"};
+      }
+    }
+  }
   else if(option == MEMORY_SNAPSHOT_HARNESS_SNAPSHOT_OPT)
   {
     memory_snapshot_file = require_exactly_one_value(option, values);

src/goto-harness/memory_snapshot_harness_generator_options.h

@@ -14,12 +14,16 @@ Author: Diffblue Ltd.
 #define MEMORY_SNAPSHOT_HARNESS_SNAPSHOT_OPT "memory-snapshot"
 #define MEMORY_SNAPSHOT_HARNESS_INITIAL_LOCATION_OPT "initial-location"
 #define MEMORY_SNAPSHOT_HARNESS_HAVOC_VARIABLES_OPT "havoc-variables"
+#define MEMORY_SNAPSHOT_HARNESS_TREAT_POINTER_AS_ARRAY_OPT "pointer-as-array"
+#define MEMORY_SNAPSHOT_HARNESS_ASSOCIATED_ARRAY_SIZE_OPT "size-of-array"
 
 // clang-format off
 #define MEMORY_SNAPSHOT_HARNESS_GENERATOR_OPTIONS                              \
   "(" MEMORY_SNAPSHOT_HARNESS_SNAPSHOT_OPT "):"                                \
   "(" MEMORY_SNAPSHOT_HARNESS_INITIAL_LOCATION_OPT "):"                        \
   "(" MEMORY_SNAPSHOT_HARNESS_HAVOC_VARIABLES_OPT "):"                         \
+  "(" MEMORY_SNAPSHOT_HARNESS_TREAT_POINTER_AS_ARRAY_OPT "):"                  \
+  "(" MEMORY_SNAPSHOT_HARNESS_ASSOCIATED_ARRAY_SIZE_OPT "):"                   \
 // MEMORY_SNAPSHOT_HARNESS_GENERATOR_OPTIONS
 
 // clang-format on
@@ -37,6 +41,16 @@ Author: Diffblue Ltd.
   " variables from `vars' to\n"                                                \
   "                              non-deterministic values\n"                   \
   COMMON_HARNESS_GENERATOR_HELP                                                \
+  "--" MEMORY_SNAPSHOT_HARNESS_TREAT_POINTER_AS_ARRAY_OPT                      \
+  " p    treat the global pointer with the name `p' as\n"                      \
+  "                              an array\n"                                   \
+  "--" MEMORY_SNAPSHOT_HARNESS_ASSOCIATED_ARRAY_SIZE_OPT                       \
+  " array_name:size_name\n"                                                    \
+  "                              set the parameter <size_name> to the size"    \
+  " of\n                              the array <array_name>\n"                \
+  "                              (implies "                                    \
+  "-- " MEMORY_SNAPSHOT_HARNESS_TREAT_POINTER_AS_ARRAY_OPT                     \
+  " <array_name>)\n"                                                           \
 // MEMORY_SNAPSHOT_HARNESS_GENERATOR_HELP
 
 // clang-format on