CBMC
All Classes Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros Modules Pages
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 <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
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 }
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 {
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;
110 }
111 catch(const std::string &e)
112 {
113 log.error() << "C++ string exception : " << e << messaget::eom;
115 }
116 catch(const char *e)
117 {
118 log.error() << "C string exception : " << e << messaget::eom;
120 }
121 catch(int e)
122 {
123 log.error() << "Numeric exception : " << e << messaget::eom;
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;
136 }
137 catch(const invariant_failedt &e)
138 {
139 log.error() << e.what() << messaget::eom;
141 }
142 catch(...)
143 {
144 log.error() << "Unknown exception type!" << messaget::eom;
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
158std::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
170std::string
171banner_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
178}
configt config
Definition config.cpp:25
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition ai.h:562
std::string unknown_arg
Definition cmdline.h:155
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:220
static irep_idt this_architecture()
Definition config.cpp:1458
static irep_idt this_operating_system()
Definition config.cpp:1562
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:391
static eomt eom
Definition message.h:289
mstreamt & status() const
Definition message.h:406
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 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:2449
STL namespace.
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()
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.
const char * CBMC_VERSION