CBMC
parse_options.cpp
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module:
4 
5 Author: Daniel Kroening, kroening@kroening.com
6 
7 \*******************************************************************/
8 
9 #include "parse_options.h"
10 
11 #include <climits>
12 
13 #if defined (_WIN32)
14 #define EX_OK 0
15 #define EX_USAGE 1
16 #else
17 #include <sysexits.h>
18 #endif
19 
20 #include "cmdline.h"
21 #include "config.h"
22 #include "exception_utils.h"
23 #include "exit_codes.h"
24 #include "signal_catcher.h"
25 #include "string_utils.h"
26 #include "version.h"
27 
29  const std::string &_optstring,
30  int argc,
31  const char **argv,
32  const std::string &program)
33  : parse_result(cmdline.parse(
34  argc,
35  argv,
36  (std::string("?h(help)") + _optstring).c_str())),
37  ui_message_handler(cmdline, program),
38  log(ui_message_handler)
39 {
40 }
41 
43 {
44 }
45 
47 {
48  log.error() << "Usage error!\n" << messaget::eom;
49  help();
50 }
51 
55 {
56  if(!cmdline.unknown_arg.empty())
57  {
58  log.error() << "Unknown option: " << cmdline.unknown_arg;
59  auto const suggestions =
61  if(!suggestions.empty())
62  {
63  log.error() << ", did you mean ";
64  if(suggestions.size() > 1)
65  {
66  log.error() << "one of ";
67  }
68  join_strings(log.error(), suggestions.begin(), suggestions.end(), ", ");
69  log.error() << "?";
70  }
71  log.error() << messaget::eom;
72  }
73 }
74 
76 {
77  // catch all exceptions here so that this code is not duplicated
78  // for each tool
79  try
80  {
81  if(parse_result)
82  {
83  usage_error();
85  return EX_USAGE;
86  }
87 
88  if(cmdline.isset('?') || cmdline.isset('h') || cmdline.isset("help"))
89  {
90  help();
91  return EX_OK;
92  }
93 
94  // install signal catcher
96 
97  return doit();
98  }
99 
100  // CPROVER style exceptions in order of decreasing happiness
102  {
103  log.error() << e.what() << messaget::eom;
105  }
106  catch(const cprover_exception_baset &e)
107  {
108  log.error() << e.what() << messaget::eom;
109  return CPROVER_EXIT_EXCEPTION;
110  }
111  catch(const std::string &e)
112  {
113  log.error() << "C++ string exception : " << e << messaget::eom;
114  return CPROVER_EXIT_EXCEPTION;
115  }
116  catch(const char *e)
117  {
118  log.error() << "C string exception : " << e << messaget::eom;
119  return CPROVER_EXIT_EXCEPTION;
120  }
121  catch(int e)
122  {
123  log.error() << "Numeric exception : " << e << messaget::eom;
124  return CPROVER_EXIT_EXCEPTION;
125  }
126  // C++ style exceptions
127  catch(const std::bad_alloc &)
128  {
129  log.error() << "Out of memory" << messaget::eom;
131  }
132  catch(const std::exception &e)
133  {
134  log.error() << e.what() << messaget::eom;
135  return CPROVER_EXIT_EXCEPTION;
136  }
137  catch(const invariant_failedt &e)
138  {
139  log.error() << e.what() << messaget::eom;
140  return CPROVER_EXIT_EXCEPTION;
141  }
142  catch(...)
143  {
144  log.error() << "Unknown exception type!" << messaget::eom;
145  return CPROVER_EXIT_EXCEPTION;
146  }
147 }
148 
150  const std::string &front_end)
151 {
152  log.status() << front_end << " version " << CBMC_VERSION << " "
153  << sizeof(void *) * CHAR_BIT << "-bit "
154  << config.this_architecture() << " "
156 }
157 
158 std::string align_center_with_border(const std::string &text)
159 {
160  auto const total_length = std::size_t{63};
161  auto const border = std::string{"* *"};
162  auto const fill =
163  total_length - std::min(total_length, 2 * border.size() + text.size());
164  auto const fill_right = fill / 2;
165  auto const fill_left = fill - fill_right;
166  return border + std::string(fill_left, ' ') + text +
167  std::string(fill_right, ' ') + border;
168 }
169 
170 std::string
171 banner_string(const std::string &front_end, const std::string &version)
172 {
173  const std::string version_str = front_end + " " + version + " " +
174  std::to_string(sizeof(void *) * CHAR_BIT) +
175  "-bit";
176 
177  return align_center_with_border(version_str);
178 }
configt config
Definition: config.cpp:25
std::string unknown_arg
Definition: cmdline.h:152
virtual bool isset(char option) const
Definition: cmdline.cpp:30
std::vector< std::string > get_argument_suggestions(const std::string &unknown_argument)
Definition: cmdline.cpp:210
static irep_idt this_architecture()
Definition: config.cpp:1361
static irep_idt this_operating_system()
Definition: config.cpp:1461
Base class for exceptions thrown in the cprover project.
Definition: c_errors.h:64
Thrown when users pass incorrect command line arguments, for example passing no files to analysis or ...
std::string what() const override
A human readable description of what went wrong.
A logic error, augmented with a distinguished field to hold a backtrace.
Definition: c_errors.h:28
mstreamt & error() const
Definition: message.h:399
mstreamt & status() const
Definition: message.h:414
static eomt eom
Definition: message.h:297
virtual int doit()=0
virtual void usage_error()
parse_options_baset(const std::string &optstring, int argc, const char **argv, const std::string &program)
void unknown_option_msg()
Print an error message mentioning the option that was not recognized when parsing the command line.
void log_version_and_architecture(const std::string &front_end)
Write version and system architecture to log.status().
virtual int main()
virtual void help()
Document and give macros for the exit codes of CPROVER binaries.
#define CPROVER_EXIT_INTERNAL_OUT_OF_MEMORY
Memory allocation has failed and this has been detected within the program.
Definition: exit_codes.h:52
#define CPROVER_EXIT_USAGE_ERROR
A usage error is returned when the command line is invalid or conflicting.
Definition: exit_codes.h:33
#define CPROVER_EXIT_EXCEPTION
An (unanticipated) exception was thrown during computation.
Definition: exit_codes.h:41
double log(double x)
Definition: math.c:2776
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)
void install_signal_catcher()
std::string to_string(const string_not_contains_constraintt &expr)
Used for debug printing.
Stream & join_strings(Stream &&os, const It b, const It e, const Delimiter &delimiter, TransformFunc &&transform_func)
Prints items to an stream, separated by a constant delimiter.
Definition: string_utils.h:61
const char * CBMC_VERSION