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>
23 
24 class goto_functionst;
25 class optionst;
26 
27 // clang-format off
28 #define CLOBBER_OPTIONS \
29  "(depth):(context-bound):(unwind):" \
30  OPT_GOTO_CHECK \
31  OPT_SHOW_GOTO_FUNCTIONS \
32  OPT_SHOW_PROPERTIES \
33  "(no-assertions)(no-assumptions)" \
34  "(error-label):(verbosity):(no-library)" \
35  "(version)" \
36  "(string-abstraction)" \
37  "(show-locs)(show-vcc)(show-trace)" \
38  "(property):" \
39 // clang-format on
40 
42  public parse_options_baset,
43  public language_uit
44 {
45 public:
46  virtual int doit();
47  virtual void help();
48 
49  clobber_parse_optionst(int argc, const char **argv);
51  int argc,
52  const char **argv,
53  const std::string &extra_options);
54 
55 protected:
57 
59 
61  const optionst &options,
62  goto_modelt &);
63 
65 
66  void report_success();
67  void report_failure();
68  void show_counterexample(const class goto_tracet &);
69 };
70 
71 #endif // CPROVER_CLOBBER_CLOBBER_PARSE_OPTIONS_H
void show_counterexample(const class goto_tracet &)
ui_message_handlert ui_message_handler
Show the goto functions.
bool set_properties(goto_functionst &)
virtual int doit()
invoke main modules
virtual void help()
display command line help
bool process_goto_program(const optionst &options, goto_modelt &)
Program Transformation.
void get_command_line_options(optionst &)
clobber_parse_optionst(int argc, const char **argv)
Show the properties.
TO_BE_DOCUMENTED.
Definition: goto_trace.h:152