30 "failed to supply a goto-binary name or an option for inspection",
31 "<input goto-binary> <inspection-option>"};
40 auto binary_filename =
cmdline.args[0];
43 auto read_goto_binary_result =
45 if(!read_goto_binary_result.has_value())
48 "failed to read goto program from file '" + binary_filename +
"'"};
50 auto goto_model = std::move(read_goto_binary_result.value());
55 config.set_from_symbol_table(goto_model.symbol_table);
57 if(
cmdline.isset(
"show-goto-functions"))
86 " {bgoto-inspect} [{y-?}] [{y-h}] [{y--help}] \t show this help\n"
87 " {bgoto-inspect} {y--version} \t show version and exit\n"
88 " {bgoto-inspect} {y--show-goto-functions} {ufile_name} \t show code for"
89 " goto-functions present in goto-binary {ufile_name}\n"
Thrown when failing to deserialize a value from some low level format, like JSON or raw bytes.
Thrown when users pass incorrect command line arguments, for example passing no files to analysis or ...
parse_options_baset(const std::string &optstring, int argc, const char **argv, const std::string &program)
ui_message_handlert ui_message_handler
static void show_goto_functions(const goto_modelt &goto_model)
Document and give macros for the exit codes of CPROVER binaries.
#define CPROVER_EXIT_INCORRECT_TASK
The command line is correctly structured but cannot be carried out due to missing files,...
#define CPROVER_EXIT_SUCCESS
Success indicates the required analysis has been performed without error.
#define GOTO_INSPECT_OPTIONS
std::string align_center_with_border(const std::string &text)
Utility for displaying help centered messages borderered by "* *".
std::string banner_string(const std::string &front_end, const std::string &version)
static bool read_goto_binary(const std::string &filename, symbol_tablet &, goto_functionst &, message_handlert &)
Read a goto binary from a file, but do not update config.
goto_inspect_parse_optionst(int argc, const char *argv[])
const char * CBMC_VERSION