cprover
parse_options.cpp
Go to the documentation of this file.
1/*******************************************************************\
2
3Module:
4
5Author: 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 "config.h"
25#include "exception_utils.h"
26#include "exit_codes.h"
27#include "signal_catcher.h"
28#include "string_utils.h"
29#include "version.h"
30
32 const std::string &_optstring,
33 int argc,
34 const char **argv,
35 const std::string &program)
36 : parse_result(cmdline.parse(
37 argc,
38 argv,
39 (std::string("?h(help)") + _optstring).c_str())),
40 ui_message_handler(cmdline, program),
41 log(ui_message_handler)
42{
43}
44
46{
47}
48
50{
51 log.error() << "Usage error!\n" << messaget::eom;
52 help();
53}
54
58{
59 if(!cmdline.unknown_arg.empty())
60 {
61 log.error() << "Unknown option: " << cmdline.unknown_arg;
62 auto const suggestions =
64 if(!suggestions.empty())
65 {
66 log.error() << ", did you mean ";
67 if(suggestions.size() > 1)
68 {
69 log.error() << "one of ";
70 }
71 join_strings(log.error(), suggestions.begin(), suggestions.end(), ", ");
72 log.error() << "?";
73 }
75 }
76}
77
79{
80 // catch all exceptions here so that this code is not duplicated
81 // for each tool
82 try
83 {
84 if(parse_result)
85 {
88 return EX_USAGE;
89 }
90
91 if(cmdline.isset('?') || cmdline.isset('h') || cmdline.isset("help"))
92 {
93 help();
94 return EX_OK;
95 }
96
97 // install signal catcher
99
100 return doit();
101 }
102
103 // CPROVER style exceptions in order of decreasing happiness
105 {
106 log.error() << e.what() << messaget::eom;
108 }
109 catch(const cprover_exception_baset &e)
110 {
111 log.error() << e.what() << messaget::eom;
113 }
114 catch(const std::string &e)
115 {
116 log.error() << "C++ string exception : " << e << messaget::eom;
118 }
119 catch(const char *e)
120 {
121 log.error() << "C string exception : " << e << messaget::eom;
123 }
124 catch(int e)
125 {
126 log.error() << "Numeric exception : " << e << messaget::eom;
128 }
129 // C++ style exceptions
130 catch(const std::bad_alloc &)
131 {
132 log.error() << "Out of memory" << messaget::eom;
134 }
135 catch(const std::exception &e)
136 {
137 log.error() << e.what() << messaget::eom;
139 }
140 catch(const invariant_failedt &e)
141 {
142 log.error() << e.what() << messaget::eom;
144 }
145 catch(...)
146 {
147 log.error() << "Unknown exception type!" << messaget::eom;
149 }
150}
151
153 const std::string &front_end)
154{
155 log.status() << front_end << " version " << CBMC_VERSION << " "
156 << sizeof(void *) * CHAR_BIT << "-bit "
157 << config.this_architecture() << " "
159}
160
161std::string align_center_with_border(const std::string &text)
162{
163 auto const total_length = std::size_t{63};
164 auto const border = std::string{"* *"};
165 auto const fill =
166 total_length - std::min(total_length, 2 * border.size() + text.size());
167 auto const fill_right = fill / 2;
168 auto const fill_left = fill - fill_right;
169 return border + std::string(fill_left, ' ') + text +
170 std::string(fill_right, ' ') + border;
171}
172
173std::string
174banner_string(const std::string &front_end, const std::string &version)
175{
176 const std::string version_str = front_end + " " + version + " " +
177 std::to_string(sizeof(void *) * CHAR_BIT) +
178 "-bit";
179
180 return align_center_with_border(version_str);
181}
182
183std::string help_entry(
184 const std::string &option,
185 const std::string &description,
186 const std::size_t left_margin,
187 const std::size_t width)
188{
189 PRECONDITION(!option.empty());
190 PRECONDITION(!std::isspace(option.front()));
191 PRECONDITION(!std::isspace(option.back()));
192 PRECONDITION(option.length() <= width);
193
194 PRECONDITION(!description.empty());
195 PRECONDITION(!std::isspace(description.front()));
196 PRECONDITION(!std::isspace(description.back()));
197
198 PRECONDITION(left_margin < width);
199
200 std::string result;
201
202 if(option.length() >= left_margin - 1)
203 {
204 result = " " + option + "\n";
205 result += wrap_line(description, left_margin, width) + "\n";
206
207 return result;
208 }
209
210 std::string padding(left_margin - option.length() - 1, ' ');
211 result = " " + option + padding;
212
213 if(description.length() <= (width - left_margin))
214 {
215 return result + description + "\n";
216 }
217
218 auto it = description.cbegin() + (width - left_margin);
219 auto rit = std::reverse_iterator<decltype(it)>(it) - 1;
220
221 auto rit_space = std::find(rit, description.crend(), ' ');
222 auto it_space = rit_space.base() - 1;
223 CHECK_RETURN(*it_space == ' ');
224
225 result.append(description.cbegin(), it_space);
226 result.append("\n");
227
228 result +=
229 wrap_line(it_space + 1, description.cend(), left_margin, width) + "\n";
230
231 return result;
232}
std::string unknown_arg
Definition: cmdline.h:146
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:1350
static irep_idt this_operating_system()
Definition: config.cpp:1450
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:110
mstreamt & error() const
Definition: message.h:399
static eomt eom
Definition: message.h:297
mstreamt & status() const
Definition: message.h:414
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()
configt config
Definition: config.cpp:25
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
STL namespace.
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:495
#define PRECONDITION(CONDITION)
Definition: invariant.h:463
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
const char * CBMC_VERSION