-
Notifications
You must be signed in to change notification settings - Fork 273
/
Copy pathgoto_cc_mode.cpp
142 lines (119 loc) · 3.26 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
141
142
/*******************************************************************\
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/help_formatter.h>
#include <util/message.h>
#include <util/parse_options.h>
#include <util/version.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";
// clang-format on
help_mode();
std::cout << help_formatter(
"Usage: \tPurpose:\n"
"\n"
" {y--verbosity} {u#} \t verbosity level\n"
" {y--function} {uname} \t set entry point to name\n"
" {y--native-compiler} {ucmd} \t command to invoke as "
"preprocessor/compiler\n"
" {y--native-linker} {ucmd} \t command to invoke as linker\n"
" {y--native-assembler} {ucmd} \t command to invoke as assembler "
"(goto-as only)\n"
" {y--export-file-local-symbols} \t "
"name-mangle and export file-local symbols\n"
" {y--mangle-suffix} {usuffix} \t append suffix to exported file-local "
"symbols\n"
" {y--print-rejected-preprocessed-source} {ufile} \t "
"copy failing (preprocessed) source to file\n"
"\n");
}
/// 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();
}