Add max-field-sensitivity-array-size option

together with no-array-field-sensitivity, this makes it possible to
control the maximum size for which the transformation is applied and
totally deactivate field sensitivity for arrays if needed.

Author: romainbrenguier

jbmc/src/jbmc/jbmc_parse_options.cpp

@@ -135,6 +135,25 @@ void jbmc_parse_optionst::get_command_line_options(optionst &options)
   parse_java_language_options(cmdline, options);
   parse_java_object_factory_options(cmdline, options);
 
+  if(cmdline.isset("max-field-sensitivity-array-size"))
+  {
+    options.set_option(
+      "max-field-sensitivity-array-size",
+      cmdline.get_value("max-field-sensitivity-array-size"));
+  }
+
+  if(cmdline.isset("no-array-field-sensitivity"))
+  {
+    if(cmdline.isset("max-field-sensitivity-array-size"))
+    {
+      log.error()
+        << "--no-array-field-sensitivity and --max-field-sensitivity-array-size"
+        << " must not be given together" << messaget::eom;
+      exit(CPROVER_EXIT_USAGE_ERROR);
+    }
+    options.set_option("no-array-field-sensitivity", true);
+  }
+
   if(cmdline.isset("show-symex-strategies"))
   {
     log.status() << show_path_strategies() << messaget::eom;

src/cbmc/cbmc_parse_options.cpp

@@ -147,6 +147,25 @@ void cbmc_parse_optionst::get_command_line_options(optionst &options)
     exit(CPROVER_EXIT_USAGE_ERROR);
   }
 
+  if(cmdline.isset("max-field-sensitivity-array-size"))
+  {
+    options.set_option(
+      "max-field-sensitivity-array-size",
+      cmdline.get_value("max-field-sensitivity-array-size"));
+  }
+
+  if(cmdline.isset("no-array-field-sensitivity"))
+  {
+    if(cmdline.isset("max-field-sensitivity-array-size"))
+    {
+      log.error()
+        << "--no-array-field-sensitivity and --max-field-sensitivity-array-size"
+        << " must not be given together" << messaget::eom;
+      exit(CPROVER_EXIT_USAGE_ERROR);
+    }
+    options.set_option("no-array-field-sensitivity", true);
+  }
+
   if(cmdline.isset("partial-loops") && cmdline.isset("unwinding-assertions"))
   {
     log.error()

src/goto-checker/bmc_util.h

@@ -186,7 +186,8 @@ void run_property_decider(
   "(show-symex-strategies)" \
   "(depth):" \
   "(unwind):" \
-  "(unwindset):" \
+  "(max-field-sensitivity-array-size):" \
+  "(no-array-field-sensitivity)" \
   "(graphml-witness):" \
   "(unwindset):"
 
@@ -198,6 +199,14 @@ void run_property_decider(
   " --program-only               only show program expression\n" \
   " --show-loops                 show the loops in the program\n" \
   " --depth nr                   limit search depth\n" \
+  " --max-field-sensitivity-array-size M\n" \
+  "                              maximum size M of arrays for which field\n" \
+  "                              sensitivity will be applied to array,\n" \
+  "                              the default is 64\n" \
+  " --no-array-field-sensitivity\n" \
+  "                              deactivate field sensitivity for arrays, this is\n" \
+  "                              equivalent to setting the maximum field \n" \
+  "                              sensitivity size for arrays to 0\n" \
   " --unwind nr                  unwind nr times\n" \
   " --unwindset L:B,...          unwind loop L with a bound of B\n" \
   "                              (use --show-loops to get the loop IDs)\n" \

src/goto-symex/symex_main.cpp

@@ -46,7 +46,12 @@ symex_configt::symex_configt(const optionst &options)
     run_validation_checks(options.get_bool_option("validate-ssa-equation")),
     show_symex_steps(options.get_bool_option("show-goto-symex-steps")),
     max_field_sensitivity_array_size(
-      options.get_unsigned_int_option("max-field-sensitivity-array-size"))
+      options.is_set("no-array-field-sensitivity")
+        ? 0
+        : options.is_set("max-field-sensitivity-array-size")
+            ? options.get_unsigned_int_option(
+                "max-field-sensitivity-array-size")
+            : DEFAULT_MAX_FIELD_SENSITIVITY_ARRAY_SIZE)
 {
 }