Add option --min-null-tree-depth to cbmc

Author: danpoe

src/cbmc/cbmc_parse_options.cpp

@@ -925,6 +925,8 @@ void cbmc_parse_optionst::help()
     " --round-to-zero              rounding towards zero\n"
     " --max-nondet-tree-depth N    limit size of nondet (e.g. input) object tree;\n" /* NOLINT(*) */ \
     "                              at level N references are set to null\n" /* NOLINT(*) */ \
+    " --min-null-tree-depth N      minimum level at which a pointer can first be\n" /* NOLINT(*) */ \
+    "                              NULL in a recursively nondet initialized struct\n" /* NOLINT(*) */ \
     HELP_FUNCTIONS
     "\n"
     "Program representations:\n"

src/cbmc/cbmc_parse_options.h

@@ -75,6 +75,7 @@ class optionst;
   "(localize-faults)(localize-faults-method):" \
   OPT_GOTO_TRACE \
   "(max-nondet-tree-depth):" \
+  "(min-null-tree-depth):" \
   "(claim):(show-claims)(floatbv)(all-claims)(all-properties)" // legacy, and will eventually disappear // NOLINT(whitespace/line_length)
 // clang-format on
 

src/util/object_factory_parameters.cpp

@@ -23,6 +23,11 @@ void object_factory_parameterst::set(const optionst &options)
     max_nondet_tree_depth =
       options.get_unsigned_int_option("max-nondet-tree-depth");
   }
+  if(options.is_set("min-null-tree-depth"))
+  {
+    min_null_tree_depth =
+      options.get_unsigned_int_option("min-null-tree-depth");
+  }
   if(options.is_set("max-nondet-string-length"))
   {
     max_nondet_string_length =
@@ -54,6 +59,11 @@ void parse_object_factory_options(const cmdlinet &cmdline, optionst &options)
     options.set_option(
       "max-nondet-tree-depth", cmdline.get_value("max-nondet-tree-depth"));
   }
+  if(cmdline.isset("min-null-tree-depth"))
+  {
+    options.set_option(
+      "min-null-tree-depth", cmdline.get_value("min-null-tree-depth"));
+  }
   if(cmdline.isset("max-nondet-string-length"))
   {
     options.set_option(