|
| 1 | +/*******************************************************************\ |
| 2 | +Module: Parse Options Module |
| 3 | +Author: Qinheping Hu |
| 4 | +\*******************************************************************/ |
| 5 | + |
| 6 | +/// \file |
| 7 | +/// Main Module |
| 8 | + |
| 9 | +#include "goto_synthesizer_parse_options.h" |
| 10 | + |
| 11 | +#include <util/config.h> |
| 12 | +#include <util/exit_codes.h> |
| 13 | +#include <util/version.h> |
| 14 | + |
| 15 | +#include <goto-programs/read_goto_binary.h> |
| 16 | + |
| 17 | +#include <iostream> |
| 18 | + |
| 19 | +/// invoke main modules |
| 20 | +int goto_synthesizer_parse_optionst::doit() |
| 21 | +{ |
| 22 | + if(cmdline.isset("version")) |
| 23 | + { |
| 24 | + std::cout << CBMC_VERSION << '\n'; |
| 25 | + return CPROVER_EXIT_SUCCESS; |
| 26 | + } |
| 27 | + |
| 28 | + if(cmdline.args.size() != 1 && cmdline.args.size() != 2) |
| 29 | + { |
| 30 | + help(); |
| 31 | + return CPROVER_EXIT_USAGE_ERROR; |
| 32 | + } |
| 33 | + |
| 34 | + messaget::eval_verbosity( |
| 35 | + cmdline.get_value("verbosity"), messaget::M_STATISTICS, ui_message_handler); |
| 36 | + |
| 37 | + register_languages(); |
| 38 | + |
| 39 | + const auto result_get_goto_program = get_goto_program(); |
| 40 | + if(result_get_goto_program != CPROVER_EXIT_SUCCESS) |
| 41 | + return result_get_goto_program; |
| 42 | + |
| 43 | + // TODO |
| 44 | + // Migrate synthesizer and tests from goto-instrument to goto-synthesizer |
| 45 | + |
| 46 | + help(); |
| 47 | + return CPROVER_EXIT_USAGE_ERROR; |
| 48 | +} |
| 49 | + |
| 50 | +int goto_synthesizer_parse_optionst::get_goto_program() |
| 51 | +{ |
| 52 | + log.status() << "Reading GOTO program from '" << cmdline.args[0] << "'" |
| 53 | + << messaget::eom; |
| 54 | + |
| 55 | + config.set(cmdline); |
| 56 | + |
| 57 | + auto result = read_goto_binary(cmdline.args[0], ui_message_handler); |
| 58 | + |
| 59 | + if(!result.has_value()) |
| 60 | + return CPROVER_EXIT_USAGE_ERROR; |
| 61 | + |
| 62 | + goto_model = std::move(result.value()); |
| 63 | + |
| 64 | + config.set_from_symbol_table(goto_model.symbol_table); |
| 65 | + return CPROVER_EXIT_SUCCESS; |
| 66 | +} |
| 67 | + |
| 68 | +/// display command line help |
| 69 | +void goto_synthesizer_parse_optionst::help() |
| 70 | +{ |
| 71 | + // clang-format off |
| 72 | + std::cout << '\n' << banner_string("Goto-synthesizer", CBMC_VERSION) << '\n' |
| 73 | + << align_center_with_border("Copyright (C) 2022") << '\n' |
| 74 | + << align_center_with_border("Qinheping Hu") << '\n' |
| 75 | + << align_center_with_border( "[email protected]") << '\n' |
| 76 | + << |
| 77 | + "\n" |
| 78 | + "Usage: Purpose:\n" |
| 79 | + "\n" |
| 80 | + " goto-synthesizer [-?] [-h] [--help] show help\n" |
| 81 | + " goto-synthesizer in out synthesize and apply loop invariants.\n" // NOLINT(*) |
| 82 | + "\n" |
| 83 | + "Main options:\n" |
| 84 | + "\n" |
| 85 | + "Other options:\n" |
| 86 | + " --version show version and exit\n" |
| 87 | + " --xml-ui use XML-formatted output\n" |
| 88 | + " --json-ui use JSON-formatted output\n" |
| 89 | + " --verbosity # verbosity level\n" |
| 90 | + "\n"; |
| 91 | + // clang-format on |
| 92 | +} |
0 commit comments