CBMC
Loading...
Searching...
No Matches
goto_diff_parse_options.h
Go to the documentation of this file.
1/*******************************************************************\
2
3Module: GOTO-DIFF Command Line Option Processing
4
5Author: Peter Schrammel
6
7\*******************************************************************/
8
11
12#ifndef CPROVER_GOTO_DIFF_GOTO_DIFF_PARSE_OPTIONS_H
13#define CPROVER_GOTO_DIFF_GOTO_DIFF_PARSE_OPTIONS_H
14
15#include <util/parse_options.h>
16#include <util/timestamper.h>
17#include <util/ui_message.h>
18
21
24
25class goto_modelt;
26class optionst;
27
28// clang-format off
29#define GOTO_DIFF_OPTIONS \
30 "(json-ui)" \
31 OPT_SHOW_GOTO_FUNCTIONS \
32 OPT_SHOW_PROPERTIES \
33 "(show-loops)" \
34 OPT_GOTO_CHECK \
35 OPT_COVER \
36 "(verbosity):(version)" \
37 OPT_FLUSH \
38 OPT_TIMESTAMP \
39 "u(unified)(change-impact)(forward-impact)(backward-impact)" \
40 "(compact-output)"
41// clang-format on
42
44{
45public:
46 int doit() override;
47 void help() override;
48
49 goto_diff_parse_optionst(int argc, const char **argv);
50
51protected:
52 void register_languages() override;
53
55
56 bool process_goto_program(const optionst &options, goto_modelt &goto_model);
57};
58
59#endif // CPROVER_GOTO_DIFF_GOTO_DIFF_PARSE_OPTIONS_H
int doit() override
invoke main modules
bool process_goto_program(const optionst &options, goto_modelt &goto_model)
void help() override
display command line help
void get_command_line_options(optionst &options)
Coverage Instrumentation.
Program Transformation.
Show the goto functions.
Show the properties.
Emit timestamps.