Skip to content

Commit 48d03c8

Browse files
committed
Parse c object factory options
1 parent c1eb656 commit 48d03c8

File tree

2 files changed

+8
-0
lines changed

2 files changed

+8
-0
lines changed

src/cbmc/cbmc_parse_options.cpp

Lines changed: 5 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -109,6 +109,7 @@ void cbmc_parse_optionst::get_command_line_options(optionst &options)
109109
}
110110

111111
cbmc_parse_optionst::set_default_options(options);
112+
parse_c_object_factory_options(cmdline, options);
112113

113114
if(cmdline.isset("cover") && cmdline.isset("unwinding-assertions"))
114115
{
@@ -922,6 +923,10 @@ void cbmc_parse_optionst::help()
922923
" --round-to-plus-inf rounding towards plus infinity\n"
923924
" --round-to-minus-inf rounding towards minus infinity\n"
924925
" --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(*) */ \
925930
HELP_FUNCTIONS
926931
"\n"
927932
"Program representations:\n"

src/cbmc/cbmc_parse_options.h

Lines changed: 3 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -12,6 +12,8 @@ Author: Daniel Kroening, [email protected]
1212
#ifndef CPROVER_CBMC_CBMC_PARSE_OPTIONS_H
1313
#define CPROVER_CBMC_CBMC_PARSE_OPTIONS_H
1414

15+
#include <ansi-c/c_object_factory_parameters.h>
16+
1517
#include <util/ui_message.h>
1618
#include <util/parse_options.h>
1719
#include <util/timestamper.h>
@@ -72,6 +74,7 @@ class optionst;
7274
OPT_FLUSH \
7375
"(localize-faults)(localize-faults-method):" \
7476
OPT_GOTO_TRACE \
77+
"(max-nondet-tree-depth):" \
7578
"(claim):(show-claims)(floatbv)(all-claims)(all-properties)" // legacy, and will eventually disappear // NOLINT(whitespace/line_length)
7679
// clang-format on
7780

0 commit comments

Comments
 (0)