Add --vsd-arrays up-to-n-elements option

Default n is 10.
Additional --vsd-max-array-elements options gives finer control.

Author: jezhiggins

regression/goto-analyzer/variable-sensitivity-array-nondet-access/test-constants-up-to-3-elements.desc

@@ -0,0 +1,11 @@
+CORE
+main.c
+--show --variable-sensitivity --vsd-values constants --vsd-arrays up-to-n-elements --vsd-array-max-elements 3
+^EXIT=0$
+^SIGNAL=0$
+main::1::arr_at_ix \(\) -> TOP @ \[9\]
+main::1::arr_0_after_write \(\) -> TOP
+main::1::arr_1_after_write \(\) -> TOP
+main::1::arr_2_after_write \(\) -> TOP
+main::1::arr_3_after_write \(\) -> TOP
+main::1::arr_4_after_write \(\) -> TOP

regression/goto-analyzer/variable-sensitivity-array-nondet-access/test-intervals-up-to-3-elements.desc

@@ -0,0 +1,11 @@
+CORE
+main.c
+--show --variable-sensitivity --vsd-values intervals --vsd-arrays up-to-n-elements --vsd-array-max-elements 3
+^EXIT=0$
+^SIGNAL=0$
+main::1::arr_at_ix \(\) -> \[1, 5\] @ \[9\]
+main::1::arr_0_after_write \(\) -> \[1, 63\]
+main::1::arr_1_after_write \(\) -> \[2, 63\]
+main::1::arr_2_after_write \(\) -> \[3, 63\]
+main::1::arr_3_after_write \(\) -> \[3, 63\]
+main::1::arr_4_after_write \(\) -> \[3, 63\]

regression/goto-analyzer/variable-sensitivity-array-nondet-access/test-value-sets-up-to-3-elements.desc

@@ -0,0 +1,11 @@
+CORE
+main.c
+--show --variable-sensitivity --vsd-values set-of-constants --vsd-arrays up-to-n-elements --vsd-array-max-elements 3
+^EXIT=0$
+^SIGNAL=0$
+main::1::arr_at_ix \(\) -> value-set-begin: 1, 3, 4, 5 :value-set-end
+main::1::arr_0_after_write \(\) -> value-set-begin: 1, 99 :value-set-end
+main::1::arr_1_after_write \(\) -> value-set-begin: 2 :value-set-end
+main::1::arr_2_after_write \(\) -> value-set-begin: 3, 4, 5, 99 :value-set-end
+main::1::arr_3_after_write \(\) -> value-set-begin: 3, 4, 5, 99 :value-set-end
+main::1::arr_4_after_write \(\) -> value-set-begin: 3, 4, 5, 99 :value-set-end

src/analyses/variable-sensitivity/variable_sensitivity_configuration.cpp

@@ -47,8 +47,7 @@ vsd_configt vsd_configt::from_options(const optionst &options)
                               ? flow_sensitivityt::insensitive
                               : flow_sensitivityt::sensitive;
 
-  config.maximum_array_index =
-    option_to_size(options, "arrays", array_option_size_mappings);
+  config.maximum_array_index = configure_max_array_size(options);
 
   return config;
 }
@@ -105,12 +104,14 @@ const vsd_configt::option_mappingt vsd_configt::struct_option_mappings = {
 const vsd_configt::option_mappingt vsd_configt::array_option_mappings = {
   {"top-bottom", ARRAY_INSENSITIVE},
   {"smash", ARRAY_SENSITIVE},
+  {"up-to-n-elements", ARRAY_SENSITIVE},
   {"every-element", ARRAY_SENSITIVE}};
 
 const vsd_configt::option_size_mappingt
   vsd_configt::array_option_size_mappings = {
     {"top-bottom", 0},
     {"smash", 0},
+    {"up-to-n-elements", 10},
     {"every-element", std::numeric_limits<size_t>::max()}};
 
 const vsd_configt::option_mappingt vsd_configt::union_option_mappings = {
@@ -153,6 +154,17 @@ ABSTRACT_OBJECT_TYPET vsd_configt::option_to_abstract_type(
   return selected->second;
 }
 
+size_t vsd_configt::configure_max_array_size(const optionst &options)
+{
+  if(options.get_option("arrays") == "up-to-n-elements")
+  {
+    size_t max_elements = options.get_unsigned_int_option("array-max-elements");
+    if(max_elements != 0)
+      return max_elements - 1;
+  }
+  return option_to_size(options, "arrays", array_option_size_mappings);
+}
+
 size_t vsd_configt::option_to_size(
   const optionst &options,
   const std::string &option_name,

src/analyses/variable-sensitivity/variable_sensitivity_configuration.h

@@ -87,6 +87,8 @@ struct vsd_configt
     const option_mappingt &mapping,
     ABSTRACT_OBJECT_TYPET default_type);
 
+  static size_t configure_max_array_size(const optionst &options);
+
   static size_t option_to_size(
     const optionst &options,
     const std::string &option_name,

src/analyses/variable-sensitivity/variable_sensitivity_domain.h

@@ -75,6 +75,7 @@
   "(vsd-values):"                                                              \
   "(vsd-structs):"                                                             \
   "(vsd-arrays):"                                                              \
+  "(vsd-array-max-elements):"                                                  \
   "(vsd-pointers):"                                                            \
   "(vsd-unions):"                                                              \
   "(vsd-flow-insensitive)"                                                     \
@@ -88,7 +89,9 @@
   " --vsd-structs                struct field sensitive analysis - "           \
   "top-bottom|every-field\n" /* NOLINT(whitespace/line_length) */              \
   " --vsd-arrays                 array entry sensitive analysis - "            \
-  "top-bottom|smash|every-element\n" /* NOLINT(whitespace/line_length) */      \
+  "top-bottom|smash|up-to-n-elements|every-element\n" /* NOLINT(whitespace/line_length) */ \
+  " --vsd-array-max-elements     the n in --vsd-arrays up-to-n-elements - "    \
+  "defaults 10 if not given" /* NOLINT(whitespace/line_length) */ \
   " --vsd-pointers               pointer sensitive analysis - "                \
   "top-bottom|constants|value-set\n" /* NOLINT(whitespace/line_length) */      \
   " --vsd-unions                 union sensitive analysis - top-bottom\n"      \
@@ -102,6 +105,7 @@
   options.set_option("values", cmdline.get_value("vsd-values"));               \
   options.set_option("pointers", cmdline.get_value("vsd-pointers"));           \
   options.set_option("arrays", cmdline.get_value("vsd-arrays"));               \
+  options.set_option("array-max-elements", cmdline.get_value("vsd-array-max-elements")); /* NOLINT(whitespace/line_length) */ \
   options.set_option("structs", cmdline.get_value("vsd-structs"));             \
   options.set_option("unions", cmdline.get_value("vsd-unions"));               \
   options.set_option("flow-insensitive", cmdline.isset("vsd-flow-insensitive")); /* NOLINT(whitespace/line_length) */ \