12 #ifndef CPROVER_SYMEX_SYMEX_PARSE_OPTIONS_H 13 #define CPROVER_SYMEX_SYMEX_PARSE_OPTIONS_H 30 #define SYMEX_OPTIONS \ 33 "(depth):(context-bound):(branch-bound):(unwind):(max-search-time):" \ 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)" \ 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)" 82 #endif // CPROVER_SYMEX_SYMEX_PARSE_OPTIONS_H
void report_cover(const path_searcht::property_mapt &)
std::map< irep_idt, property_entryt > property_mapt
bool process_goto_program(const optionst &options)
virtual void help()
display command line help
ui_message_handlert ui_message_handler
void get_command_line_options(optionst &options)
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)
virtual int doit()
invoke main modules
void show_counterexample(const class goto_tracet &)