Skip to content

Commit a1d7785

Browse files
author
martin
committed
Move the definition and description of config's options into config.h
This should not change the functionality apart from: - goto-analyzer no longer parses Java options. They were ignored so this is an improvement. - The no-arch option is no longer supported or documented. It didn't work and was ignored so, again, an improvement. - The '--gcc' option is now described in the help documentation on all platforms.
1 parent 64c1757 commit a1d7785

File tree

5 files changed

+98
-86
lines changed

5 files changed

+98
-86
lines changed

‎src/cbmc/cbmc_parse_options.cpp

Lines changed: 7 additions & 43 deletions
Original file line numberDiff line numberDiff line change
@@ -998,46 +998,14 @@ void cbmc_parse_optionst::help()
998998
" (implies --trace)\n"
999999
"\n"
10001000
"C/C++ frontend options:\n"
1001-
" -I path set include path (C/C++)\n"
1002-
" -D macro define preprocessor macro (C/C++)\n"
10031001
" --preprocess stop after preprocessing\n"
1004-
" --16, --32, --64 set width of int\n"
1005-
" --LP64, --ILP64, --LLP64,\n"
1006-
" --ILP32, --LP32 set width of int, long and pointers\n"
1007-
" --little-endian allow little-endian word-byte conversions\n"
1008-
" --big-endian allow big-endian word-byte conversions\n"
1009-
" --unsigned-char make \"char\" unsigned by default\n"
1010-
" --mm model set memory model (default: sc)\n"
1011-
" --arch set architecture (default: "
1012-
<< configt::this_architecture() << ")\n"
1013-
" --os set operating system (default: "
1014-
<< configt::this_operating_system() << ")\n"
1015-
" --c89/99/11 set C language standard (default: "
1016-
<< (configt::ansi_ct::default_c_standard()==
1017-
configt::ansi_ct::c_standardt::C89?"c89":
1018-
configt::ansi_ct::default_c_standard()==
1019-
configt::ansi_ct::c_standardt::C99?"c99":
1020-
configt::ansi_ct::default_c_standard()==
1021-
configt::ansi_ct::c_standardt::C11?"c11":"") << ")\n" // NOLINT(*)
1022-
" --cpp98/03/11 set C++ language standard (default: "
1023-
<< (configt::cppt::default_cpp_standard()==
1024-
configt::cppt::cpp_standardt::CPP98?"cpp98": // NOLINT(*)
1025-
configt::cppt::default_cpp_standard()==
1026-
configt::cppt::cpp_standardt::CPP03?"cpp03": // NOLINT(*)
1027-
configt::cppt::default_cpp_standard()==
1028-
configt::cppt::cpp_standardt::CPP11?"cpp11":"") << ")\n" // NOLINT(*)
1029-
#ifdef _WIN32
1030-
" --gcc use GCC as preprocessor\n"
1031-
#endif
1032-
" --no-arch don't set up an architecture\n"
1033-
" --no-library disable built-in abstract C library\n"
1034-
" --round-to-nearest rounding towards nearest even (default)\n"
1035-
" --round-to-plus-inf rounding towards plus infinity\n"
1036-
" --round-to-minus-inf rounding towards minus infinity\n"
1037-
" --round-to-zero rounding towards zero\n"
1002+
HELP_CONFIG_C_CPP
10381003
HELP_ANSI_C_LANGUAGE
10391004
HELP_FUNCTIONS
10401005
"\n"
1006+
"Platform options:\n"
1007+
HELP_CONFIG_PLATFORM
1008+
"\n"
10411009
"Program representations:\n"
10421010
" --show-parse-tree show parse tree\n"
10431011
" --show-symbol-table show loaded symbol table\n"
@@ -1046,12 +1014,8 @@ void cbmc_parse_optionst::help()
10461014
"Program instrumentation options:\n"
10471015
HELP_GOTO_CHECK
10481016
HELP_COVER
1049-
" --mm MM memory consistency model for concurrent programs\n" // NOLINT(*)
1050-
// NOLINTNEXTLINE(whitespace/line_length)
1051-
" --malloc-fail-assert set malloc failure mode to assert-then-assume\n"
1052-
" --malloc-fail-null set malloc failure mode to return null\n"
1053-
// NOLINTNEXTLINE(whitespace/line_length)
1054-
" --malloc-may-fail allow malloc calls to return a null pointer\n"
1017+
" --mm MM memory consistency model for concurrent programs (default: sc)\n" // NOLINT(*)
1018+
HELP_CONFIG_LIBRARY
10551019
HELP_REACHABILITY_SLICER
10561020
HELP_REACHABILITY_SLICER_FB
10571021
" --full-slice run full slicer (experimental)\n" // NOLINT(*)
@@ -1068,7 +1032,7 @@ void cbmc_parse_optionst::help()
10681032
HELP_BMC
10691033
"\n"
10701034
"Backend options:\n"
1071-
" --object-bits n number of bits used for object addresses\n"
1035+
HELP_CONFIG_BACKEND
10721036
" --dimacs generate CNF in DIMACS format\n"
10731037
" --beautify beautify the counterexample (greedy heuristic)\n" // NOLINT(*)
10741038
" --localize-faults localize faults (experimental)\n"

‎src/cbmc/cbmc_parse_options.h

Lines changed: 3 additions & 10 deletions
Original file line numberDiff line numberDiff line change
@@ -15,6 +15,7 @@ Author: Daniel Kroening, [email protected]
1515
#include <ansi-c/ansi_c_language.h>
1616
#include <ansi-c/c_object_factory_parameters.h>
1717

18+
#include <util/config.h>
1819
#include <util/parse_options.h>
1920
#include <util/timestamper.h>
2021
#include <util/ui_message.h>
@@ -50,11 +51,9 @@ class optionst;
5051
"(document-subgoals)(outfile):(test-preprocessor)" \
5152
"(write-solver-stats-to):" \
5253
"(show-array-constraints)" \
53-
"D:I:(c89)(c99)(c11)(cpp98)(cpp03)(cpp11)" \
54-
"(object-bits):" \
54+
OPT_CONFIG_C_CPP \
55+
OPT_CONFIG_PLATFORM \
5556
OPT_GOTO_CHECK \
56-
"(malloc-fail-assert)(malloc-fail-null)" \
57-
"(malloc-may-fail)" \
5857
OPT_XML_INTERFACE \
5958
OPT_JSON_INTERFACE \
6059
"(smt1)(smt2)(fpa)(cvc3)(cvc4)(boolector)(yices)(z3)(mathsat)" \
@@ -64,8 +63,6 @@ class optionst;
6463
"(beautify)" \
6564
"(dimacs)(refine)(max-node-refinement):(refine-arrays)(refine-arithmetic)"\
6665
OPT_STRING_REFINEMENT_CBMC \
67-
"(16)(32)(64)(LP64)(ILP64)(LLP64)(ILP32)(LP32)" \
68-
"(little-endian)(big-endian)" \
6966
OPT_SHOW_GOTO_FUNCTIONS \
7067
OPT_SHOW_PROPERTIES \
7168
"(show-symbol-table)(show-parse-tree)" \
@@ -79,11 +76,7 @@ class optionst;
7976
"(symex-coverage-report):" \
8077
"(mm):" \
8178
OPT_TIMESTAMP \
82-
"(i386-linux)(i386-macos)(i386-win32)(win32)(winx64)(gcc)" \
83-
"(ppc-macos)(unsigned-char)" \
8479
"(arrays-uf-always)(arrays-uf-never)" \
85-
"(string-abstraction)(no-arch)(arch):" \
86-
"(round-to-nearest)(round-to-plus-inf)(round-to-minus-inf)(round-to-zero)" \
8780
OPT_FLUSH \
8881
"(localize-faults)" \
8982
OPT_GOTO_TRACE \

‎src/goto-analyzer/goto_analyzer_parse_options.cpp

Lines changed: 5 additions & 28 deletions
Original file line numberDiff line numberDiff line change
@@ -942,36 +942,12 @@ void goto_analyzer_parse_optionst::help()
942942
" --taint file_name perform taint analysis using rules in given file\n"
943943
"\n"
944944
"C/C++ frontend options:\n"
945-
" -I path set include path (C/C++)\n"
946-
" -D macro define preprocessor macro (C/C++)\n"
947-
" --arch X set architecture (default: "
948-
<< configt::this_architecture() << ")\n"
949-
" --os set operating system (default: "
950-
<< configt::this_operating_system() << ")\n"
951-
" --c89/99/11 set C language standard (default: "
952-
<< (configt::ansi_ct::default_c_standard()==
953-
configt::ansi_ct::c_standardt::C89?"c89":
954-
configt::ansi_ct::default_c_standard()==
955-
configt::ansi_ct::c_standardt::C99?"c99":
956-
configt::ansi_ct::default_c_standard()==
957-
configt::ansi_ct::c_standardt::C11?
958-
"c11":"") << ")\n"
959-
" --cpp98/03/11 set C++ language standard (default: "
960-
<< (configt::cppt::default_cpp_standard()==
961-
configt::cppt::cpp_standardt::CPP98?
962-
"cpp98":
963-
configt::cppt::default_cpp_standard()==
964-
configt::cppt::cpp_standardt::CPP03?
965-
"cpp03":
966-
configt::cppt::default_cpp_standard()==
967-
configt::cppt::cpp_standardt::CPP11?
968-
"cpp11":"") << ")\n"
969-
#ifdef _WIN32
970-
" --gcc use GCC as preprocessor\n"
971-
#endif
972-
" --no-library disable built-in abstract C library\n"
945+
HELP_CONFIG_C_CPP
973946
HELP_FUNCTIONS
974947
"\n"
948+
"Platform options:\n"
949+
HELP_CONFIG_PLATFORM
950+
"\n"
975951
"Program representations:\n"
976952
" --show-parse-tree show parse tree\n"
977953
" --show-symbol-table show loaded symbol table\n"
@@ -980,6 +956,7 @@ void goto_analyzer_parse_optionst::help()
980956
"\n"
981957
"Program instrumentation options:\n"
982958
HELP_GOTO_CHECK
959+
HELP_CONFIG_LIBRARY
983960
"\n"
984961
"Other options:\n"
985962
HELP_VALIDATE

‎src/goto-analyzer/goto_analyzer_parse_options.h

Lines changed: 3 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -89,6 +89,7 @@ Author: Daniel Kroening, [email protected]
8989
#ifndef CPROVER_GOTO_ANALYZER_GOTO_ANALYZER_PARSE_OPTIONS_H
9090
#define CPROVER_GOTO_ANALYZER_GOTO_ANALYZER_PARSE_OPTIONS_H
9191

92+
#include <util/config.h>
9293
#include <util/parse_options.h>
9394
#include <util/timestamper.h>
9495
#include <util/ui_message.h>
@@ -157,18 +158,15 @@ class optionst;
157158

158159
#define GOTO_ANALYSER_OPTIONS \
159160
OPT_FUNCTIONS \
160-
"D:I:(std89)(std99)(std11)" \
161-
"(classpath):(cp):(main-class):" \
162-
"(16)(32)(64)(LP64)(ILP64)(LLP64)(ILP32)(LP32)" \
163-
"(little-endian)(big-endian)" \
161+
OPT_CONFIG_C_CPP \
162+
OPT_CONFIG_PLATFORM \
164163
OPT_SHOW_GOTO_FUNCTIONS \
165164
OPT_SHOW_PROPERTIES \
166165
OPT_GOTO_CHECK \
167166
"(show-loops)" \
168167
"(show-symbol-table)(show-parse-tree)" \
169168
"(show-reachable-properties)(property):" \
170169
"(verbosity):(version)" \
171-
"(gcc)(arch):" \
172170
OPT_FLUSH \
173171
OPT_TIMESTAMP \
174172
OPT_VALIDATE \

‎src/util/config.h

Lines changed: 80 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -20,6 +20,86 @@ class cmdlinet;
2020
class symbol_tablet;
2121
class namespacet;
2222

23+
// Configt is the one place beyond *_parse_options where options are ... parsed.
24+
// Options that are handled by configt are documented here.
25+
26+
// clang-format off
27+
#define OPT_CONFIG_C_CPP \
28+
"D:I:(include)(function)" \
29+
"(c89)(c99)(c11)(cpp98)(cpp03)(cpp11)" \
30+
"(unsigned-char)" \
31+
"(round-to-even)(round-to-nearest)" \
32+
"(round-to-plus-inf)(round-to-minus-inf)(round-to-zero)" \
33+
34+
#define HELP_CONFIG_C_CPP \
35+
" -I path set include path (C/C++)\n" \
36+
" -D macro define preprocessor macro (C/C++)\n" \
37+
" --c89/99/11 set C language standard (default: " \
38+
<< (configt::ansi_ct::default_c_standard()== \
39+
configt::ansi_ct::c_standardt::C89?"c89": \
40+
configt::ansi_ct::default_c_standard()== \
41+
configt::ansi_ct::c_standardt::C99?"c99": \
42+
configt::ansi_ct::default_c_standard()== \
43+
configt::ansi_ct::c_standardt::C11?"c11":"") << ")\n"\
44+
" --cpp98/03/11 set C++ language standard (default: " \
45+
<< (configt::cppt::default_cpp_standard()== \
46+
configt::cppt::cpp_standardt::CPP98?"cpp98":\
47+
configt::cppt::default_cpp_standard()== \
48+
configt::cppt::cpp_standardt::CPP03?"cpp03":\
49+
configt::cppt::default_cpp_standard()== \
50+
configt::cppt::cpp_standardt::CPP11?"cpp11":"") << ")\n"\
51+
" --unsigned-char make \"char\" unsigned by default\n" \
52+
" --round-to-nearest rounding towards nearest even (default)\n" \
53+
" --round-to-plus-inf rounding towards plus infinity\n" \
54+
" --round-to-minus-inf rounding towards minus infinity\n" \
55+
" --round-to-zero rounding towards zero\n" \
56+
57+
58+
#define OPT_CONFIG_LIBRARY \
59+
"(malloc-fail-assert)(malloc-fail-null)(malloc-may-fail)" \
60+
"(no-library)" \
61+
"(string-abstraction)" \
62+
63+
#define HELP_CONFIG_LIBRARY \
64+
" --malloc-fail-assert set malloc failure mode to assert-then-assume\n"\
65+
" --malloc-fail-null set malloc failure mode to return null\n" \
66+
" --malloc-may-fail allow malloc calls to return a null pointer\n" \
67+
" --no-library disable built-in abstract C library\n" \
68+
69+
70+
#define OPT_CONFIG_JAVA \
71+
"(classpath)(cp)(main-class)" \
72+
73+
74+
#define OPT_CONFIG_PLATFORM \
75+
"(arch):(os):" \
76+
"(16)(32)(64)(LP64)(ILP64)(LLP64)(ILP32)(LP32)" \
77+
"(little-endian)(big-endian)" \
78+
"(i386-linux)" \
79+
"(i386-win32)(win32)(winx64)" \
80+
"(i386-macos)(ppc-macos)" \
81+
"(gcc)" \
82+
83+
#define HELP_CONFIG_PLATFORM \
84+
" --arch set architecture (default: " \
85+
<< configt::this_architecture() << ")\n" \
86+
" --os set operating system (default: " \
87+
<< configt::this_operating_system() << ")\n" \
88+
" --16, --32, --64 set width of int\n" \
89+
" --LP64, --ILP64, --LLP64,\n" \
90+
" --ILP32, --LP32 set width of int, long and pointers\n" \
91+
" --little-endian allow little-endian word-byte conversions\n" \
92+
" --big-endian allow big-endian word-byte conversions\n" \
93+
" --gcc use GCC as preprocessor\n" \
94+
95+
#define OPT_CONFIG_BACKEND \
96+
"(object-bits)" \
97+
98+
#define HELP_CONFIG_BACKEND \
99+
" --object-bits n number of bits used for object addresses\n"
100+
101+
// clang-format on
102+
23103
/*! \brief Globally accessible architectural configuration
24104
*/
25105
class configt

0 commit comments

Comments
 (0)