File tree 2 files changed +8
-0
lines changed
2 files changed +8
-0
lines changed Original file line number Diff line number Diff line change @@ -109,6 +109,7 @@ void cbmc_parse_optionst::get_command_line_options(optionst &options)
109
109
}
110
110
111
111
cbmc_parse_optionst::set_default_options (options);
112
+ parse_c_object_factory_options (cmdline, options);
112
113
113
114
if (cmdline.isset (" cover" ) && cmdline.isset (" unwinding-assertions" ))
114
115
{
@@ -922,6 +923,10 @@ void cbmc_parse_optionst::help()
922
923
" --round-to-plus-inf rounding towards plus infinity\n "
923
924
" --round-to-minus-inf rounding towards minus infinity\n "
924
925
" --round-to-zero rounding towards zero\n "
926
+ " --max-nondet-tree-depth N limit size of nondet (e.g. input) object tree;\n " /* NOLINT(*) */ \
927
+ " at level N pointers are set to null\n " /* NOLINT(*) */ \
928
+ " --min-null-tree-depth N minimum level at which a pointer can first be\n " /* NOLINT(*) */ \
929
+ " NULL in a recursively nondet initialized struct\n " /* NOLINT(*) */ \
925
930
HELP_FUNCTIONS
926
931
" \n "
927
932
" Program representations:\n "
Original file line number Diff line number Diff line change 12
12
#ifndef CPROVER_CBMC_CBMC_PARSE_OPTIONS_H
13
13
#define CPROVER_CBMC_CBMC_PARSE_OPTIONS_H
14
14
15
+ #include < ansi-c/c_object_factory_parameters.h>
16
+
15
17
#include < util/ui_message.h>
16
18
#include < util/parse_options.h>
17
19
#include < util/timestamper.h>
@@ -72,6 +74,7 @@ class optionst;
72
74
OPT_FLUSH \
73
75
" (localize-faults)(localize-faults-method):" \
74
76
OPT_GOTO_TRACE \
77
+ " (max-nondet-tree-depth):" \
75
78
" (claim):(show-claims)(floatbv)(all-claims)(all-properties)" // legacy, and will eventually disappear // NOLINT(whitespace/line_length)
76
79
// clang-format on
77
80
You can’t perform that action at this time.
0 commit comments