cprover
symex_bmc.h
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: Bounded Model Checking for ANSI-C
4 
5 Author: Daniel Kroening, kroening@kroening.com
6 
7 \*******************************************************************/
8 
11 
12 #ifndef CPROVER_CBMC_SYMEX_BMC_H
13 #define CPROVER_CBMC_SYMEX_BMC_H
14 
15 #include <util/message.h>
16 
17 #include <goto-symex/goto_symex.h>
18 
19 #include "symex_coverage.h"
20 
21 class symex_bmct:
22  public goto_symext,
23  public messaget
24 {
25 public:
26  symex_bmct(
27  const namespacet &_ns,
28  symbol_tablet &_new_symbol_table,
29  symex_targett &_target);
30 
31  // To show progress
33 
34  // Control unwinding.
35 
36  void set_unwind_limit(unsigned limit)
37  {
38  max_unwind=limit;
39  max_unwind_is_set=true;
40  }
41 
43  unsigned thread_nr,
44  const irep_idt &id,
45  unsigned limit)
46  {
47  thread_loop_limits[thread_nr][id]=limit;
48  }
49 
51  const irep_idt &id,
52  unsigned limit)
53  {
54  loop_limits[id]=limit;
55  }
56 
58  const goto_functionst &goto_functions,
59  const std::string &path) const
60  {
61  return symex_coverage.generate_report(goto_functions, path);
62  }
63 
65 
66 protected:
67  // We have
68  // 1) a global limit (max_unwind)
69  // 2) a limit per loop, all threads
70  // 3) a limit for a particular thread.
71  // We use the most specific of the above.
72 
73  unsigned max_unwind;
75 
76  typedef std::unordered_map<irep_idt, unsigned, irep_id_hash> loop_limitst;
77  loop_limitst loop_limits;
78 
79  typedef std::map<unsigned, loop_limitst> thread_loop_limitst;
80  thread_loop_limitst thread_loop_limits;
81 
82  //
83  // overloaded from goto_symext
84  //
85  virtual void symex_step(
86  const goto_functionst &goto_functions,
87  statet &state);
88 
89  virtual void merge_goto(
90  const statet::goto_statet &goto_state,
91  statet &state);
92 
93  // for loop unwinding
94  virtual bool get_unwind(
95  const symex_targett::sourcet &source,
96  unsigned unwind);
97 
98  virtual bool get_unwind_recursion(
99  const irep_idt &identifier,
100  const unsigned thread_nr,
101  unsigned unwind);
102 
103  virtual void no_body(const irep_idt &identifier);
104 
105  std::unordered_set<irep_idt, irep_id_hash> body_warnings;
106 
108 };
109 
110 #endif // CPROVER_CBMC_SYMEX_BMC_H
bool record_coverage
Definition: symex_bmc.h:64
void set_unwind_loop_limit(const irep_idt &id, unsigned limit)
Definition: symex_bmc.h:50
bool generate_report(const goto_functionst &goto_functions, const std::string &path) const
virtual bool get_unwind(const symex_targett::sourcet &source, unsigned unwind)
Definition: symex_bmc.cpp:106
void set_unwind_limit(unsigned limit)
Definition: symex_bmc.h:36
std::map< unsigned, loop_limitst > thread_loop_limitst
Definition: symex_bmc.h:79
bool output_coverage_report(const goto_functionst &goto_functions, const std::string &path) const
Definition: symex_bmc.h:57
symex_coveraget symex_coverage
Definition: symex_bmc.h:107
Symbolic Execution.
The symbol table.
Definition: symbol_table.h:52
TO_BE_DOCUMENTED.
Definition: namespace.h:62
virtual void merge_goto(const statet::goto_statet &goto_state, statet &state)
Definition: symex_bmc.cpp:87
thread_loop_limitst thread_loop_limits
Definition: symex_bmc.h:80
loop_limitst loop_limits
Definition: symex_bmc.h:77
bool max_unwind_is_set
Definition: symex_bmc.h:74
The main class for the forward symbolic simulator.
Definition: goto_symex.h:41
unsigned max_unwind
Definition: symex_bmc.h:73
std::unordered_map< irep_idt, unsigned, irep_id_hash > loop_limitst
Definition: symex_bmc.h:76
virtual bool get_unwind_recursion(const irep_idt &identifier, const unsigned thread_nr, unsigned unwind)
Definition: symex_bmc.cpp:147
source_locationt last_source_location
Definition: symex_bmc.h:32
Record and print code coverage of symbolic execution.
std::unordered_set< irep_idt, irep_id_hash > body_warnings
Definition: symex_bmc.h:105
virtual void symex_step(const goto_functionst &goto_functions, statet &state)
show progress
Definition: symex_bmc.cpp:31
symex_bmct(const namespacet &_ns, symbol_tablet &_new_symbol_table, symex_targett &_target)
Definition: symex_bmc.cpp:19
void set_unwind_thread_loop_limit(unsigned thread_nr, const irep_idt &id, unsigned limit)
Definition: symex_bmc.h:42
virtual void no_body(const irep_idt &identifier)
Definition: symex_bmc.cpp:192