cprover
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/message.h>
26#include <util/parse_options.h>
27#include <util/version.h>
28
29#include "goto_cc_cmdline.h"
30
33 goto_cc_cmdlinet &_cmdline,
34 const std::string &_base_name,
35 message_handlert &_message_handler)
36 : cmdline(_cmdline), base_name(_base_name), message_handler(_message_handler)
37{
39}
40
43{
44}
45
48{
49 // clang-format off
50 std::cout << '\n' << banner_string("goto-cc", CBMC_VERSION) << '\n'
51 << align_center_with_border("Copyright (C) 2006-2018") << '\n'
52 << align_center_with_border("Daniel Kroening, Michael Tautschnig,") << '\n' // NOLINT(*)
53 << align_center_with_border("Christoph Wintersteiger") << '\n'
54 <<
55 "\n";
56
57 help_mode();
58
59 std::cout <<
60 "Usage: Purpose:\n"
61 "\n"
62 " --verbosity # verbosity level\n"
63 " --function name set entry point to name\n"
64 " --native-compiler cmd command to invoke as preprocessor/compiler\n"
65 " --native-linker cmd command to invoke as linker\n"
66 " --native-assembler cmd command to invoke as assembler (goto-as only)\n"
67 " --print-rejected-preprocessed-source file\n"
68 " copy failing (preprocessed) source to file\n"
69 " --object-bits number of bits used for object addresses\n"
70 "\n";
71 // clang-format on
72}
73
76int goto_cc_modet::main(int argc, const char **argv)
77{
78 if(cmdline.parse(argc, argv))
79 {
81 return EX_USAGE;
82 }
83
84 try
85 {
86 return doit();
87 }
88
89 catch(const char *e)
90 {
92 log.error() << e << messaget::eom;
93 return EX_SOFTWARE;
94 }
95
96 catch(const std::string &e)
97 {
99 log.error() << e << messaget::eom;
100 return EX_SOFTWARE;
101 }
102
103 catch(int)
104 {
105 return EX_SOFTWARE;
106 }
107
108 catch(const std::bad_alloc &)
109 {
111 log.error() << "Out of memory" << messaget::eom;
112 return EX_SOFTWARE;
113 }
114 catch(const cprover_exception_baset &e)
115 {
117 log.error() << e.what() << messaget::eom;
118 return EX_SOFTWARE;
119 }
120}
121
125{
126 std::cerr << "Usage error!\n\n";
127 help();
128}
Base class for exceptions thrown in the cprover project.
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
Class that provides messages with a built-in verbosity 'level'.
Definition message.h:155
static eomt eom
Definition message.h:297
Command line interpretation for goto-cc.
Command line interpretation for goto-cc.
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