forked from diffblue/cbmc
-
Notifications
You must be signed in to change notification settings - Fork 0
/
Copy pathgoto_cc_mode.cpp
140 lines (116 loc) · 3.28 KB
/
goto_cc_mode.cpp
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
/*******************************************************************\
Module: Command line option container
Author: CM Wintersteiger, 2006
\*******************************************************************/
/// \file
/// Command line option container
#include "goto_cc_mode.h"
#include <iostream>
#ifdef _WIN32
#define EX_OK 0
#define EX_USAGE 64
#define EX_SOFTWARE 70
#else
#include <sysexits.h>
#endif
#include <util/exception_utils.h>
#include <util/message.h>
#include <util/version.h>
#include <cli-utils/parse_options.h>
#include "goto_cc_cmdline.h"
/// constructor
goto_cc_modet::goto_cc_modet(
goto_cc_cmdlinet &_cmdline,
const std::string &_base_name,
message_handlert &_message_handler)
: cmdline(_cmdline), base_name(_base_name), message_handler(_message_handler)
{
register_languages();
}
/// constructor
goto_cc_modet::~goto_cc_modet()
{
}
/// display command line help
void goto_cc_modet::help()
{
// clang-format off
std::cout << '\n' << banner_string("goto-cc", CBMC_VERSION) << '\n'
<< align_center_with_border("Copyright (C) 2006-2018") << '\n'
<< align_center_with_border("Daniel Kroening, Michael Tautschnig,") << '\n' // NOLINT(*)
<< align_center_with_border("Christoph Wintersteiger") << '\n'
<<
"\n";
help_mode();
std::cout <<
"Usage: Purpose:\n"
"\n"
" --verbosity # verbosity level\n"
" --function name set entry point to name\n"
" --native-compiler cmd command to invoke as preprocessor/compiler\n"
" --native-linker cmd command to invoke as linker\n"
" --native-assembler cmd command to invoke as assembler (goto-as only)\n"
" --export-file-local-symbols\n"
" name-mangle and export file-local symbols\n"
" --mangle-suffix suffix append suffix to exported file-local symbols\n"
" --print-rejected-preprocessed-source file\n"
" copy failing (preprocessed) source to file\n"
" --object-bits number of bits used for object addresses\n"
"\n";
// clang-format on
}
/// starts the compiler
/// \return error code
int goto_cc_modet::main(int argc, const char **argv)
{
if(cmdline.parse(argc, argv))
{
usage_error();
return EX_USAGE;
}
try
{
return doit();
}
catch(const char *e)
{
messaget log{message_handler};
log.error() << e << messaget::eom;
return EX_SOFTWARE;
}
catch(const std::string &e)
{
messaget log{message_handler};
log.error() << e << messaget::eom;
return EX_SOFTWARE;
}
catch(int)
{
return EX_SOFTWARE;
}
catch(const std::bad_alloc &)
{
messaget log{message_handler};
log.error() << "Out of memory" << messaget::eom;
return EX_SOFTWARE;
}
catch(const invalid_source_file_exceptiont &e)
{
messaget log{message_handler};
log.error().source_location = e.get_source_location();
log.error() << e.get_reason() << messaget::eom;
return EX_SOFTWARE;
}
catch(const cprover_exception_baset &e)
{
messaget log{message_handler};
log.error() << e.what() << messaget::eom;
return EX_SOFTWARE;
}
}
/// Prints a message informing the user about incorrect options.
void goto_cc_modet::usage_error()
{
std::cerr << "Usage error!\n\n";
help();
}