Skip to content
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.

Commit a1496e0

Browse files
peterschrammelpeterschrammel
committedMar 21, 2019
[Do not merge] Use cmdline_definition in CBMC
1 parent f93e0e6 commit a1496e0

File tree

2 files changed

+76
-164
lines changed

2 files changed

+76
-164
lines changed
 

‎src/cbmc/cbmc_parse_options.cpp

+35-120
Original file line numberDiff line numberDiff line change
@@ -23,6 +23,7 @@ Author: Daniel Kroening, kroening@kroening.com
2323
#include <util/make_unique.h>
2424
#include <util/unicode.h>
2525
#include <util/version.h>
26+
#include <util/xml.h>
2627

2728
#include <langapi/language.h>
2829

@@ -83,7 +84,7 @@ Author: Daniel Kroening, kroening@kroening.com
8384
#include "xml_interface.h"
8485

8586
cbmc_parse_optionst::cbmc_parse_optionst(int argc, const char **argv)
86-
: parse_options_baset(CBMC_OPTIONS, argc, argv, ui_message_handler),
87+
: parse_options_baset(cbmc_options.to_option_string(), argc, argv, ui_message_handler),
8788
xml_interfacet(cmdline),
8889
messaget(ui_message_handler),
8990
ui_message_handler(cmdline, std::string("CBMC ") + CBMC_VERSION)
@@ -93,9 +94,9 @@ cbmc_parse_optionst::cbmc_parse_optionst(int argc, const char **argv)
9394
::cbmc_parse_optionst::cbmc_parse_optionst(
9495
int argc,
9596
const char **argv,
96-
const std::string &extra_options)
97+
const cmdline_definitiont &extra_options)
9798
: parse_options_baset(
98-
CBMC_OPTIONS + extra_options,
99+
(cbmc_options + extra_options).to_option_string(),
99100
argc,
100101
argv,
101102
ui_message_handler),
@@ -915,121 +916,35 @@ bool cbmc_parse_optionst::process_goto_program(
915916
/// display command line help
916917
void cbmc_parse_optionst::help()
917918
{
918-
// clang-format off
919-
std::cout << '\n' << banner_string("CBMC", CBMC_VERSION) << '\n'
920-
<< align_center_with_border("Copyright (C) 2001-2018") << '\n'
921-
<< align_center_with_border("Daniel Kroening, Edmund Clarke") << '\n' // NOLINT(*)
922-
<< align_center_with_border("Carnegie Mellon University, Computer Science Department") << '\n' // NOLINT(*)
923-
<< align_center_with_border("kroening@kroening.com") << '\n' // NOLINT(*)
924-
<< align_center_with_border("Protected in part by U.S. patent 7,225,417") << '\n' // NOLINT(*)
925-
<<
926-
"\n"
927-
"Usage: Purpose:\n"
928-
"\n"
929-
" cbmc [-?] [-h] [--help] show help\n"
930-
" cbmc file.c ... source file names\n"
931-
"\n"
932-
"Analysis options:\n"
933-
HELP_SHOW_PROPERTIES
934-
" --symex-coverage-report f generate a Cobertura XML coverage report in f\n" // NOLINT(*)
935-
" --property id only check one specific property\n"
936-
" --stop-on-fail stop analysis once a failed property is detected\n" // NOLINT(*)
937-
" --trace give a counterexample trace for failed properties\n" //NOLINT(*)
938-
"\n"
939-
"C/C++ frontend options:\n"
940-
" -I path set include path (C/C++)\n"
941-
" -D macro define preprocessor macro (C/C++)\n"
942-
" --preprocess stop after preprocessing\n"
943-
" --16, --32, --64 set width of int\n"
944-
" --LP64, --ILP64, --LLP64,\n"
945-
" --ILP32, --LP32 set width of int, long and pointers\n"
946-
" --little-endian allow little-endian word-byte conversions\n"
947-
" --big-endian allow big-endian word-byte conversions\n"
948-
" --unsigned-char make \"char\" unsigned by default\n"
949-
" --mm model set memory model (default: sc)\n"
950-
" --arch set architecture (default: "
951-
<< configt::this_architecture() << ")\n"
952-
" --os set operating system (default: "
953-
<< configt::this_operating_system() << ")\n"
954-
" --c89/99/11 set C language standard (default: "
955-
<< (configt::ansi_ct::default_c_standard()==
956-
configt::ansi_ct::c_standardt::C89?"c89":
957-
configt::ansi_ct::default_c_standard()==
958-
configt::ansi_ct::c_standardt::C99?"c99":
959-
configt::ansi_ct::default_c_standard()==
960-
configt::ansi_ct::c_standardt::C11?"c11":"") << ")\n" // NOLINT(*)
961-
" --cpp98/03/11 set C++ language standard (default: "
962-
<< (configt::cppt::default_cpp_standard()==
963-
configt::cppt::cpp_standardt::CPP98?"cpp98": // NOLINT(*)
964-
configt::cppt::default_cpp_standard()==
965-
configt::cppt::cpp_standardt::CPP03?"cpp03": // NOLINT(*)
966-
configt::cppt::default_cpp_standard()==
967-
configt::cppt::cpp_standardt::CPP11?"cpp11":"") << ")\n" // NOLINT(*)
968-
#ifdef _WIN32
969-
" --gcc use GCC as preprocessor\n"
970-
#endif
971-
" --no-arch don't set up an architecture\n"
972-
" --no-library disable built-in abstract C library\n"
973-
" --round-to-nearest rounding towards nearest even (default)\n"
974-
" --round-to-plus-inf rounding towards plus infinity\n"
975-
" --round-to-minus-inf rounding towards minus infinity\n"
976-
" --round-to-zero rounding towards zero\n"
977-
HELP_ANSI_C_LANGUAGE
978-
HELP_FUNCTIONS
979-
"\n"
980-
"Program representations:\n"
981-
" --show-parse-tree show parse tree\n"
982-
" --show-symbol-table show loaded symbol table\n"
983-
HELP_SHOW_GOTO_FUNCTIONS
984-
"\n"
985-
"Program instrumentation options:\n"
986-
HELP_GOTO_CHECK
987-
" --no-assertions ignore user assertions\n"
988-
" --no-assumptions ignore user assumptions\n"
989-
" --error-label label check that label is unreachable\n"
990-
" --cover CC create test-suite with coverage criterion CC\n" // NOLINT(*)
991-
" --mm MM memory consistency model for concurrent programs\n" // NOLINT(*)
992-
HELP_REACHABILITY_SLICER
993-
HELP_REACHABILITY_SLICER_FB
994-
" --full-slice run full slicer (experimental)\n" // NOLINT(*)
995-
" --drop-unused-functions drop functions trivially unreachable from main function\n" // NOLINT(*)
996-
"\n"
997-
"Semantic transformations:\n"
998-
// NOLINTNEXTLINE(whitespace/line_length)
999-
" --nondet-static add nondeterministic initialization of variables with static lifetime\n"
1000-
"\n"
1001-
"BMC options:\n"
1002-
HELP_BMC
1003-
"\n"
1004-
"Backend options:\n"
1005-
" --object-bits n number of bits used for object addresses\n"
1006-
" --dimacs generate CNF in DIMACS format\n"
1007-
" --beautify beautify the counterexample (greedy heuristic)\n" // NOLINT(*)
1008-
" --localize-faults localize faults (experimental)\n"
1009-
" --smt2 use default SMT2 solver (Z3)\n"
1010-
" --boolector use Boolector\n"
1011-
" --cprover-smt2 use CPROVER SMT2 solver\n"
1012-
" --cvc4 use CVC4\n"
1013-
" --mathsat use MathSAT\n"
1014-
" --yices use Yices\n"
1015-
" --z3 use Z3\n"
1016-
" --refine use refinement procedure (experimental)\n"
1017-
HELP_STRING_REFINEMENT_CBMC
1018-
" --outfile filename output formula to given file\n"
1019-
" --arrays-uf-never never turn arrays into uninterpreted functions\n" // NOLINT(*)
1020-
" --arrays-uf-always always turn arrays into uninterpreted functions\n" // NOLINT(*)
1021-
"\n"
1022-
"Other options:\n"
1023-
" --version show version and exit\n"
1024-
" --xml-ui use XML-formatted output\n"
1025-
" --xml-interface bi-directional XML interface\n"
1026-
" --json-ui use JSON-formatted output\n"
1027-
// NOLINTNEXTLINE(whitespace/line_length)
1028-
HELP_VALIDATE
1029-
HELP_GOTO_TRACE
1030-
HELP_FLUSH
1031-
" --verbosity # verbosity level\n"
1032-
HELP_TIMESTAMP
1033-
"\n";
1034-
// clang-format on
919+
switch(ui_message_handler.get_ui())
920+
{
921+
case ui_message_handlert::uit::PLAIN:
922+
// clang-format off
923+
log.result()
924+
<< '\n' << banner_string("CBMC", CBMC_VERSION) << '\n'
925+
<< align_center_with_border("Copyright (C) 2001-2018") << '\n'
926+
<< align_center_with_border("Daniel Kroening, Edmund Clarke")
927+
<< '\n' // NOLINT(*)
928+
<< align_center_with_border(
929+
"Carnegie Mellon University, Computer Science Department")
930+
<< '\n' // NOLINT(*)
931+
<< align_center_with_border("kroening@kroening.com") << '\n' // NOLINT(*)
932+
<< align_center_with_border("Protected in part by U.S. patent 7,225,417")
933+
<< '\n' // NOLINT(*)
934+
<<
935+
"\n"
936+
"Usage: Purpose:\n"
937+
"\n"
938+
" cbmc [-?] [-h] [--help] show help\n"
939+
" cbmc file.c ... source file names\n"
940+
<< cbmc_options.to_help_text(30, 80) << messaget::eom;
941+
// clang-format on
942+
break;
943+
case ui_message_handlert::uit::JSON_UI:
944+
ui_message_handler.get_json_stream().push_back(cbmc_options.to_json());
945+
break;
946+
case ui_message_handlert::uit::XML_UI:
947+
log.result() << cbmc_options.to_xml();
948+
break;
949+
}
1035950
}

‎src/cbmc/cbmc_parse_options.h

+41-44
Original file line numberDiff line numberDiff line change
@@ -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>
@@ -38,49 +39,45 @@ class goto_functionst;
3839
class optionst;
3940

4041
// clang-format off
41-
#define CBMC_OPTIONS \
42-
OPT_BMC \
43-
"(preprocess)(slice-by-trace):" \
44-
OPT_FUNCTIONS \
45-
"(no-simplify)(full-slice)" \
46-
OPT_REACHABILITY_SLICER \
47-
"(debug-level):(no-propagation)(no-simplify-if)" \
48-
"(document-subgoals)(outfile):(test-preprocessor)" \
49-
"D:I:(c89)(c99)(c11)(cpp98)(cpp03)(cpp11)" \
50-
"(object-bits):" \
51-
OPT_GOTO_CHECK \
52-
"(no-assertions)(no-assumptions)" \
53-
"(xml-ui)(xml-interface)(json-ui)" \
54-
"(smt1)(smt2)(fpa)(cvc3)(cvc4)(boolector)(yices)(z3)(mathsat)" \
55-
"(cprover-smt2)" \
56-
"(no-sat-preprocessor)" \
57-
"(beautify)" \
58-
"(dimacs)(refine)(max-node-refinement):(refine-arrays)(refine-arithmetic)"\
59-
OPT_STRING_REFINEMENT_CBMC \
60-
"(16)(32)(64)(LP64)(ILP64)(LLP64)(ILP32)(LP32)" \
61-
"(little-endian)(big-endian)" \
62-
OPT_SHOW_GOTO_FUNCTIONS \
63-
OPT_SHOW_PROPERTIES \
64-
"(show-symbol-table)(show-parse-tree)" \
65-
"(drop-unused-functions)" \
66-
"(property):(stop-on-fail)(trace)" \
67-
"(error-label):(verbosity):(no-library)" \
68-
"(nondet-static)" \
69-
"(version)" \
70-
"(cover):(symex-coverage-report):" \
71-
"(mm):" \
72-
OPT_TIMESTAMP \
73-
"(i386-linux)(i386-macos)(i386-win32)(win32)(winx64)(gcc)" \
74-
"(ppc-macos)(unsigned-char)" \
75-
"(arrays-uf-always)(arrays-uf-never)" \
76-
"(string-abstraction)(no-arch)(arch):" \
77-
"(round-to-nearest)(round-to-plus-inf)(round-to-minus-inf)(round-to-zero)" \
78-
OPT_FLUSH \
79-
"(localize-faults)" \
80-
OPT_GOTO_TRACE \
81-
OPT_VALIDATE \
82-
OPT_ANSI_C_LANGUAGE \
83-
"(claim):(show-claims)(floatbv)(all-claims)(all-properties)" // legacy, and will eventually disappear // NOLINT(whitespace/line_length)
42+
const cmdline_definitiont ui_options
43+
{
44+
{
45+
"json-ui",
46+
{},
47+
"use JSON-formatted output",
48+
"Other options",
49+
{}
50+
},
51+
{
52+
"xml-ui",
53+
{},
54+
"use XML-formatted output",
55+
"Other options",
56+
{}
57+
}
58+
};
59+
60+
const cmdline_definitiont cbmc_options(
61+
ui_options
62+
+ cmdline_definitiont{
63+
{
64+
"preprocess",
65+
{},
66+
"stop after preprocessing. "
67+
"This is a veeeeeeeeeeeeeeeeery long help text. "
68+
"This is a veeeeeeeeeeeeeeeeery long help text.",
69+
"C/C++ frontend options",
70+
{}
71+
},
72+
{
73+
"slice-by-trace",
74+
cmdline_optiont::argumentt{"f", "string"},
75+
"",
76+
"",
77+
cmdline_optiont::deprecatedt("-slice-by-trace has been removed")
78+
}
79+
}
80+
+ ui_options);
8481
// clang-format on
8582

8683
class cbmc_parse_optionst:
@@ -96,7 +93,7 @@ class cbmc_parse_optionst:
9693
cbmc_parse_optionst(
9794
int argc,
9895
const char **argv,
99-
const std::string &extra_options);
96+
const cmdline_definitiont &extra_options);
10097

10198
/// \brief Set the options that have default values
10299
///

0 commit comments

Comments
 (0)
Please sign in to comment.