CBMC
goto_inspect_parse_options.cpp
Go to the documentation of this file.
1 // Author: Fotis Koutoulakis for Diffblue Ltd.
2 
4 
5 #include <util/config.h>
6 #include <util/exception_utils.h>
7 #include <util/exit_codes.h>
8 #include <util/help_formatter.h>
9 #include <util/version.h>
10 
14 
15 #include <iostream>
16 
18 {
19  if(cmdline.isset("version"))
20  {
21  std::cout << CBMC_VERSION << '\n';
22  return CPROVER_EXIT_SUCCESS;
23  }
24 
25  // Before we do anything else, ensure that a file argument has been given.
26  if(cmdline.args.size() != 1)
27  {
28  help();
30  "failed to supply a goto-binary name or an option for inspection",
31  "<input goto-binary> <inspection-option>"};
32  }
33 
34  // This just sets up the defaults (and would interpret options such as --32).
36 
37  // Normally we would register language front-ends here but as goto-inspect
38  // only works on goto binaries, we don't need to
39 
40  auto binary_filename = cmdline.args[0];
41 
42  // Read goto binary into goto-model
43  auto read_goto_binary_result =
44  read_goto_binary(binary_filename, ui_message_handler);
45  if(!read_goto_binary_result.has_value())
46  {
48  "failed to read goto program from file '" + binary_filename + "'"};
49  }
50  auto goto_model = std::move(read_goto_binary_result.value());
51 
52  // This has to be called after the defaults are set up (as per the
53  // config.set(cmdline) above) otherwise, e.g. the architecture specification
54  // will be unknown.
55  config.set_from_symbol_table(goto_model.symbol_table);
56 
57  if(cmdline.isset("show-goto-functions"))
58  {
60  goto_model, ui_message_handler, cmdline.isset("list-goto-functions"));
61  return CPROVER_EXIT_SUCCESS;
62  }
63 
64  // If an option + binary was provided, the program will have exited
65  // gracefully through a different branch. If we hit the code below, it
66  // means that something has gone wrong - it's also possible to fall through
67  // this case if no optional inspection flag is present in the argument
68  // vector. This will ensure that the return value in that case is
69  // semantically meaningful, and provide a return value that also satisfies
70  // the compiler's requirements based on the signature of `doit()`.
72 }
73 
75 {
76  std::cout << '\n'
77  << banner_string("Goto-Inspect", CBMC_VERSION) << '\n'
78  << align_center_with_border("Copyright (C) 2023") << '\n'
79  << align_center_with_border("Diffblue Ltd.") << '\n'
80  << align_center_with_border("info@diffblue.com") << '\n';
81 
82  std::cout << help_formatter(
83  "\n"
84  "Usage: \tPurpose:\n"
85  "\n"
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"
90  "\n");
91 }
92 
94  int argc,
95  const char *argv[])
98  argc,
99  argv,
100  std::string("GOTO-INSPECT ") + CBMC_VERSION}
101 {
102 }
configt config
Definition: config.cpp:25
virtual bool isset(char option) const
Definition: cmdline.cpp:30
argst args
Definition: cmdline.h:151
bool set(const cmdlinet &cmdline)
Definition: config.cpp:798
void set_from_symbol_table(const symbol_table_baset &)
Definition: config.cpp:1266
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 ...
ui_message_handlert ui_message_handler
Definition: parse_options.h:45
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,...
Definition: exit_codes.h:49
#define CPROVER_EXIT_SUCCESS
Success indicates the required analysis has been performed without error.
Definition: exit_codes.h:16
#define GOTO_INSPECT_OPTIONS
Symbol Table + CFG.
Help Formatter.
static help_formattert help_formatter(const std::string &s)
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.
Read Goto Programs.
Show the goto functions.
goto_inspect_parse_optionst(int argc, const char *argv[])
const char * CBMC_VERSION