9#ifndef CPROVER_GOTO_SYNTHESIZER_GOTO_SYNTHESIZER_PARSE_OPTIONS_H
10#define CPROVER_GOTO_SYNTHESIZER_GOTO_SYNTHESIZER_PARSE_OPTIONS_H
24#define GOTO_SYNTHESIZER_OPTIONS \
25 OPT_DUMP_LOOP_CONTRACTS \
26 "(" FLAG_LOOP_CONTRACTS_NO_UNWIND ")" \
29 "(arrays-uf-always)(arrays-uf-never)" \
30 "(verbosity):(version)(xml-ui)(json-ui)" \
void help() override
display command line help
goto_synthesizer_parse_optionst(int argc, const char **argv)
void register_languages() override
int doit() override
invoke main modules
parse_options_baset(const std::string &optstring, int argc, const char **argv, const std::string &program)
Verify and use annotated invariants and pre/post-conditions.
Dump Loop Contracts as JSON.