|
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