cprover
bmc.h File Reference

Bounded Model Checking for ANSI-C + HDL. More...

Include dependency graph for bmc.h:
This graph shows which files directly or indirectly include this file:

Go to the source code of this file.

Classes

class  bmct
 Bounded model checking or path exploration for goto-programs. More...
 
class  path_explorert
 Symbolic execution from a saved branch point. More...
 

Macros

#define OPT_BMC
 
#define HELP_BMC
 

Detailed Description

Bounded Model Checking for ANSI-C + HDL.

Definition in file bmc.h.

Macro Definition Documentation

◆ HELP_BMC

#define HELP_BMC
Value:
" --paths [strategy] explore paths one at a time\n" \
" --show-symex-strategies list strategies for use with --paths\n" \
" --program-only only show program expression\n" \
" --show-loops show the loops in the program\n" \
" --depth nr limit search depth\n" \
" --unwind nr unwind nr times\n" \
" --unwindset L:B,... unwind loop L with a bound of B\n" \
" (use --show-loops to get the loop IDs)\n" \
" --show-vcc show the verification conditions\n" \
" --slice-formula remove assignments unrelated to property\n" \
" --unwinding-assertions generate unwinding assertions (cannot be\n" \
" used with --cover or --partial-loops)\n" \
" --partial-loops permit paths with partial loops\n" \
" --no-self-loops-to-assumptions\n" \
" do not simplify while(1){} to assume(0)\n" \
" --no-pretty-names do not simplify identifiers\n" \
" --graphml-witness filename write the witness in GraphML format to " \
"filename\n"

Definition at line 317 of file bmc.h.

Referenced by cbmc_parse_optionst::help(), and jbmc_parse_optionst::help().

◆ OPT_BMC

#define OPT_BMC
Value:
"(program-only)" \
"(show-loops)" \
"(show-vcc)" \
"(slice-formula)" \
"(unwinding-assertions)" \
"(no-unwinding-assertions)" \
"(no-pretty-names)" \
"(no-self-loops-to-assumptions)" \
"(partial-loops)" \
"(paths):" \
"(show-symex-strategies)" \
"(depth):" \
"(unwind):" \
"(unwindset):" \
"(graphml-witness):" \
"(unwindset):"

Definition at line 299 of file bmc.h.