@@ -15,6 +15,7 @@ Author: Daniel Kroening, kroening@kroening.com
1515#include < ansi-c/ansi_c_language.h>
1616#include < ansi-c/c_object_factory_parameters.h>
1717
18+ #include < util/cmdline_definition.h>
1819#include < util/parse_options.h>
1920#include < util/timestamper.h>
2021#include < util/ui_message.h>
@@ -77,50 +78,6 @@ const cmdline_definitiont cbmc_options(
7778 }
7879 }
7980 + ui_options);
80-
81- #define CBMC_OPTIONS \
82- OPT_BMC \
83- " (preprocess)(slice-by-trace):" \
84- OPT_FUNCTIONS \
85- " (no-simplify)(full-slice)" \
86- OPT_REACHABILITY_SLICER \
87- " (debug-level):(no-propagation)(no-simplify-if)" \
88- " (document-subgoals)(outfile):(test-preprocessor)" \
89- " D:I:(c89)(c99)(c11)(cpp98)(cpp03)(cpp11)" \
90- " (object-bits):" \
91- OPT_GOTO_CHECK \
92- " (no-assertions)(no-assumptions)" \
93- " (xml-ui)(xml-interface)(json-ui)" \
94- " (smt1)(smt2)(fpa)(cvc3)(cvc4)(boolector)(yices)(z3)(mathsat)" \
95- " (cprover-smt2)" \
96- " (no-sat-preprocessor)" \
97- " (beautify)" \
98- " (dimacs)(refine)(max-node-refinement):(refine-arrays)(refine-arithmetic)" \
99- OPT_STRING_REFINEMENT_CBMC \
100- " (16)(32)(64)(LP64)(ILP64)(LLP64)(ILP32)(LP32)" \
101- " (little-endian)(big-endian)" \
102- OPT_SHOW_GOTO_FUNCTIONS \
103- OPT_SHOW_PROPERTIES \
104- " (show-symbol-table)(show-parse-tree)" \
105- " (drop-unused-functions)" \
106- " (property):(stop-on-fail)(trace)" \
107- " (error-label):(verbosity):(no-library)" \
108- " (nondet-static)" \
109- " (version)" \
110- " (cover):(symex-coverage-report):" \
111- " (mm):" \
112- OPT_TIMESTAMP \
113- " (i386-linux)(i386-macos)(i386-win32)(win32)(winx64)(gcc)" \
114- " (ppc-macos)(unsigned-char)" \
115- " (arrays-uf-always)(arrays-uf-never)" \
116- " (string-abstraction)(no-arch)(arch):" \
117- " (round-to-nearest)(round-to-plus-inf)(round-to-minus-inf)(round-to-zero)" \
118- OPT_FLUSH \
119- " (localize-faults)" \
120- OPT_GOTO_TRACE \
121- OPT_VALIDATE \
122- OPT_ANSI_C_LANGUAGE \
123- " (claim):(show-claims)(floatbv)(all-claims)(all-properties)" // legacy, and will eventually disappear // NOLINT(whitespace/line_length)
12481// clang-format on
12582
12683class cbmc_parse_optionst :
0 commit comments