cprover
Toggle main menu visibility
Loading...
Searching...
No Matches
goto_cc_mode.cpp
Go to the documentation of this file.
1
/*******************************************************************\
2
3
Module: Command line option container
4
5
Author: CM Wintersteiger, 2006
6
7
\*******************************************************************/
8
11
12
#include "
goto_cc_mode.h
"
13
14
#include <iostream>
15
16
#ifdef _WIN32
17
#define EX_OK 0
18
#define EX_USAGE 64
19
#define EX_SOFTWARE 70
20
#else
21
#include <sysexits.h>
22
#endif
23
24
#include <
util/exception_utils.h
>
25
#include <
util/help_formatter.h
>
26
#include <
util/message.h
>
27
#include <
util/parse_options.h
>
28
#include <
util/version.h
>
29
30
#include "
goto_cc_cmdline.h
"
31
33
goto_cc_modet::goto_cc_modet
(
34
goto_cc_cmdlinet
&_cmdline,
35
const
std::string &_base_name,
36
message_handlert
&_message_handler)
37
:
cmdline
(_cmdline),
base_name
(_base_name),
message_handler
(_message_handler)
38
{
39
register_languages
();
40
}
41
43
goto_cc_modet::~goto_cc_modet
()
44
{
45
}
46
48
void
goto_cc_modet::help
()
49
{
50
// clang-format off
51
std::cout <<
'\n'
<<
banner_string
(
"goto-cc"
,
CBMC_VERSION
) <<
'\n'
52
<<
align_center_with_border
(
"Copyright (C) 2006-2018"
) <<
'\n'
53
<<
align_center_with_border
(
"Daniel Kroening, Michael Tautschnig,"
) <<
'\n'
// NOLINT(*)
54
<<
align_center_with_border
(
"Christoph Wintersteiger"
) <<
'\n'
55
<<
56
"\n"
;
57
// clang-format on
58
59
help_mode
();
60
61
std::cout <<
help_formatter
(
62
"Usage: \tPurpose:\n"
63
"\n"
64
" {y--verbosity} {u#} \t verbosity level\n"
65
" {y--function} {uname} \t set entry point to name\n"
66
" {y--native-compiler} {ucmd} \t command to invoke as "
67
"preprocessor/compiler\n"
68
" {y--native-linker} {ucmd} \t command to invoke as linker\n"
69
" {y--native-assembler} {ucmd} \t command to invoke as assembler "
70
"(goto-as only)\n"
71
" {y--export-file-local-symbols} \t "
72
"name-mangle and export file-local symbols\n"
73
" {y--mangle-suffix} {usuffix} \t append suffix to exported file-local "
74
"symbols\n"
75
" {y--print-rejected-preprocessed-source} {ufile} \t "
76
"copy failing (preprocessed) source to file\n"
77
"\n"
);
78
}
79
82
int
goto_cc_modet::main
(
int
argc,
const
char
**argv)
83
{
84
if
(
cmdline
.parse(argc, argv))
85
{
86
usage_error
();
87
return
EX_USAGE;
88
}
89
90
try
91
{
92
return
doit
();
93
}
94
95
catch
(
const
char
*e)
96
{
97
messaget
log{
message_handler
};
98
log.
error
() << e <<
messaget::eom
;
99
return
EX_SOFTWARE;
100
}
101
102
catch
(
const
std::string &e)
103
{
104
messaget
log{
message_handler
};
105
log.
error
() << e <<
messaget::eom
;
106
return
EX_SOFTWARE;
107
}
108
109
catch
(
int
)
110
{
111
return
EX_SOFTWARE;
112
}
113
114
catch
(
const
std::bad_alloc &)
115
{
116
messaget
log{
message_handler
};
117
log.
error
() <<
"Out of memory"
<<
messaget::eom
;
118
return
EX_SOFTWARE;
119
}
120
121
catch
(
const
invalid_source_file_exceptiont
&e)
122
{
123
messaget
log{
message_handler
};
124
log.
error
().
source_location
= e.get_source_location();
125
log.
error
() << e.get_reason() <<
messaget::eom
;
126
return
EX_SOFTWARE;
127
}
128
129
catch
(
const
cprover_exception_baset
&e)
130
{
131
messaget
log{
message_handler
};
132
log.
error
() << e.what() <<
messaget::eom
;
133
return
EX_SOFTWARE;
134
}
135
}
136
138
void
goto_cc_modet::usage_error
()
139
{
140
std::cerr <<
"Usage error!\n\n"
;
141
help
();
142
}
cprover_exception_baset
Base class for exceptions thrown in the cprover project.
Definition
c_errors.h:64
goto_cc_cmdlinet
Definition
goto_cc_cmdline.h:20
goto_cc_modet::~goto_cc_modet
~goto_cc_modet()
constructor
Definition
goto_cc_mode.cpp:43
goto_cc_modet::doit
virtual int doit()=0
goto_cc_modet::goto_cc_modet
goto_cc_modet(goto_cc_cmdlinet &, const std::string &_base_name, message_handlert &)
constructor
Definition
goto_cc_mode.cpp:33
goto_cc_modet::cmdline
goto_cc_cmdlinet & cmdline
Definition
goto_cc_mode.h:38
goto_cc_modet::help_mode
virtual void help_mode()=0
goto_cc_modet::message_handler
message_handlert & message_handler
Definition
goto_cc_mode.h:40
goto_cc_modet::base_name
const std::string base_name
Definition
goto_cc_mode.h:39
goto_cc_modet::usage_error
virtual void usage_error()
Prints a message informing the user about incorrect options.
Definition
goto_cc_mode.cpp:138
goto_cc_modet::register_languages
void register_languages()
Definition
goto_cc_languages.cpp:19
goto_cc_modet::help
void help()
display command line help
Definition
goto_cc_mode.cpp:48
goto_cc_modet::main
int main(int argc, const char **argv)
starts the compiler
Definition
goto_cc_mode.cpp:82
invalid_source_file_exceptiont
Thrown when we can't handle something in an input source file.
Definition
exception_utils.h:172
message_handlert
Definition
message.h:27
messaget::mstreamt::source_location
source_locationt source_location
Definition
message.h:239
messaget
Class that provides messages with a built-in verbosity 'level'.
Definition
message.h:154
messaget::error
mstreamt & error() const
Definition
message.h:391
messaget::eom
static eomt eom
Definition
message.h:289
exception_utils.h
goto_cc_cmdline.h
Command line interpretation for goto-cc.
goto_cc_mode.h
Command line interpretation for goto-cc.
help_formatter.h
Help Formatter.
help_formatter
static help_formattert help_formatter(const std::string &s)
Definition
help_formatter.h:40
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:158
banner_string
std::string banner_string(const std::string &front_end, const std::string &version)
Definition
parse_options.cpp:171
parse_options.h
message.h
version.h
CBMC_VERSION
const char * CBMC_VERSION
goto-cc
goto_cc_mode.cpp
Generated by
1.17.0