cprover
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 <algorithm>
12 #include <cctype>
13 #include <climits>
14 #include <iostream>
15 
16 #if defined (_WIN32)
17 #define EX_OK 0
18 #define EX_USAGE 1
19 #else
20 #include <sysexits.h>
21 #endif
22 
23 #include "cmdline.h"
24 #include "exception_utils.h"
25 #include "exit_codes.h"
26 #include "signal_catcher.h"
27 #include "string_utils.h"
28 
30  const std::string &_optstring,
31  int argc,
32  const char **argv,
33  const std::string &program)
34  : parse_result(cmdline.parse(
35  argc,
36  argv,
37  (std::string("?h(help)") + _optstring).c_str())),
38  ui_message_handler(cmdline, program),
39  log(ui_message_handler)
40 {
41 }
42 
44 {
45 }
46 
48 {
49  log.error() << "Usage error!\n" << messaget::eom;
50  help();
51 }
52 
56 {
57  if(!cmdline.unknown_arg.empty())
58  {
59  log.error() << "Unknown option: " << cmdline.unknown_arg;
60  auto const suggestions =
62  if(!suggestions.empty())
63  {
64  log.error() << ", did you mean ";
65  if(suggestions.size() > 1)
66  {
67  log.error() << "one of ";
68  }
69  join_strings(log.error(), suggestions.begin(), suggestions.end(), ", ");
70  log.error() << "?";
71  }
72  log.error() << messaget::eom;
73  }
74 }
75 
77 {
78  // catch all exceptions here so that this code is not duplicated
79  // for each tool
80  try
81  {
82  if(parse_result)
83  {
84  usage_error();
86  return EX_USAGE;
87  }
88 
89  if(cmdline.isset('?') || cmdline.isset('h') || cmdline.isset("help"))
90  {
91  help();
92  return EX_OK;
93  }
94 
95  // install signal catcher
97 
98  return doit();
99  }
100 
101  // CPROVER style exceptions in order of decreasing happiness
103  {
104  log.error() << e.what() << messaget::eom;
106  }
107  catch(const cprover_exception_baset &e)
108  {
109  log.error() << e.what() << messaget::eom;
110  return CPROVER_EXIT_EXCEPTION;
111  }
112  catch(const std::string &e)
113  {
114  log.error() << "C++ string exception : " << e << messaget::eom;
115  return CPROVER_EXIT_EXCEPTION;
116  }
117  catch(const char *e)
118  {
119  log.error() << "C string exception : " << e << messaget::eom;
120  return CPROVER_EXIT_EXCEPTION;
121  }
122  catch(int e)
123  {
124  log.error() << "Numeric exception : " << e << messaget::eom;
125  return CPROVER_EXIT_EXCEPTION;
126  }
127  // C++ style exceptions
128  catch(const std::bad_alloc &)
129  {
130  log.error() << "Out of memory" << messaget::eom;
132  }
133  catch(const std::exception &e)
134  {
135  log.error() << e.what() << messaget::eom;
136  return CPROVER_EXIT_EXCEPTION;
137  }
138  catch(const invariant_failedt &e)
139  {
140  log.error() << e.what() << messaget::eom;
141  return CPROVER_EXIT_EXCEPTION;
142  }
143  catch(...)
144  {
145  log.error() << "Unknown exception type!" << messaget::eom;
146  return CPROVER_EXIT_EXCEPTION;
147  }
148 }
149 
150 std::string align_center_with_border(const std::string &text)
151 {
152  auto const total_length = std::size_t{63};
153  auto const border = std::string{"* *"};
154  auto const fill =
155  total_length - std::min(total_length, 2 * border.size() + text.size());
156  auto const fill_right = fill / 2;
157  auto const fill_left = fill - fill_right;
158  return border + std::string(fill_left, ' ') + text +
159  std::string(fill_right, ' ') + border;
160 }
161 
162 std::string
163 banner_string(const std::string &front_end, const std::string &version)
164 {
165  const std::string version_str = front_end + " " + version + " " +
166  std::to_string(sizeof(void *) * CHAR_BIT) +
167  "-bit";
168 
169  return align_center_with_border(version_str);
170 }
171 
172 std::string help_entry(
173  const std::string &option,
174  const std::string &description,
175  const std::size_t left_margin,
176  const std::size_t width)
177 {
178  PRECONDITION(!option.empty());
179  PRECONDITION(!std::isspace(option.front()));
180  PRECONDITION(!std::isspace(option.back()));
181  PRECONDITION(option.length() <= width);
182 
183  PRECONDITION(!description.empty());
184  PRECONDITION(!std::isspace(description.front()));
185  PRECONDITION(!std::isspace(description.back()));
186 
187  PRECONDITION(left_margin < width);
188 
189  std::string result;
190 
191  if(option.length() >= left_margin - 1)
192  {
193  result = " " + option + "\n";
194  result += wrap_line(description, left_margin, width) + "\n";
195 
196  return result;
197  }
198 
199  std::string padding(left_margin - option.length() - 1, ' ');
200  result = " " + option + padding;
201 
202  if(description.length() <= (width - left_margin))
203  {
204  return result + description + "\n";
205  }
206 
207  auto it = description.cbegin() + (width - left_margin);
208  auto rit = std::reverse_iterator<decltype(it)>(it) - 1;
209 
210  auto rit_space = std::find(rit, description.crend(), ' ');
211  auto it_space = rit_space.base() - 1;
212  CHECK_RETURN(*it_space == ' ');
213 
214  result.append(description.cbegin(), it_space);
215  result.append("\n");
216 
217  result +=
218  wrap_line(it_space + 1, description.cend(), left_margin, width) + "\n";
219 
220  return result;
221 }
std::string unknown_arg
Definition: cmdline.h:144
virtual bool isset(char option) const
Definition: cmdline.cpp:29
std::vector< std::string > get_argument_suggestions(const std::string &unknown_argument)
Definition: cmdline.cpp:211
Base class for exceptions thrown in the cprover project.
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: invariant.h:111
mstreamt & error() const
Definition: message.h:399
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.
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
std::string help_entry(const std::string &option, const std::string &description, const std::size_t left_margin, const std::size_t width)
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()
#define CHECK_RETURN(CONDITION)
Definition: invariant.h:496
#define PRECONDITION(CONDITION)
Definition: invariant.h:464
std::string to_string(const string_not_contains_constraintt &expr)
Used for debug printing.
std::string wrap_line(const std::string &line, const std::size_t left_margin, const std::size_t width)
Wrap line at spaces to not extend past the right margin, and include given padding with spaces to the...
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:62