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 #include <util/threeval.h>
17 
19 #include <goto-symex/goto_symex.h>
20 
22 
23 #include "symex_coverage.h"
24 
25 class symex_bmct: public goto_symext
26 {
27 public:
28  symex_bmct(
29  message_handlert &mh,
31  symex_target_equationt &_target,
32  const optionst &options,
34 
35  // To show progress
37 
44  typedef
45  std::function<tvt(const irep_idt &, unsigned, unsigned, unsigned &)>
47 
54  typedef std::function<tvt(const irep_idt &, unsigned, unsigned &)>
56 
62  {
63  loop_unwind_handlers.push_back(handler);
64  }
65 
71  {
72  recursion_unwind_handlers.push_back(handler);
73  }
74 
76  const goto_functionst &goto_functions,
77  const std::string &path) const
78  {
79  return symex_coverage.generate_report(goto_functions, path);
80  }
81 
83 
85 
86 protected:
88  std::vector<loop_unwind_handlert> loop_unwind_handlers;
89 
92  std::vector<recursion_unwind_handlert> recursion_unwind_handlers;
93 
94  //
95  // overloaded from goto_symext
96  //
97  virtual void symex_step(
98  const get_goto_functiont &get_goto_function,
99  statet &state);
100 
101  virtual void merge_goto(
102  const statet::goto_statet &goto_state,
103  statet &state);
104 
105  // for loop unwinding
106  virtual bool get_unwind(
107  const symex_targett::sourcet &source,
108  unsigned unwind);
109 
110  virtual bool get_unwind_recursion(
111  const irep_idt &identifier,
112  const unsigned thread_nr,
113  unsigned unwind);
114 
115  virtual void no_body(const irep_idt &identifier);
116 
117  std::unordered_set<irep_idt> body_warnings;
118 
120 };
121 
122 #endif // CPROVER_CBMC_SYMEX_BMC_H
std::unordered_set< irep_idt > body_warnings
Definition: symex_bmc.h:117
bool record_coverage
Definition: symex_bmc.h:82
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:107
std::vector< recursion_unwind_handlert > recursion_unwind_handlers
Callbacks that may provide an unwind/do-not-unwind decision for a recursive call. ...
Definition: symex_bmc.h:92
std::function< const goto_functionst::goto_functiont &(const irep_idt &)> get_goto_functiont
Definition: goto_symex.h:84
void add_loop_unwind_handler(loop_unwind_handlert handler)
Add a callback function that will be called to determine whether to unwind loops. ...
Definition: symex_bmc.h:61
void add_recursion_unwind_handler(recursion_unwind_handlert handler)
Add a callback function that will be called to determine whether to unwind recursion.
Definition: symex_bmc.h:70
bool output_coverage_report(const goto_functionst &goto_functions, const std::string &path) const
Definition: symex_bmc.h:75
symex_coveraget symex_coverage
Definition: symex_bmc.h:119
const symbol_tablet & outer_symbol_table
The symbol table associated with the goto-program that we&#39;re executing.
Definition: goto_symex.h:228
Symbolic Execution.
The symbol table.
Definition: symbol_table.h:19
path_storaget & path_storage
Definition: goto_symex.h:467
virtual void merge_goto(const statet::goto_statet &goto_state, statet &state)
Definition: symex_bmc.cpp:88
Loop unwinding.
Storage for symbolic execution paths to be resumed later.
Definition: path_storage.h:24
const optionst & options
Definition: goto_symex.h:202
The main class for the forward symbolic simulator.
Definition: goto_symex.h:46
virtual bool get_unwind_recursion(const irep_idt &identifier, const unsigned thread_nr, unsigned unwind)
Definition: symex_bmc.cpp:156
symex_bmct(message_handlert &mh, const symbol_tablet &outer_symbol_table, symex_target_equationt &_target, const optionst &options, path_storaget &path_storage)
Definition: symex_bmc.cpp:21
std::function< tvt(const irep_idt &, unsigned, unsigned, unsigned &)> loop_unwind_handlert
Loop unwind handlers take the function ID and loop number, the unwind count so far, and an out-parameter specifying an advisory maximum, which they may set.
Definition: symex_bmc.h:46
virtual void symex_step(const get_goto_functiont &get_goto_function, statet &state)
show progress
Definition: symex_bmc.cpp:34
source_locationt last_source_location
Definition: symex_bmc.h:36
Record and print code coverage of symbolic execution.
std::vector< loop_unwind_handlert > loop_unwind_handlers
Callbacks that may provide an unwind/do-not-unwind decision for a loop.
Definition: symex_bmc.h:88
std::function< tvt(const irep_idt &, unsigned, unsigned &)> recursion_unwind_handlert
Recursion unwind handlers take the function ID, the unwind count so far, and an out-parameter specify...
Definition: symex_bmc.h:55
Storage of symbolic execution paths to resume.
unwindsett unwindset
Definition: symex_bmc.h:84
virtual void no_body(const irep_idt &identifier)
Definition: symex_bmc.cpp:203