cprover
|
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"
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 |
Bounded Model Checking for ANSI-C + HDL.
Definition in file bmc.h.
#define HELP_BMC |
Definition at line 317 of file bmc.h.
Referenced by cbmc_parse_optionst::help(), and jbmc_parse_optionst::help().
#define OPT_BMC |