|
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,93 +721,81 @@ 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( |
| 727 | + "\n" |
| 728 | + "Usage: \tPurpose:\n" |
| 729 | + "\n" |
| 730 | + " {bjanalyzer} [{y-?}] [{y-h}] [{y--help}] \t show this help\n" |
| 731 | + " {bjanalyzer}\n" |
| 732 | + HELP_JAVA_METHOD_NAME |
| 733 | + " {bjanalyzer}\n" |
| 734 | + HELP_JAVA_CLASS_NAME |
| 735 | + " {bjanalyzer}\n" |
| 736 | + HELP_JAVA_JAR |
| 737 | + " {bjanalyzer}\n" |
| 738 | + HELP_JAVA_GOTO_BINARY |
725 | 739 | "\n"
|
726 |
| - "Usage: Purpose:\n" |
| 740 | + HELP_JAVA_CLASSPATH |
| 741 | + HELP_FUNCTIONS |
727 | 742 | "\n"
|
728 |
| - " janalyzer [-?] [-h] [--help] show help\n" |
729 |
| - " janalyzer\n" |
730 |
| - << HELP_JAVA_METHOD_NAME |
731 |
| - << " janalyzer\n" |
732 |
| - << HELP_JAVA_CLASS_NAME |
733 |
| - << " janalyzer\n" |
734 |
| - << HELP_JAVA_JAR |
735 |
| - << " janalyzer\n" |
736 |
| - << HELP_JAVA_GOTO_BINARY |
737 |
| - << "\n" |
738 |
| - << HELP_JAVA_CLASSPATH |
739 |
| - << HELP_FUNCTIONS |
740 |
| - << "\n" |
741 | 743 | "Task options:\n"
|
742 |
| - << help_entry("--show", "display the abstract domains") |
743 |
| - << help_entry("--verify", "use the abstract domains to check assertions") |
744 |
| - << help_entry( |
745 |
| - "--simplify file_name", |
746 |
| - "use the abstract domains to simplify the program") |
747 |
| - << help_entry( |
748 |
| - "--no-simplify-slicing", |
749 |
| - "do not remove instructions from which no property can be reached (use " |
750 |
| - "with --simplify)") |
751 |
| - << help_entry("--unreachable-instructions", "list dead code") |
752 |
| - << help_entry( |
753 |
| - "--unreachable-functions", |
754 |
| - "list functions unreachable from the entry point") |
755 |
| - << help_entry( |
756 |
| - "--reachable-functions", "list functions reachable from the entry point") |
757 |
| - << "\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 | + "\n" |
758 | 755 | "Abstract interpreter options:\n"
|
759 |
| - << help_entry( |
760 |
| - "--location-sensitive", "use location-sensitive abstract interpreter") |
761 |
| - << help_entry("--concurrent", "use concurrency-aware abstract interpreter") |
762 |
| - << "\n" |
| 756 | + " {y--location-sensitive} \t use location-sensitive abstract interpreter" |
| 757 | + " {y--concurrent} \t use concurrency-aware abstract interpreter\n" |
| 758 | + "\n" |
763 | 759 | "Domain options:\n"
|
764 |
| - << help_entry("--constants", "constant domain") |
765 |
| - << help_entry("--intervals", "interval domain") |
766 |
| - << help_entry("--non-null", "non-null domain") |
767 |
| - << help_entry( |
768 |
| - "--dependence-graph", |
769 |
| - "data and control dependencies between instructions") |
770 |
| - << "\n" |
| 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 | + "\n" |
771 | 766 | "Output options:\n"
|
772 |
| - << help_entry( |
773 |
| - "--text file_name", "output results in plain text to given file") |
774 |
| - << help_entry( |
775 |
| - "--json file_name", "output results in JSON format to given file") |
776 |
| - << help_entry( |
777 |
| - "--xml file_name", "output results in XML format to given file") |
778 |
| - << help_entry( |
779 |
| - "--dot file_name", "output results in DOT format to given file") |
780 |
| - << "\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" |
| 771 | + "\n" |
781 | 772 | "Specific analyses:\n"
|
782 |
| - << help_entry( |
783 |
| - "--taint file_name", "perform taint analysis using rules in given file") |
784 |
| - << help_entry( |
785 |
| - "--show-taint", "print taint analysis results on stdout") |
786 |
| - << help_entry( |
787 |
| - "--show-local-may-alias", "perform procedure-local may alias analysis") |
788 |
| - << "\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" |
| 777 | + "\n" |
789 | 778 | "Java Bytecode frontend options:\n"
|
790 |
| - << JAVA_BYTECODE_LANGUAGE_OPTIONS_HELP |
791 |
| - << "\n" |
| 779 | + JAVA_BYTECODE_LANGUAGE_OPTIONS_HELP |
| 780 | + "\n" |
792 | 781 | "Platform options:\n"
|
793 |
| - << HELP_CONFIG_PLATFORM |
794 |
| - << "\n" |
| 782 | + HELP_CONFIG_PLATFORM |
| 783 | + "\n" |
795 | 784 | "Program representations:\n"
|
796 |
| - << help_entry("--show-parse-tree", "show parse tree") |
797 |
| - << help_entry("--show-symbol-table", "show loaded symbol table") |
798 |
| - << HELP_SHOW_GOTO_FUNCTIONS |
799 |
| - << HELP_SHOW_PROPERTIES |
800 |
| - << "\n" |
| 785 | + " {y--show-parse-tree} \t show parse tree\n" |
| 786 | + " {y--show-symbol-table} \t show loaded symbol table\n" |
| 787 | + HELP_SHOW_GOTO_FUNCTIONS |
| 788 | + HELP_SHOW_PROPERTIES |
| 789 | + "\n" |
801 | 790 | "Program instrumentation options:\n"
|
802 |
| - << help_entry("--no-assertions", "ignore user assertions") |
803 |
| - << help_entry("--no-assumptions", "ignore user assumptions") |
804 |
| - << help_entry("--property id", "enable selected properties only") |
805 |
| - << "\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" |
| 794 | + "\n" |
806 | 795 | "Other options:\n"
|
807 |
| - << help_entry("--version", "show version and exit") |
808 |
| - << help_entry("--verbosity #", "verbosity level") |
809 |
| - << HELP_TIMESTAMP |
810 |
| - << "\n"; |
| 796 | + " {y--version} \t show version and exit\n" |
| 797 | + " {y--verbosity {u#} \t verbosity level\n" |
| 798 | + HELP_TIMESTAMP |
| 799 | + "\n"); |
811 | 800 | // clang-format on
|
812 | 801 | }
|
0 commit comments