From 708acf4b0aaa57222563ccbcfcfec18bdde41e55 Mon Sep 17 00:00:00 2001 From: Daniel Kroening Date: Sun, 26 Aug 2018 22:11:05 +0100 Subject: [PATCH 1/3] missing newline in help --- src/cbmc/cbmc_parse_options.cpp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/cbmc/cbmc_parse_options.cpp b/src/cbmc/cbmc_parse_options.cpp index 6c876029513..096bded2b01 100644 --- a/src/cbmc/cbmc_parse_options.cpp +++ b/src/cbmc/cbmc_parse_options.cpp @@ -966,7 +966,7 @@ void cbmc_parse_optionst::help() " --refine-strings use string refinement (experimental)\n" " --string-printable add constraint that strings are printable (experimental)\n" // NOLINT(*) " --string-max-input-length add constraint on the length of input strings\n" // NOLINT(*) - " --string-max-length add constraint on the length of strings" + " --string-max-length add constraint on the length of strings\n" " (deprecated: use string-max-input-length instead)\n" // NOLINT(*) " --outfile filename output formula to given file\n" " --arrays-uf-never never turn arrays into uninterpreted functions\n" // NOLINT(*) From 5513c79e2b05cace739656d541049560fc16d069 Mon Sep 17 00:00:00 2001 From: Daniel Kroening Date: Sun, 26 Aug 2018 22:12:26 +0100 Subject: [PATCH 2/3] remove help for --smt1 option --- src/cbmc/cbmc_parse_options.cpp | 1 - 1 file changed, 1 deletion(-) diff --git a/src/cbmc/cbmc_parse_options.cpp b/src/cbmc/cbmc_parse_options.cpp index 096bded2b01..8fed2b68444 100644 --- a/src/cbmc/cbmc_parse_options.cpp +++ b/src/cbmc/cbmc_parse_options.cpp @@ -955,7 +955,6 @@ void cbmc_parse_optionst::help() " --dimacs generate CNF in DIMACS format\n" " --beautify beautify the counterexample (greedy heuristic)\n" // NOLINT(*) " --localize-faults localize faults (experimental)\n" - " --smt1 use default SMT1 solver (obsolete)\n" " --smt2 use default SMT2 solver (Z3)\n" " --boolector use Boolector\n" " --mathsat use MathSAT\n" From 30f055b34e624eb5101da14434fbc0c9abca701f Mon Sep 17 00:00:00 2001 From: Daniel Kroening Date: Sun, 26 Aug 2018 22:15:40 +0100 Subject: [PATCH 3/3] help: --drop-unused-functions belongs with the transformation --- src/cbmc/cbmc_parse_options.cpp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/cbmc/cbmc_parse_options.cpp b/src/cbmc/cbmc_parse_options.cpp index 8fed2b68444..964b64410f2 100644 --- a/src/cbmc/cbmc_parse_options.cpp +++ b/src/cbmc/cbmc_parse_options.cpp @@ -931,7 +931,6 @@ void cbmc_parse_optionst::help() " --show-parse-tree show parse tree\n" " --show-symbol-table show loaded symbol table\n" HELP_SHOW_GOTO_FUNCTIONS - " --drop-unused-functions drop functions trivially unreachable from main function\n" // NOLINT(*) "\n" "Program instrumentation options:\n" HELP_GOTO_CHECK @@ -942,6 +941,7 @@ void cbmc_parse_optionst::help() " --mm MM memory consistency model for concurrent programs\n" // NOLINT(*) HELP_REACHABILITY_SLICER " --full-slice run full slicer (experimental)\n" // NOLINT(*) + " --drop-unused-functions drop functions trivially unreachable from main function\n" // NOLINT(*) "\n" "Semantic transformations:\n" // NOLINTNEXTLINE(whitespace/line_length)