Skip to content

Commit b26d347

Browse files
martin-csmartin-cs
authored
Merge pull request diffblue#5874 from martin-cs/refactor/config-set-up
Move the declaration and description of options that configt handles into config.h
2 parents ced2d39 + 42896e7 commit b26d347

9 files changed

+120
-143
lines changed

‎.gitignore

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -61,6 +61,7 @@ regression/**/tests-*.log
6161
regression/**/*.goto-cc-saved
6262
regression/**/*.gb
6363
regression/**/*.smt2
64+
regression/solver-hardness/solver-hardness-simple/solver_hardness.json
6465
jbmc/regression/**/tests.log
6566
jbmc/regression/**/tests-symex-driven-loading.log
6667

‎scripts/expected_doxygen_warnings.txt

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -84,7 +84,7 @@ warning: Included by graph for 'goto_functions.h' not generated, too many nodes
8484
warning: Included by graph for 'goto_model.h' not generated, too many nodes (110), threshold is 60. Consider increasing DOT_GRAPH_MAX_NODES.
8585
warning: Included by graph for 'arith_tools.h' not generated, too many nodes (181), threshold is 60. Consider increasing DOT_GRAPH_MAX_NODES.
8686
warning: Included by graph for 'c_types.h' not generated, too many nodes (110), threshold is 60. Consider increasing DOT_GRAPH_MAX_NODES.
87-
warning: Included by graph for 'config.h' not generated, too many nodes (85), threshold is 60. Consider increasing DOT_GRAPH_MAX_NODES.
87+
warning: Included by graph for 'config.h' not generated, too many nodes (87), threshold is 60. Consider increasing DOT_GRAPH_MAX_NODES.
8888
warning: Included by graph for 'exception_utils.h' not generated, too many nodes (61), threshold is 60. Consider increasing DOT_GRAPH_MAX_NODES.
8989
warning: Included by graph for 'expr.h' not generated, too many nodes (87), threshold is 60. Consider increasing DOT_GRAPH_MAX_NODES.
9090
warning: Included by graph for 'expr_util.h' not generated, too many nodes (61), threshold is 60. Consider increasing DOT_GRAPH_MAX_NODES.

‎src/cbmc/cbmc_parse_options.cpp

Lines changed: 7 additions & 61 deletions
Original file line numberDiff line numberDiff line change
@@ -203,9 +203,6 @@ void cbmc_parse_optionst::get_command_line_options(optionst &options)
203203
if(cmdline.isset("mm"))
204204
options.set_option("mm", cmdline.get_value("mm"));
205205

206-
if(cmdline.isset("c89"))
207-
config.ansi_c.set_c89();
208-
209206
if(cmdline.isset("symex-complexity-limit"))
210207
options.set_option(
211208
"symex-complexity-limit", cmdline.get_value("symex-complexity-limit"));
@@ -215,21 +212,6 @@ void cbmc_parse_optionst::get_command_line_options(optionst &options)
215212
"symex-complexity-failed-child-loops-limit",
216213
cmdline.get_value("symex-complexity-failed-child-loops-limit"));
217214

218-
if(cmdline.isset("c99"))
219-
config.ansi_c.set_c99();
220-
221-
if(cmdline.isset("c11"))
222-
config.ansi_c.set_c11();
223-
224-
if(cmdline.isset("cpp98"))
225-
config.cpp.set_cpp98();
226-
227-
if(cmdline.isset("cpp03"))
228-
config.cpp.set_cpp03();
229-
230-
if(cmdline.isset("cpp11"))
231-
config.cpp.set_cpp11();
232-
233215
if(cmdline.isset("property"))
234216
options.set_option("property", cmdline.get_values("property"));
235217

@@ -1016,46 +998,14 @@ void cbmc_parse_optionst::help()
1016998
" (implies --trace)\n"
1017999
"\n"
10181000
"C/C++ frontend options:\n"
1019-
" -I path set include path (C/C++)\n"
1020-
" -D macro define preprocessor macro (C/C++)\n"
10211001
" --preprocess stop after preprocessing\n"
1022-
" --16, --32, --64 set width of int\n"
1023-
" --LP64, --ILP64, --LLP64,\n"
1024-
" --ILP32, --LP32 set width of int, long and pointers\n"
1025-
" --little-endian allow little-endian word-byte conversions\n"
1026-
" --big-endian allow big-endian word-byte conversions\n"
1027-
" --unsigned-char make \"char\" unsigned by default\n"
1028-
" --mm model set memory model (default: sc)\n"
1029-
" --arch set architecture (default: "
1030-
<< configt::this_architecture() << ")\n"
1031-
" --os set operating system (default: "
1032-
<< configt::this_operating_system() << ")\n"
1033-
" --c89/99/11 set C language standard (default: "
1034-
<< (configt::ansi_ct::default_c_standard()==
1035-
configt::ansi_ct::c_standardt::C89?"c89":
1036-
configt::ansi_ct::default_c_standard()==
1037-
configt::ansi_ct::c_standardt::C99?"c99":
1038-
configt::ansi_ct::default_c_standard()==
1039-
configt::ansi_ct::c_standardt::C11?"c11":"") << ")\n" // NOLINT(*)
1040-
" --cpp98/03/11 set C++ language standard (default: "
1041-
<< (configt::cppt::default_cpp_standard()==
1042-
configt::cppt::cpp_standardt::CPP98?"cpp98": // NOLINT(*)
1043-
configt::cppt::default_cpp_standard()==
1044-
configt::cppt::cpp_standardt::CPP03?"cpp03": // NOLINT(*)
1045-
configt::cppt::default_cpp_standard()==
1046-
configt::cppt::cpp_standardt::CPP11?"cpp11":"") << ")\n" // NOLINT(*)
1047-
#ifdef _WIN32
1048-
" --gcc use GCC as preprocessor\n"
1049-
#endif
1050-
" --no-arch don't set up an architecture\n"
1051-
" --no-library disable built-in abstract C library\n"
1052-
" --round-to-nearest rounding towards nearest even (default)\n"
1053-
" --round-to-plus-inf rounding towards plus infinity\n"
1054-
" --round-to-minus-inf rounding towards minus infinity\n"
1055-
" --round-to-zero rounding towards zero\n"
1002+
HELP_CONFIG_C_CPP
10561003
HELP_ANSI_C_LANGUAGE
10571004
HELP_FUNCTIONS
10581005
"\n"
1006+
"Platform options:\n"
1007+
HELP_CONFIG_PLATFORM
1008+
"\n"
10591009
"Program representations:\n"
10601010
" --show-parse-tree show parse tree\n"
10611011
" --show-symbol-table show loaded symbol table\n"
@@ -1064,12 +1014,8 @@ void cbmc_parse_optionst::help()
10641014
"Program instrumentation options:\n"
10651015
HELP_GOTO_CHECK
10661016
HELP_COVER
1067-
" --mm MM memory consistency model for concurrent programs\n" // NOLINT(*)
1068-
// NOLINTNEXTLINE(whitespace/line_length)
1069-
" --malloc-fail-assert set malloc failure mode to assert-then-assume\n"
1070-
" --malloc-fail-null set malloc failure mode to return null\n"
1071-
// NOLINTNEXTLINE(whitespace/line_length)
1072-
" --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
10731019
HELP_REACHABILITY_SLICER
10741020
HELP_REACHABILITY_SLICER_FB
10751021
" --full-slice run full slicer (experimental)\n" // NOLINT(*)
@@ -1086,7 +1032,7 @@ void cbmc_parse_optionst::help()
10861032
HELP_BMC
10871033
"\n"
10881034
"Backend options:\n"
1089-
" --object-bits n number of bits used for object addresses\n"
1035+
HELP_CONFIG_BACKEND
10901036
" --dimacs generate CNF in DIMACS format\n"
10911037
" --beautify beautify the counterexample (greedy heuristic)\n" // NOLINT(*)
10921038
" --localize-faults localize faults (experimental)\n"

‎src/cbmc/cbmc_parse_options.h

Lines changed: 5 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,11 @@ 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 \
56+
OPT_CONFIG_BACKEND \
57+
OPT_CONFIG_LIBRARY \
5558
OPT_GOTO_CHECK \
56-
"(malloc-fail-assert)(malloc-fail-null)" \
57-
"(malloc-may-fail)" \
5859
OPT_XML_INTERFACE \
5960
OPT_JSON_INTERFACE \
6061
"(smt1)(smt2)(fpa)(cvc3)(cvc4)(boolector)(yices)(z3)(mathsat)" \
@@ -64,8 +65,6 @@ class optionst;
6465
"(beautify)" \
6566
"(dimacs)(refine)(max-node-refinement):(refine-arrays)(refine-arithmetic)"\
6667
OPT_STRING_REFINEMENT_CBMC \
67-
"(16)(32)(64)(LP64)(ILP64)(LLP64)(ILP32)(LP32)" \
68-
"(little-endian)(big-endian)" \
6968
OPT_SHOW_GOTO_FUNCTIONS \
7069
OPT_SHOW_PROPERTIES \
7170
"(show-symbol-table)(show-parse-tree)" \
@@ -79,11 +78,7 @@ class optionst;
7978
"(symex-coverage-report):" \
8079
"(mm):" \
8180
OPT_TIMESTAMP \
82-
"(i386-linux)(i386-macos)(i386-win32)(win32)(winx64)(gcc)" \
83-
"(ppc-macos)(unsigned-char)" \
8481
"(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)" \
8782
OPT_FLUSH \
8883
"(localize-faults)" \
8984
OPT_GOTO_TRACE \

‎src/goto-analyzer/goto_analyzer_parse_options.cpp

Lines changed: 5 additions & 48 deletions
Original file line numberDiff line numberDiff line change
@@ -101,26 +101,6 @@ void goto_analyzer_parse_optionst::get_command_line_options(optionst &options)
101101
if(cmdline.isset("function"))
102102
options.set_option("function", cmdline.get_value("function"));
103103

104-
#if 0
105-
if(cmdline.isset("c89"))
106-
config.ansi_c.set_c89();
107-
108-
if(cmdline.isset("c99"))
109-
config.ansi_c.set_c99();
110-
111-
if(cmdline.isset("c11"))
112-
config.ansi_c.set_c11();
113-
114-
if(cmdline.isset("cpp98"))
115-
config.cpp.set_cpp98();
116-
117-
if(cmdline.isset("cpp03"))
118-
config.cpp.set_cpp03();
119-
120-
if(cmdline.isset("cpp11"))
121-
config.cpp.set_cpp11();
122-
#endif
123-
124104
// all checks supported by goto_check
125105
PARSE_OPTIONS_GOTO_CHECK(cmdline, options);
126106

@@ -962,36 +942,12 @@ void goto_analyzer_parse_optionst::help()
962942
" --taint file_name perform taint analysis using rules in given file\n"
963943
"\n"
964944
"C/C++ frontend options:\n"
965-
" -I path set include path (C/C++)\n"
966-
" -D macro define preprocessor macro (C/C++)\n"
967-
" --arch X set architecture (default: "
968-
<< configt::this_architecture() << ")\n"
969-
" --os set operating system (default: "
970-
<< configt::this_operating_system() << ")\n"
971-
" --c89/99/11 set C language standard (default: "
972-
<< (configt::ansi_ct::default_c_standard()==
973-
configt::ansi_ct::c_standardt::C89?"c89":
974-
configt::ansi_ct::default_c_standard()==
975-
configt::ansi_ct::c_standardt::C99?"c99":
976-
configt::ansi_ct::default_c_standard()==
977-
configt::ansi_ct::c_standardt::C11?
978-
"c11":"") << ")\n"
979-
" --cpp98/03/11 set C++ language standard (default: "
980-
<< (configt::cppt::default_cpp_standard()==
981-
configt::cppt::cpp_standardt::CPP98?
982-
"cpp98":
983-
configt::cppt::default_cpp_standard()==
984-
configt::cppt::cpp_standardt::CPP03?
985-
"cpp03":
986-
configt::cppt::default_cpp_standard()==
987-
configt::cppt::cpp_standardt::CPP11?
988-
"cpp11":"") << ")\n"
989-
#ifdef _WIN32
990-
" --gcc use GCC as preprocessor\n"
991-
#endif
992-
" --no-library disable built-in abstract C library\n"
945+
HELP_CONFIG_C_CPP
993946
HELP_FUNCTIONS
994947
"\n"
948+
"Platform options:\n"
949+
HELP_CONFIG_PLATFORM
950+
"\n"
995951
"Program representations:\n"
996952
" --show-parse-tree show parse tree\n"
997953
" --show-symbol-table show loaded symbol table\n"
@@ -1000,6 +956,7 @@ void goto_analyzer_parse_optionst::help()
1000956
"\n"
1001957
"Program instrumentation options:\n"
1002958
HELP_GOTO_CHECK
959+
HELP_CONFIG_LIBRARY
1003960
"\n"
1004961
"Other options:\n"
1005962
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/goto-diff/goto_diff_parse_options.cpp

Lines changed: 0 additions & 18 deletions
Original file line numberDiff line numberDiff line change
@@ -97,24 +97,6 @@ void goto_diff_parse_optionst::get_command_line_options(optionst &options)
9797
if(cmdline.isset("mm"))
9898
options.set_option("mm", cmdline.get_value("mm"));
9999

100-
if(cmdline.isset("c89"))
101-
config.ansi_c.set_c89();
102-
103-
if(cmdline.isset("c99"))
104-
config.ansi_c.set_c99();
105-
106-
if(cmdline.isset("c11"))
107-
config.ansi_c.set_c11();
108-
109-
if(cmdline.isset("cpp98"))
110-
config.cpp.set_cpp98();
111-
112-
if(cmdline.isset("cpp03"))
113-
config.cpp.set_cpp03();
114-
115-
if(cmdline.isset("cpp11"))
116-
config.cpp.set_cpp11();
117-
118100
// all checks supported by goto_check
119101
PARSE_OPTIONS_GOTO_CHECK(cmdline, options);
120102

‎src/util/config.cpp

Lines changed: 18 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -1127,6 +1127,24 @@ bool configt::set(const cmdlinet &cmdline)
11271127

11281128
ansi_c.malloc_may_fail = cmdline.isset("malloc-may-fail");
11291129

1130+
if(cmdline.isset("c89"))
1131+
ansi_c.set_c89();
1132+
1133+
if(cmdline.isset("c99"))
1134+
ansi_c.set_c99();
1135+
1136+
if(cmdline.isset("c11"))
1137+
ansi_c.set_c11();
1138+
1139+
if(cmdline.isset("cpp98"))
1140+
cpp.set_cpp98();
1141+
1142+
if(cmdline.isset("cpp03"))
1143+
cpp.set_cpp03();
1144+
1145+
if(cmdline.isset("cpp11"))
1146+
cpp.set_cpp11();
1147+
11301148
return false;
11311149
}
11321150

0 commit comments

Comments
 (0)