CBMC
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 
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 {
40 }
41 
44 {
45 }
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 
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  {
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 }
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
Definition: goto_cc_mode.h:38
virtual void help_mode()=0
message_handlert & message_handler
Definition: goto_cc_mode.h:40
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:2776
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