Parse c object factory options

Author: danpoe

src/cbmc/cbmc_parse_options.cpp

@@ -109,6 +109,7 @@ void cbmc_parse_optionst::get_command_line_options(optionst &options)
   }
 
   cbmc_parse_optionst::set_default_options(options);
+  parse_c_object_factory_options(cmdline, options);
 
   if(cmdline.isset("cover") && cmdline.isset("unwinding-assertions"))
   {
@@ -922,6 +923,10 @@ void cbmc_parse_optionst::help()
     " --round-to-plus-inf          rounding towards plus infinity\n"
     " --round-to-minus-inf         rounding towards minus infinity\n"
     " --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 pointers 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

@@ -12,6 +12,8 @@ Author: Daniel Kroening, kroening@kroening.com
 #ifndef CPROVER_CBMC_CBMC_PARSE_OPTIONS_H
 #define CPROVER_CBMC_CBMC_PARSE_OPTIONS_H
 
+#include <ansi-c/c_object_factory_parameters.h>
+
 #include <util/ui_message.h>
 #include <util/parse_options.h>
 #include <util/timestamper.h>
@@ -72,6 +74,7 @@ class optionst;
   OPT_FLUSH \
   "(localize-faults)(localize-faults-method):" \
   OPT_GOTO_TRACE \
+  "(max-nondet-tree-depth):" \
   "(claim):(show-claims)(floatbv)(all-claims)(all-properties)" // legacy, and will eventually disappear // NOLINT(whitespace/line_length)
 // clang-format on