cprover
Loading...
Searching...
No Matches
cbmc_parse_options.h
Go to the documentation of this file.
1/*******************************************************************\
2
3Module: CBMC Command Line Option Processing
4
5Author: Daniel Kroening, kroening@kroening.com
6
7\*******************************************************************/
8
11
12#ifndef CPROVER_CBMC_CBMC_PARSE_OPTIONS_H
13#define CPROVER_CBMC_CBMC_PARSE_OPTIONS_H
14
15#include <util/parse_options.h>
16#include <util/timestamper.h>
17#include <util/ui_message.h>
19
22
24#include <ansi-c/goto_check_c.h>
27#include <json/json_interface.h>
28#include <langapi/language.h>
31
32class optionst;
33
34// clang-format off
35#define CBMC_OPTIONS \
36 OPT_BMC \
37 "(preprocess)(slice-by-trace):" \
38 OPT_FUNCTIONS \
39 "(no-simplify)(full-slice)" \
40 OPT_REACHABILITY_SLICER \
41 "(no-propagation)(no-simplify-if)" \
42 "(document-subgoals)(test-preprocessor)" \
43 "(show-array-constraints)" \
44 OPT_CONFIG_C_CPP \
45 OPT_CONFIG_PLATFORM \
46 OPT_CONFIG_BACKEND \
47 OPT_CONFIG_LIBRARY \
48 OPT_GOTO_CHECK \
49 OPT_XML_INTERFACE \
50 OPT_JSON_INTERFACE \
51 OPT_SOLVER \
52 OPT_STRING_REFINEMENT_CBMC \
53 OPT_SHOW_GOTO_FUNCTIONS \
54 OPT_SHOW_PROPERTIES \
55 "(show-symbol-table)(show-parse-tree)" \
56 "(drop-unused-functions)" \
57 "(havoc-undefined-functions)" \
58 "(property):(stop-on-fail)(trace)" \
59 "(verbosity):(no-library)" \
60 "(nondet-static)" \
61 "(version)" \
62 "(export-symex-ready-goto):" \
63 OPT_COVER \
64 "(symex-coverage-report):" \
65 "(mm):" \
66 OPT_TIMESTAMP \
67 "(arrays-uf-always)(arrays-uf-never)" \
68 OPT_FLUSH \
69 "(localize-faults)" \
70 OPT_GOTO_TRACE \
71 OPT_VALIDATE \
72 OPT_ANSI_C_LANGUAGE \
73 "(claim):(show-claims)(floatbv)(all-claims)(all-properties)" // legacy, and will eventually disappear // NOLINT(whitespace/line_length)
74// clang-format on
75
77{
78public:
79 virtual int doit() override;
80 virtual void help() override;
81
82 cbmc_parse_optionst(int argc, const char **argv);
84 int argc,
85 const char **argv,
86 const std::string &extra_options);
87
92 static void set_default_options(optionst &);
93
94 static bool process_goto_program(goto_modelt &, const optionst &, messaget &);
95
96 static int get_goto_program(
98 const optionst &,
99 const cmdlinet &,
101
102protected:
104
105 void register_languages() override;
107 void preprocessing(const optionst &);
108 bool set_properties();
109};
110
111#endif // CPROVER_CBMC_CBMC_PARSE_OPTIONS_H
Bounded Model Checking Utilities.
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition ai.h:563
virtual int doit() override
invoke main modules
static bool process_goto_program(goto_modelt &, const optionst &, messaget &)
static void set_default_options(optionst &)
Set the options that have default values.
static int get_goto_program(goto_modelt &, const optionst &, const cmdlinet &, ui_message_handlert &)
void get_command_line_options(optionst &)
void register_languages() override
void preprocessing(const optionst &)
virtual void help() override
display command line help
cbmc_parse_optionst(int argc, const char **argv)
Class that provides messages with a built-in verbosity 'level'.
Definition message.h:155
Coverage Instrumentation.
Program Transformation.
Symbol Table + CFG.
Traces of GOTO Programs.
JSON Commandline Interface.
Abstract interface to support a programming language.
String support via creating string constraints and progressively instantiating the universal constrai...
Emit timestamps.
XML Interface.