|
| 1 | +// Author: Fotis Koutoulakis for Diffblue Ltd. |
| 2 | + |
| 3 | +#include "goto_inspect_parse_options.h" |
| 4 | + |
| 5 | +#include <util/config.h> |
| 6 | +#include <util/exception_utils.h> |
| 7 | +#include <util/exit_codes.h> |
| 8 | +#include <util/version.h> |
| 9 | + |
| 10 | +#include <goto-programs/goto_model.h> |
| 11 | +#include <goto-programs/read_goto_binary.h> |
| 12 | +#include <goto-programs/show_goto_functions.h> |
| 13 | + |
| 14 | +#include <iostream> |
| 15 | + |
| 16 | +int goto_inspect_parse_optionst::doit() |
| 17 | +{ |
| 18 | + if(cmdline.isset("version")) |
| 19 | + { |
| 20 | + std::cout << CBMC_VERSION << '\n'; |
| 21 | + return CPROVER_EXIT_SUCCESS; |
| 22 | + } |
| 23 | + |
| 24 | + // Before we do anything else, ensure that a file argument has been given. |
| 25 | + if(cmdline.args.size() != 1) |
| 26 | + { |
| 27 | + help(); |
| 28 | + throw invalid_command_line_argument_exceptiont{ |
| 29 | + "failed to supply a goto-binary name or an option for inspection", |
| 30 | + "<input goto-binary> <inspection-option>"}; |
| 31 | + } |
| 32 | + |
| 33 | + // This just sets up the defaults (and would interpret options such as --32). |
| 34 | + config.set(cmdline); |
| 35 | + |
| 36 | + // Normally we would register language front-ends here but as goto-inspect |
| 37 | + // only works on goto binaries, we don't need to |
| 38 | + |
| 39 | + auto binary_filename = cmdline.args[0]; |
| 40 | + |
| 41 | + // Read goto binary into goto-model |
| 42 | + auto read_goto_binary_result = |
| 43 | + read_goto_binary(binary_filename, ui_message_handler); |
| 44 | + if(!read_goto_binary_result.has_value()) |
| 45 | + { |
| 46 | + throw deserialization_exceptiont{ |
| 47 | + "failed to read goto program from file '" + binary_filename + "'"}; |
| 48 | + } |
| 49 | + auto goto_model = std::move(read_goto_binary_result.value()); |
| 50 | + |
| 51 | + // This has to be called after the defaults are set up (as per the |
| 52 | + // config.set(cmdline) above) otherwise, e.g. the architecture specification |
| 53 | + // will be unknown. |
| 54 | + config.set_from_symbol_table(goto_model.symbol_table); |
| 55 | + |
| 56 | + if(cmdline.isset("show-goto-functions")) |
| 57 | + { |
| 58 | + show_goto_functions( |
| 59 | + goto_model, ui_message_handler, cmdline.isset("list-goto-functions")); |
| 60 | + return CPROVER_EXIT_SUCCESS; |
| 61 | + } |
| 62 | + |
| 63 | + // If an option + binary was provided, the program will have exited |
| 64 | + // gracefully through a different branch. If we hit the code below, it |
| 65 | + // means that something has gone wrong - it's also possible to fall through |
| 66 | + // this case if no optional inspection flag is present in the argument |
| 67 | + // vector. This will ensure that the return value in that case is |
| 68 | + // semantically meaningful, and provide a return value that also satisfies |
| 69 | + // the compiler's requirements based on the signature of `doit()`. |
| 70 | + return CPROVER_EXIT_INCORRECT_TASK; |
| 71 | +} |
| 72 | + |
| 73 | +void goto_inspect_parse_optionst::help() |
| 74 | +{ |
| 75 | + std::cout << '\n' |
| 76 | + << banner_string("Goto-Inspect", CBMC_VERSION) << '\n' |
| 77 | + << align_center_with_border("Copyright (C) 2023") << '\n' |
| 78 | + << align_center_with_border("Diffblue Ltd.") << '\n' |
| 79 | + << align_center_with_border( "[email protected]") << '\n' |
| 80 | + << '\n' |
| 81 | + << "Usage: Purpose:\n" |
| 82 | + << '\n' |
| 83 | + << " goto-inspect [-?] [-h] [--help] show help\n" |
| 84 | + << " goto-inspect --version show version\n" |
| 85 | + << " goto-inspect --show-goto-functions show code for " |
| 86 | + "goto-functions present in goto-binary\n" |
| 87 | + << "\n" |
| 88 | + << "<in> goto binary to read from\n"; |
| 89 | +} |
| 90 | + |
| 91 | +goto_inspect_parse_optionst::goto_inspect_parse_optionst( |
| 92 | + int argc, |
| 93 | + const char *argv[]) |
| 94 | + : parse_options_baset{ |
| 95 | + GOTO_INSPECT_OPTIONS, |
| 96 | + argc, |
| 97 | + argv, |
| 98 | + std::string("GOTO-INSPECT ") + CBMC_VERSION} |
| 99 | +{ |
| 100 | +} |
0 commit comments