cprover
bmc.h
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: Bounded Model Checking for ANSI-C + HDL
4 
5 Author: Daniel Kroening, kroening@kroening.com
6 
7 \*******************************************************************/
8 
11 
12 #ifndef CPROVER_CBMC_BMC_H
13 #define CPROVER_CBMC_BMC_H
14 
15 #include <list>
16 #include <map>
17 
18 #include <util/options.h>
19 
20 #include <solvers/prop/prop.h>
21 #include <solvers/prop/prop_conv.h>
22 #include <solvers/sat/cnf.h>
23 #include <solvers/sat/satcheck.h>
24 #include <solvers/smt1/smt1_dec.h>
25 #include <solvers/smt2/smt2_dec.h>
26 #include <langapi/language_ui.h>
29 
30 #include "symex_bmc.h"
31 
32 class bmct:public safety_checkert
33 {
34 public:
36  const optionst &_options,
37  const symbol_tablet &_symbol_table,
38  message_handlert &_message_handler,
39  prop_convt &_prop_conv):
40  safety_checkert(ns, _message_handler),
41  options(_options),
42  ns(_symbol_table, new_symbol_table),
43  equation(ns),
45  prop_conv(_prop_conv),
46  ui(ui_message_handlert::uit::PLAIN)
47  {
50  !options.get_option("symex-coverage-report").empty();
51  }
52 
53  virtual resultt run(const goto_functionst &goto_functions);
54  virtual ~bmct() { }
55 
56  // additional stuff
58 
59  void set_ui(language_uit::uit _ui) { ui=_ui; }
60 
61  // the safety_checkert interface
63  const goto_functionst &goto_functions)
64  {
65  return run(goto_functions);
66  }
67 
68 protected:
69  const optionst &options;
75 
76  // use gui format
78 
81 
82  virtual resultt decide(
83  const goto_functionst &,
84  prop_convt &);
85 
86  // unwinding
87  virtual void setup_unwind();
88  virtual void do_unwind_module();
89  void do_conversion();
90 
91  virtual void show_vcc();
92  virtual void show_vcc_plain(std::ostream &out);
93  virtual void show_vcc_json(std::ostream &out);
94 
95  virtual resultt all_properties(
96  const goto_functionst &goto_functions,
97  prop_convt &solver);
98  virtual resultt stop_on_fail(
99  const goto_functionst &goto_functions,
100  prop_convt &solver);
101  virtual void show_program();
102  virtual void report_success();
103  virtual void report_failure();
104 
105  virtual void error_trace();
106  void output_graphml(
107  resultt result,
108  const goto_functionst &goto_functions);
109 
110  bool cover(
111  const goto_functionst &goto_functions,
112  const optionst::value_listt &criteria);
113 
114  friend class bmc_all_propertiest;
115  friend class bmc_covert;
116  friend class fault_localizationt;
117 };
118 
119 #endif // CPROVER_CBMC_BMC_H
void output_graphml(resultt result, const goto_functionst &goto_functions)
outputs witnesses in graphml format
Definition: bmc.cpp:93
CNF Generation, via Tseitin.
mstreamt & result()
Definition: message.h:233
void do_conversion()
Definition: bmc.cpp:118
Generate Equation using Symbolic Execution.
virtual void show_vcc_plain(std::ostream &out)
Definition: show_vcc.cpp:26
virtual resultt all_properties(const goto_functionst &goto_functions, prop_convt &solver)
virtual resultt operator()(const goto_functionst &goto_functions)
Definition: bmc.h:62
bool record_coverage
Definition: symex_bmc.h:64
virtual void show_vcc()
Definition: show_vcc.cpp:142
bool constant_propagation
Definition: goto_symex.h:94
virtual void report_failure()
Definition: bmc.cpp:193
bool cover(const goto_functionst &goto_functions, const optionst::value_listt &criteria)
Try to cover all goals.
Definition: bmc_cover.cpp:435
virtual void setup_unwind()
Definition: bmc.cpp:543
virtual resultt decide(const goto_functionst &, prop_convt &)
Definition: bmc.cpp:495
namespacet ns
Definition: bmc.h:71
symex_bmct symex
Definition: bmc.h:73
expr_listt bmc_constraints
Definition: bmc.h:57
virtual ~bmct()
Definition: bmc.h:54
virtual void error_trace()
Definition: bmc.cpp:51
virtual void do_unwind_module()
Definition: bmc.cpp:46
void set_ui(language_uit::uit _ui)
Definition: bmc.h:59
prop_convt & prop_conv
Definition: bmc.h:74
const std::string get_option(const std::string &option) const
Definition: options.cpp:60
bool get_bool_option(const std::string &option) const
Definition: options.cpp:42
The symbol table.
Definition: symbol_table.h:52
TO_BE_DOCUMENTED.
Definition: namespace.h:62
std::list< std::string > value_listt
Definition: options.h:22
virtual resultt run(const goto_functionst &goto_functions)
Definition: bmc.cpp:310
virtual void show_vcc_json(std::ostream &out)
Definition: show_vcc.cpp:84
virtual decision_proceduret::resultt run_decision_procedure(prop_convt &prop_conv)
Definition: bmc.cpp:139
std::list< exprt > expr_listt
Definition: expr.h:166
const optionst & options
Definition: bmc.h:69
language_uit::uit ui
Definition: bmc.h:77
virtual resultt stop_on_fail(const goto_functionst &goto_functions, prop_convt &solver)
Definition: bmc.cpp:507
Safety Checker Interface.
bmct(const optionst &_options, const symbol_tablet &_symbol_table, message_handlert &_message_handler, prop_convt &_prop_conv)
Definition: bmc.h:35
virtual void show_program()
Definition: bmc.cpp:221
Bounded Model Checking for ANSI-C.
Definition: bmc.h:32
symbol_tablet new_symbol_table
Definition: bmc.h:70
symex_target_equationt equation
Definition: bmc.h:72
Options.
virtual void report_success()
Definition: bmc.cpp:165