CBMC
Loading...
Searching...
No Matches
goto_cc_mode.cpp
Go to the documentation of this file.
1/*******************************************************************\
2
3Module: Command line option container
4
5Author: 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
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
35 const std::string &_base_name,
37 : cmdline(_cmdline), base_name(_base_name), message_handler(_message_handler)
38{
40}
41
46
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
82int goto_cc_modet::main(int argc, const char **argv)
83{
84 if(cmdline.parse(argc, argv))
85 {
87 return EX_USAGE;
88 }
89
90 try
91 {
92 return doit();
93 }
94
95 catch(const char *e)
96 {
98 log.error() << e << messaget::eom;
99 return EX_SOFTWARE;
100 }
101
102 catch(const std::string &e)
103 {
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 {
117 log.error() << "Out of memory" << messaget::eom;
118 return EX_SOFTWARE;
119 }
120
121 catch(const invalid_source_file_exceptiont &e)
122 {
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 {
132 log.error() << e.what() << messaget::eom;
133 return EX_SOFTWARE;
134 }
135}
136
139{
140 std::cerr << "Usage error!\n\n";
141 help();
142}
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition ai.h:562
Base class for exceptions thrown in the cprover project.
Definition c_errors.h:64
virtual bool parse(int argc, const char **argv)=0
~goto_cc_modet()
constructor
virtual int doit()=0
goto_cc_modet(goto_cc_cmdlinet &, const std::string &_base_name, message_handlert &)
constructor
goto_cc_cmdlinet & cmdline
virtual void help_mode()=0
message_handlert & message_handler
virtual void usage_error()
Prints a message informing the user about incorrect options.
void help()
display command line help
int main(int argc, const char **argv)
starts the compiler
Thrown when we can't handle something in an input source file.
Class that provides messages with a built-in verbosity 'level'.
Definition message.h:154
static eomt eom
Definition message.h:289
Command line interpretation for goto-cc.
Command line interpretation for goto-cc.
Help Formatter.
static help_formattert help_formatter(const std::string &s)
double log(double x)
Definition math.c:2449
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)
const char * CBMC_VERSION