Bounded Model Checking for ANSI-C + HDL. More...
#include <list>#include <map>#include <util/invariant.h>#include <util/options.h>#include <util/ui_message.h>#include <util/decision_procedure.h>#include <goto-programs/goto_trace.h>#include <goto-symex/symex_target_equation.h>#include <goto-symex/path_storage.h>#include <goto-programs/goto_model.h>#include <goto-programs/safety_checker.h>#include <goto-symex/memory_model.h>#include "symex_bmc.h"
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"
◆ 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):"
