Skip to content

Commit 928a6d8

Browse files
peterschrammelpeterschrammel
authored
Merge pull request #3581 from peterschrammel/move-bmc-options
Move BMC options and help text to bmc_util [depends: 3565]
2 parents f8991d9 + 8d150f0 commit 928a6d8

File tree

6 files changed

+45
-41
lines changed

6 files changed

+45
-41
lines changed

‎jbmc/src/jbmc/jbmc_parse_options.cpp

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -53,6 +53,8 @@ Author: Daniel Kroening, [email protected]
5353

5454
#include <langapi/mode.h>
5555

56+
#include <cbmc/bmc.h> // will go away
57+
5658
#include <java_bytecode/convert_java_nondet.h>
5759
#include <java_bytecode/java_bytecode_language.h>
5860
#include <java_bytecode/java_enum_static_init_unwind_handler.h>

‎jbmc/src/jbmc/jbmc_parse_options.h

Lines changed: 1 addition & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -20,7 +20,7 @@ Author: Daniel Kroening, [email protected]
2020

2121
#include <analyses/goto_check.h>
2222

23-
#include <cbmc/bmc.h>
23+
#include <goto-checker/bmc_util.h>
2424

2525
#include <goto-programs/class_hierarchy.h>
2626
#include <goto-programs/goto_trace.h>
@@ -33,7 +33,6 @@ Author: Daniel Kroening, [email protected]
3333

3434
#include <java_bytecode/java_bytecode_language.h>
3535

36-
class bmct;
3736
class goto_functionst;
3837
class optionst;
3938

‎src/cbmc/bmc.h

Lines changed: 0 additions & 38 deletions
Original file line numberDiff line numberDiff line change
@@ -264,42 +264,4 @@ class path_explorert : public bmct
264264
goto_symext::get_goto_functiont get_goto_function) override;
265265
};
266266

267-
#define OPT_BMC \
268-
"(program-only)" \
269-
"(show-loops)" \
270-
"(show-vcc)" \
271-
"(slice-formula)" \
272-
"(unwinding-assertions)" \
273-
"(no-unwinding-assertions)" \
274-
"(no-pretty-names)" \
275-
"(no-self-loops-to-assumptions)" \
276-
"(partial-loops)" \
277-
"(paths):" \
278-
"(show-symex-strategies)" \
279-
"(depth):" \
280-
"(unwind):" \
281-
"(unwindset):" \
282-
"(graphml-witness):" \
283-
"(unwindset):"
284-
285-
#define HELP_BMC \
286-
" --paths [strategy] explore paths one at a time\n" \
287-
" --show-symex-strategies list strategies for use with --paths\n" \
288-
" --program-only only show program expression\n" \
289-
" --show-loops show the loops in the program\n" \
290-
" --depth nr limit search depth\n" \
291-
" --unwind nr unwind nr times\n" \
292-
" --unwindset L:B,... unwind loop L with a bound of B\n" \
293-
" (use --show-loops to get the loop IDs)\n" \
294-
" --show-vcc show the verification conditions\n" \
295-
" --slice-formula remove assignments unrelated to property\n" \
296-
" --unwinding-assertions generate unwinding assertions (cannot be\n" \
297-
" used with --cover or --partial-loops)\n" \
298-
" --partial-loops permit paths with partial loops\n" \
299-
" --no-self-loops-to-assumptions\n" \
300-
" do not simplify while(1){} to assume(0)\n" \
301-
" --no-pretty-names do not simplify identifiers\n" \
302-
" --graphml-witness filename write the witness in GraphML format to " \
303-
"filename\n" // NOLINT(*)
304-
305267
#endif // CPROVER_CBMC_BMC_H

‎src/cbmc/cbmc_parse_options.cpp

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -30,6 +30,8 @@ Author: Daniel Kroening, [email protected]
3030

3131
#include <cpp/cprover_library.h>
3232

33+
#include <goto-checker/bmc_util.h>
34+
3335
#include <goto-programs/adjust_float_expressions.h>
3436
#include <goto-programs/initialize_goto_model.h>
3537
#include <goto-programs/instrument_preconditions.h>

‎src/cbmc/cbmc_parse_options.h

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -24,6 +24,7 @@ Author: Daniel Kroening, [email protected]
2424

2525
#include <analyses/goto_check.h>
2626

27+
#include <goto-checker/bmc_util.h>
2728
#include <goto-checker/solver_factory.h>
2829

2930
#include <goto-programs/goto_trace.h>
@@ -33,7 +34,6 @@ Author: Daniel Kroening, [email protected]
3334
#include "bmc.h"
3435
#include "xml_interface.h"
3536

36-
class bmct;
3737
class goto_functionst;
3838
class optionst;
3939

‎src/goto-checker/bmc_util.h

Lines changed: 39 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -71,4 +71,43 @@ void slice(
7171
const optionst &,
7272
ui_message_handlert &);
7373

74+
// clang-format off
75+
#define OPT_BMC \
76+
"(program-only)" \
77+
"(show-loops)" \
78+
"(show-vcc)" \
79+
"(slice-formula)" \
80+
"(unwinding-assertions)" \
81+
"(no-unwinding-assertions)" \
82+
"(no-pretty-names)" \
83+
"(no-self-loops-to-assumptions)" \
84+
"(partial-loops)" \
85+
"(paths):" \
86+
"(show-symex-strategies)" \
87+
"(depth):" \
88+
"(unwind):" \
89+
"(unwindset):" \
90+
"(graphml-witness):" \
91+
"(unwindset):"
92+
93+
#define HELP_BMC \
94+
" --paths [strategy] explore paths one at a time\n" \
95+
" --show-symex-strategies list strategies for use with --paths\n" \
96+
" --program-only only show program expression\n" \
97+
" --show-loops show the loops in the program\n" \
98+
" --depth nr limit search depth\n" \
99+
" --unwind nr unwind nr times\n" \
100+
" --unwindset L:B,... unwind loop L with a bound of B\n" \
101+
" (use --show-loops to get the loop IDs)\n" \
102+
" --show-vcc show the verification conditions\n" \
103+
" --slice-formula remove assignments unrelated to property\n" \
104+
" --unwinding-assertions generate unwinding assertions (cannot be\n" \
105+
" used with --cover or --partial-loops)\n" \
106+
" --partial-loops permit paths with partial loops\n" \
107+
" --no-self-loops-to-assumptions\n" \
108+
" do not simplify while(1){} to assume(0)\n" \
109+
" --no-pretty-names do not simplify identifiers\n" \
110+
" --graphml-witness filename write the witness in GraphML format to filename\n" // NOLINT(*)
111+
// clang-format on
112+
74113
#endif // CPROVER_GOTO_CHECKER_BMC_UTIL_H

0 commit comments

Comments
 (0)