cprover
symex_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_SYMEX_SYMEX_PARSE_OPTIONS_H
13 #define CPROVER_SYMEX_SYMEX_PARSE_OPTIONS_H
14 
15 #include <util/ui_message.h>
16 #include <util/parse_options.h>
17 
20 
21 #include <langapi/language_ui.h>
22 
23 #include <analyses/goto_check.h>
24 
25 #include "path_search.h"
26 
27 class goto_functionst;
28 class optionst;
29 
30 #define SYMEX_OPTIONS \
31  "(function):" \
32  "D:I:" \
33  "(depth):(context-bound):(branch-bound):(unwind):(max-search-time):" \
34  OPT_GOTO_CHECK \
35  "(no-assertions)(no-assumptions)" \
36  "(16)(32)(64)(LP64)(ILP64)(LLP64)(ILP32)(LP32)" \
37  "(little-endian)(big-endian)" \
38  "(error-label):(verbosity):(no-library)" \
39  "(version)" \
40  "(bfs)(dfs)(locs)" \
41  "(cover):" \
42  "(i386-linux)(i386-macos)(i386-win32)(win32)(winx64)(gcc)" \
43  "(ppc-macos)(unsigned-char)" \
44  "(string-abstraction)(no-arch)(arch):(floatbv)(fixedbv)" \
45  "(round-to-nearest)(round-to-plus-inf)(round-to-minus-inf)(round-to-zero)" \
46  "(show-locs)(show-vcc)(show-properties)" \
47  "(drop-unused-functions)" \
48  OPT_SHOW_GOTO_FUNCTIONS \
49  "(property):(trace)(show-trace)(stop-on-fail)(eager-infeasibility)" \
50  "(no-simplify)(no-unwinding-assertions)(no-propagation)"
51  // the last line is for CBMC-regression testing only
52 
54  public parse_options_baset,
55  public language_uit
56 {
57 public:
58  virtual int doit();
59  virtual void help();
60 
61  symex_parse_optionst(int argc, const char **argv);
62 
63 protected:
66 
67  void get_command_line_options(optionst &options);
68  bool process_goto_program(const optionst &options);
69  bool set_properties();
70 
71  void report_success();
72  void report_failure();
75  void show_counterexample(const class goto_tracet &);
76 
77  void eval_verbosity();
78 
79  std::string get_test(const goto_tracet &goto_trace);
80 };
81 
82 #endif // CPROVER_SYMEX_SYMEX_PARSE_OPTIONS_H
void report_cover(const path_searcht::property_mapt &)
Definition: symex_cover.cpp:46
std::map< irep_idt, property_entryt > property_mapt
Definition: path_search.h:102
Show the goto functions.
bool process_goto_program(const optionst &options)
virtual void help()
display command line help
ui_message_handlert ui_message_handler
Symbol Table + CFG.
void get_command_line_options(optionst &options)
Program Transformation.
void report_properties(const path_searcht::property_mapt &)
symex_parse_optionst(int argc, const char **argv)
Path-based Symbolic Execution.
std::string get_test(const goto_tracet &goto_trace)
Definition: symex_cover.cpp:22
virtual int doit()
invoke main modules
TO_BE_DOCUMENTED.
Definition: goto_trace.h:146
void show_counterexample(const class goto_tracet &)