CBMC
goto_diff_parse_options.h
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: GOTO-DIFF Command Line Option Processing
4 
5 Author: 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 
22 #include <ansi-c/goto_check_c.h>
23 #include <goto-instrument/cover.h>
24 
25 class goto_modelt;
26 class 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 {
45 public:
46  int doit() override;
47  void help() override;
48 
49  goto_diff_parse_optionst(int argc, const char **argv);
50 
51 protected:
52  void register_languages() override;
53 
54  void get_command_line_options(optionst &options);
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
goto_diff_parse_optionst(int argc, const char **argv)
void get_command_line_options(optionst &options)
Coverage Instrumentation.
Program Transformation.
Show the goto functions.
Show the properties.
Emit timestamps.