cprover
clobber_parse_options.h
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: Command Line Parsing
4 
5 Author: Daniel Kroening, kroening@kroening.com
6 
7 \*******************************************************************/
8 
11 
12 #ifndef CPROVER_CLOBBER_CLOBBER_PARSE_OPTIONS_H
13 #define CPROVER_CLOBBER_CLOBBER_PARSE_OPTIONS_H
14 
15 #include <util/ui_message.h>
16 #include <util/parse_options.h>
17 
18 #include <langapi/language_ui.h>
19 
20 #include <analyses/goto_check.h>
22 
23 class goto_functionst;
24 class optionst;
25 
26 #define CLOBBER_OPTIONS \
27  "(depth):(context-bound):(unwind):" \
28  OPT_GOTO_CHECK \
29  OPT_SHOW_GOTO_FUNCTIONS \
30  "(no-assertions)(no-assumptions)" \
31  "(error-label):(verbosity):(no-library)" \
32  "(version)" \
33  "(string-abstraction)" \
34  "(show-locs)(show-vcc)(show-properties)(show-trace)" \
35  "(property):"
36 
38  public parse_options_baset,
39  public language_uit
40 {
41 public:
42  virtual int doit();
43  virtual void help();
44 
45  clobber_parse_optionst(int argc, const char **argv);
47  int argc,
48  const char **argv,
49  const std::string &extra_options);
50 
51 protected:
53 
54  void get_command_line_options(optionst &options);
55 
56  bool get_goto_program(
57  const optionst &options,
58  goto_functionst &goto_functions);
59 
61  const optionst &options,
62  goto_functionst &goto_functions);
63 
64  bool set_properties(goto_functionst &goto_functions);
65 
66  void report_success();
67  void report_failure();
68  void show_counterexample(const class goto_tracet &);
69 
70  void eval_verbosity();
71 };
72 
73 #endif // CPROVER_CLOBBER_CLOBBER_PARSE_OPTIONS_H
bool set_properties(goto_functionst &goto_functions)
void show_counterexample(const class goto_tracet &)
ui_message_handlert ui_message_handler
Show the goto functions.
virtual int doit()
invoke main modules
virtual void help()
display command line help
Program Transformation.
bool get_goto_program(const optionst &options, goto_functionst &goto_functions)
bool process_goto_program(const optionst &options, goto_functionst &goto_functions)
clobber_parse_optionst(int argc, const char **argv)
TO_BE_DOCUMENTED.
Definition: goto_trace.h:146
void get_command_line_options(optionst &options)