1313
1414#include < util/config.h>
1515#include < util/exit_codes.h>
16+ #include < util/help_formatter.h>
1617#include < util/options.h>
1718#include < util/version.h>
1819
@@ -720,61 +721,59 @@ void janalyzer_parse_optionst::help()
720721 std::cout << ' \n ' << banner_string (" JANALYZER" , CBMC_VERSION) << ' \n '
721722 << align_center_with_border (" Copyright (C) 2016-2018" ) << ' \n '
722723 << align_center_with_border (" Daniel Kroening, Diffblue" ) << ' \n '
723- <<
align_center_with_border (
" [email protected] " ) <<
' \n ' 724- <<
724+ <<
align_center_with_border (
" [email protected] " ) <<
' \n ' ;
725+
726+ std::cout << help_formatter (
725727 " \n "
726- " Usage: Purpose :\n "
728+ " Usage: \t Purpose :\n "
727729 " \n "
728- " janalyzer [-? ] [-h ] [--help] show help\n "
729- " janalyzer \n "
730+ " {bjanalyzer} [{y-?} ] [{y-h} ] [{y --help}] \t show this help\n "
731+ " {bjanalyzer} \n "
730732 HELP_JAVA_METHOD_NAME
731- " janalyzer \n "
733+ " {bjanalyzer} \n "
732734 HELP_JAVA_CLASS_NAME
733- " janalyzer \n "
735+ " {bjanalyzer} \n "
734736 HELP_JAVA_JAR
735- " janalyzer \n "
737+ " {bjanalyzer} \n "
736738 HELP_JAVA_GOTO_BINARY
737739 " \n "
738740 HELP_JAVA_CLASSPATH
739741 HELP_FUNCTIONS
740742 " \n "
741743 " Task options:\n "
742- " --show display the abstract domains\n "
743- // NOLINTNEXTLINE(whitespace/line_length)
744- " --verify use the abstract domains to check assertions\n "
745- // NOLINTNEXTLINE(whitespace/line_length)
746- " --simplify file_name use the abstract domains to simplify the program\n "
747- " --no-simplify-slicing do not remove instructions from which no\n "
748- " property can be reached (use with --simplify)\n " // NOLINT(*)
749- " --unreachable-instructions list dead code\n "
750- // NOLINTNEXTLINE(whitespace/line_length)
751- " --unreachable-functions list functions unreachable from the entry point\n "
752- // NOLINTNEXTLINE(whitespace/line_length)
753- " --reachable-functions list functions reachable from the entry point\n "
744+ " {y--show} \t display the abstract domains\n "
745+ " {y--verify} \t use the abstract domains to check assertions\n "
746+ " {y--simplify} {ufile_name} \t use the abstract domains to simplify the"
747+ " program\n "
748+ " {y--no-simplify-slicing} \t do not remove instructions from which no"
749+ " property can be reached (use with {y--simplify})\n "
750+ " {y--unreachable-instructions} \t list dead code\n "
751+ " {y--unreachable-functions} \t list functions unreachable from the entry"
752+ " point"
753+ " {y--reachable-functions} \t list functions reachable from the entry point"
754754 " \n "
755755 " Abstract interpreter options:\n "
756- // NOLINTNEXTLINE(whitespace/line_length)
757- " --location-sensitive use location-sensitive abstract interpreter\n "
758- " --concurrent use concurrency-aware abstract interpreter\n "
756+ " {y--location-sensitive} \t use location-sensitive abstract interpreter"
757+ " {y--concurrent} \t use concurrency-aware abstract interpreter\n "
759758 " \n "
760759 " Domain options:\n "
761- " --constants constant domain\n "
762- " --intervals interval domain\n "
763- " --non-null non-null domain\n "
764- " --dependence-graph data and control dependencies between instructions\n " // NOLINT(*)
760+ " {y--constants} \t constant domain\n "
761+ " {y--intervals} \t interval domain\n "
762+ " {y--non-null} \t non-null domain\n "
763+ " {y--dependence-graph} \t data and control dependencies between"
764+ " instructions"
765765 " \n "
766766 " Output options:\n "
767- " --text file_name output results in plain text to given file\n "
768- // NOLINTNEXTLINE(whitespace/line_length)
769- " --json file_name output results in JSON format to given file\n "
770- " --xml file_name output results in XML format to given file\n "
771- " --dot file_name output results in DOT format to given file\n "
767+ " {y--text} {ufile_name} \t output results in plain text to given file\n "
768+ " {y--json} {ufile_name} \t output results in JSON format to given file\n "
769+ " {y--xml} {ufile_name} \t output results in XML format to given file\n "
770+ " {y--dot} {ufile_name} \t output results in DOT format to given file\n "
772771 " \n "
773772 " Specific analyses:\n "
774- // NOLINTNEXTLINE(whitespace/line_length)
775- " --taint file_name perform taint analysis using rules in given file\n "
776- " --show-taint print taint analysis results on stdout\n "
777- " --show-local-may-alias perform procedure-local may alias analysis\n "
773+ " {y--taint} {ufile_name} \t perform taint analysis using rules in given "
774+ " file\n "
775+ " {y --show-taint} \t print taint analysis results on stdout\n "
776+ " {y --show-local-may-alias} \t perform procedure-local may alias analysis\n "
778777 " \n "
779778 " Java Bytecode frontend options:\n "
780779 JAVA_BYTECODE_LANGUAGE_OPTIONS_HELP
@@ -783,20 +782,20 @@ void janalyzer_parse_optionst::help()
783782 HELP_CONFIG_PLATFORM
784783 " \n "
785784 " Program representations:\n "
786- " --show-parse-tree show parse tree\n "
787- " --show-symbol-table show loaded symbol table\n "
785+ " {y --show-parse-tree} \t show parse tree\n "
786+ " {y --show-symbol-table} \t show loaded symbol table\n "
788787 HELP_SHOW_GOTO_FUNCTIONS
789788 HELP_SHOW_PROPERTIES
790789 " \n "
791790 " Program instrumentation options:\n "
792- " --no-assertions ignore user assertions\n "
793- " --no-assumptions ignore user assumptions\n "
794- " --property id enable selected properties only\n "
791+ " {y --no-assertions} \t ignore user assertions\n "
792+ " {y --no-assumptions} \t ignore user assumptions\n "
793+ " {y --property} {uid} \t enable selected properties only\n "
795794 " \n "
796795 " Other options:\n "
797- " --version show version and exit\n "
798- " --verbosity # verbosity level\n "
796+ " {y --version} \t show version and exit\n "
797+ " {y --verbosity {u#} \t verbosity level\n "
799798 HELP_TIMESTAMP
800- " \n " ;
799+ " \n " ) ;
801800 // clang-format on
802801}
0 commit comments