13
13
14
14
#include < util/config.h>
15
15
#include < util/exit_codes.h>
16
+ #include < util/help_formatter.h>
16
17
#include < util/options.h>
17
18
#include < util/version.h>
18
19
@@ -720,61 +721,59 @@ void janalyzer_parse_optionst::help()
720
721
std::cout << ' \n ' << banner_string (" JANALYZER" , CBMC_VERSION) << ' \n '
721
722
<< align_center_with_border (" Copyright (C) 2016-2018" ) << ' \n '
722
723
<< 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 (
725
727
" \n "
726
- " Usage: Purpose :\n "
728
+ " Usage: \t Purpose :\n "
727
729
" \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 "
730
732
HELP_JAVA_METHOD_NAME
731
- " janalyzer \n "
733
+ " {bjanalyzer} \n "
732
734
HELP_JAVA_CLASS_NAME
733
- " janalyzer \n "
735
+ " {bjanalyzer} \n "
734
736
HELP_JAVA_JAR
735
- " janalyzer \n "
737
+ " {bjanalyzer} \n "
736
738
HELP_JAVA_GOTO_BINARY
737
739
" \n "
738
740
HELP_JAVA_CLASSPATH
739
741
HELP_FUNCTIONS
740
742
" \n "
741
743
" 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"
754
754
" \n "
755
755
" 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 "
759
758
" \n "
760
759
" 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"
765
765
" \n "
766
766
" 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 "
772
771
" \n "
773
772
" 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 "
778
777
" \n "
779
778
" Java Bytecode frontend options:\n "
780
779
JAVA_BYTECODE_LANGUAGE_OPTIONS_HELP
@@ -783,20 +782,20 @@ void janalyzer_parse_optionst::help()
783
782
HELP_CONFIG_PLATFORM
784
783
" \n "
785
784
" 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 "
788
787
HELP_SHOW_GOTO_FUNCTIONS
789
788
HELP_SHOW_PROPERTIES
790
789
" \n "
791
790
" 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 "
795
794
" \n "
796
795
" 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 "
799
798
HELP_TIMESTAMP
800
- " \n " ;
799
+ " \n " ) ;
801
800
// clang-format on
802
801
}
0 commit comments