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 <climits>
13 #include <iostream>
14 
15 #if defined (_WIN32)
16 #define EX_OK 0
17 #define EX_USAGE 1
18 #else
19 #include <sysexits.h>
20 #endif
21 
22 #include "cmdline.h"
23 #include "exception_utils.h"
24 #include "exit_codes.h"
25 #include "signal_catcher.h"
26 
28  const std::string &_optstring,
29  int argc,
30  const char **argv,
31  const std::string &program)
32  : parse_result(cmdline.parse(
33  argc,
34  argv,
35  (std::string("?h(help)") + _optstring).c_str())),
36  ui_message_handler(cmdline, program),
37  log(ui_message_handler)
38 {
39 }
40 
42 {
43 }
44 
46 {
47  log.error() << "Usage error!\n" << messaget::eom;
48  help();
49 }
50 
54 {
55  if(!cmdline.unknown_arg.empty())
56  log.error() << "Unknown option: " << cmdline.unknown_arg << messaget::eom;
57 }
58 
60 {
61  // catch all exceptions here so that this code is not duplicated
62  // for each tool
63  try
64  {
65  if(parse_result)
66  {
67  usage_error();
69  return EX_USAGE;
70  }
71 
72  if(cmdline.isset('?') || cmdline.isset('h') || cmdline.isset("help"))
73  {
74  help();
75  return EX_OK;
76  }
77 
78  // install signal catcher
80 
81  return doit();
82  }
83 
84  // CPROVER style exceptions in order of decreasing happiness
86  {
87  log.error() << e.what() << messaget::eom;
89  }
90  catch(const cprover_exception_baset &e)
91  {
92  log.error() << e.what() << messaget::eom;
94  }
95  catch(const std::string &e)
96  {
97  log.error() << "C++ string exception : " << e << messaget::eom;
99  }
100  catch(const char *e)
101  {
102  log.error() << "C string exception : " << e << messaget::eom;
103  return CPROVER_EXIT_EXCEPTION;
104  }
105  catch(int e)
106  {
107  log.error() << "Numeric exception : " << e << messaget::eom;
108  return CPROVER_EXIT_EXCEPTION;
109  }
110  // C++ style exceptions
111  catch(const std::bad_alloc &)
112  {
113  log.error() << "Out of memory" << messaget::eom;
115  }
116  catch(const std::exception &e)
117  {
118  log.error() << e.what() << messaget::eom;
119  return CPROVER_EXIT_EXCEPTION;
120  }
121  catch(const invariant_failedt &e)
122  {
123  log.error() << e.what() << messaget::eom;
124  return CPROVER_EXIT_EXCEPTION;
125  }
126  catch(...)
127  {
128  log.error() << "Unknown exception type!" << messaget::eom;
129  return CPROVER_EXIT_EXCEPTION;
130  }
131 }
132 
133 std::string align_center_with_border(const std::string &text)
134 {
135  auto const total_length = std::size_t{63};
136  auto const border = std::string{"* *"};
137  auto const fill =
138  total_length - std::min(total_length, 2 * border.size() + text.size());
139  auto const fill_right = fill / 2;
140  auto const fill_left = fill - fill_right;
141  return border + std::string(fill_left, ' ') + text +
142  std::string(fill_right, ' ') + border;
143 }
144 
145 std::string
146 banner_string(const std::string &front_end, const std::string &version)
147 {
148  const std::string version_str = front_end + " " + version + " " +
149  std::to_string(sizeof(void *) * CHAR_BIT) +
150  "-bit";
151 
152  return align_center_with_border(version_str);
153 }
exception_utils.h
cmdlinet::isset
virtual bool isset(char option) const
Definition: cmdline.cpp:28
parse_options_baset::unknown_option_msg
void unknown_option_msg()
Print an error message mentioning the option that was not recognized when parsing the command line.
Definition: parse_options.cpp:53
CPROVER_EXIT_INTERNAL_OUT_OF_MEMORY
#define CPROVER_EXIT_INTERNAL_OUT_OF_MEMORY
Memory allocation has failed and this has been detected within the program.
Definition: exit_codes.h:52
invariant_failedt
A logic error, augmented with a distinguished field to hold a backtrace.
Definition: invariant.h:111
CPROVER_EXIT_EXCEPTION
#define CPROVER_EXIT_EXCEPTION
An (unanticipated) exception was thrown during computation.
Definition: exit_codes.h:41
to_string
std::string to_string(const string_not_contains_constraintt &expr)
Used for debug printing.
Definition: string_constraint.cpp:55
messaget::eom
static eomt eom
Definition: message.h:283
parse_options_baset::usage_error
virtual void usage_error()
Definition: parse_options.cpp:45
invalid_command_line_argument_exceptiont::what
std::string what() const override
A human readable description of what went wrong.
Definition: exception_utils.cpp:12
messaget::error
mstreamt & error() const
Definition: message.h:385
banner_string
std::string banner_string(const std::string &front_end, const std::string &version)
Definition: parse_options.cpp:146
cprover_exception_baset::what
virtual std::string what() const =0
A human readable description of what went wrong.
cmdlinet::unknown_arg
std::string unknown_arg
Definition: cmdline.h:86
parse_options.h
parse_options_baset::main
virtual int main()
Definition: parse_options.cpp:59
parse_options_baset::parse_options_baset
parse_options_baset(const std::string &optstring, int argc, const char **argv, const std::string &program)
Definition: parse_options.cpp:27
parse_options_baset::log
messaget log
Definition: parse_options.h:43
install_signal_catcher
void install_signal_catcher()
Definition: signal_catcher.cpp:40
cmdline.h
parse_options_baset::doit
virtual int doit()=0
exit_codes.h
CPROVER_EXIT_USAGE_ERROR
#define CPROVER_EXIT_USAGE_ERROR
A usage error is returned when the command line is invalid or conflicting.
Definition: exit_codes.h:33
invariant_failedt::what
virtual std::string what() const noexcept
Definition: invariant.cpp:118
signal_catcher.h
parse_options_baset::help
virtual void help()
Definition: parse_options.cpp:41
parse_options_baset::parse_result
bool parse_result
Definition: parse_options.h:39
invalid_command_line_argument_exceptiont
Thrown when users pass incorrect command line arguments, for example passing no files to analysis or ...
Definition: exception_utils.h:38
parse_options_baset::cmdline
cmdlinet cmdline
Definition: parse_options.h:28
align_center_with_border
std::string align_center_with_border(const std::string &text)
Utility for displaying help centered messages borderered by "* *".
Definition: parse_options.cpp:133
cprover_exception_baset
Base class for exceptions thrown in the cprover project.
Definition: exception_utils.h:25