Parse c object factory options

Author: danpoe

src/ansi-c/ansi_c_language.h

@@ -18,6 +18,18 @@ Author: Daniel Kroening, [email protected]
 
 #include "ansi_c_parse_tree.h"
 
+// clang-format off
+#define OPT_ANSI_C_LANGUAGE \
+  "(max-nondet-tree-depth):" \
+  "(min-null-tree-depth):"
+
+#define HELP_ANSI_C_LANGUAGE \
+  " --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" \
+  " --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(*) */
+// clang-format on
+
 class ansi_c_languaget:public languaget
 {
 public:

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"))
   {
@@ -933,6 +934,7 @@ 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"
+    HELP_ANSI_C_LANGUAGE
     HELP_FUNCTIONS
     "\n"
     "Program representations:\n"

src/cbmc/cbmc_parse_options.h

@@ -12,6 +12,9 @@ Author: Daniel Kroening, [email protected]
 #ifndef CPROVER_CBMC_CBMC_PARSE_OPTIONS_H
 #define CPROVER_CBMC_CBMC_PARSE_OPTIONS_H
 
+#include <ansi-c/ansi_c_language.h>
+#include <ansi-c/c_object_factory_parameters.h>
+
 #include <util/parse_options.h>
 #include <util/timestamper.h>
 #include <util/ui_message.h>
@@ -75,6 +78,7 @@ class optionst;
   "(localize-faults)(localize-faults-method):" \
   OPT_GOTO_TRACE \
   OPT_VALIDATE \
+  OPT_ANSI_C_LANGUAGE \
   "(claim):(show-claims)(floatbv)(all-claims)(all-properties)" // legacy, and will eventually disappear // NOLINT(whitespace/line_length)
 // clang-format on