cprover
musketeer_parse_options.h
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: Command Line Parsing
4 
5 Author:
6 
7 \*******************************************************************/
8 
11 
12 #ifndef CPROVER_MUSKETEER_MUSKETEER_PARSE_OPTIONS_H
13 #define CPROVER_MUSKETEER_MUSKETEER_PARSE_OPTIONS_H
14 
15 #include <util/ui_message.h>
16 #include <util/parse_options.h>
17 
18 #include <langapi/language_ui.h>
20 
21 #define GOTO_FENCE_INSERTER_OPTIONS \
22  "(scc)(one-event-per-cycle)(verbosity):" \
23  "(mm):(my-events)(unwind):" \
24  "(max-var):(max-po-trans):(ignore-arrays)(remove-function-pointers)" \
25  "(cfg-kill)(no-dependencies)(force-loop-duplication)(no-loop-duplication)" \
26  "(no-po-rendering)(render-cluster-file)(render-cluster-function)" \
27  "(cav11)(version)(const-function-pointer-propagation)(print-graph)" \
28  "(volatile)(all-shared)(pensieve)(naive)(all-shared-aeg)(async)(userdef)"
29 
31  public parse_options_baset,
32  public language_uit
33 {
34 public:
35  virtual int doit();
36  virtual void help();
37 
38  goto_fence_inserter_parse_optionst(int argc, const char **argv):
41  ui_message_handler(cmdline, "musketeer")
42  {
43  }
44 
45 protected:
47 
48  virtual void register_languages();
49 
50  void get_goto_program(
51  goto_functionst &goto_functions);
52 
54  goto_functionst &goto_functions);
55 
56  void set_verbosity();
57 };
58 
59 #endif // CPROVER_MUSKETEER_MUSKETEER_PARSE_OPTIONS_H
void instrument_goto_program(goto_functionst &goto_functions)
Goto Programs with Functions.
goto_fence_inserter_parse_optionst(int argc, const char **argv)
#define GOTO_FENCE_INSERTER_OPTIONS
virtual int doit()
invoke main modules
void get_goto_program(goto_functionst &goto_functions)
virtual void help()
display command line help