12 #ifndef CPROVER_MUSKETEER_MUSKETEER_PARSE_OPTIONS_H 13 #define CPROVER_MUSKETEER_MUSKETEER_PARSE_OPTIONS_H 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)" 59 #endif // CPROVER_MUSKETEER_MUSKETEER_PARSE_OPTIONS_H
void instrument_goto_program(goto_functionst &goto_functions)
virtual void register_languages()
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
ui_message_handlert ui_message_handler