cprover
path_replay.h
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: Dense Data Structure for Path Replay
4 
5 Author: Daniel Kroening, kroening@kroening.com
6 
7 \*******************************************************************/
8 
11 
12 #ifndef CPROVER_PATH_SYMEX_PATH_REPLAY_H
13 #define CPROVER_PATH_SYMEX_PATH_REPLAY_H
14 
15 #include "path_symex_state.h"
16 
18 {
19 public:
21  {
22  }
23 
24  explicit path_replayt(const path_symex_statet &src)
25  {
26  get_branches(src.history);
27  }
28 
29  void replay(path_symex_statet &);
30 
31 protected:
32  // TODO: consider something even denser, say something like a bitset
33  typedef std::vector<bool> branchest;
34  branchest branches;
35 
36  void get_branches(const path_symex_step_reft history);
37 };
38 
39 void path_replay(path_symex_step_reft history);
40 
41 #endif // CPROVER_PATH_SYMEX_PATH_REPLAY_H
void replay(path_symex_statet &)
branchest branches
Definition: path_replay.h:34
path_replayt(const path_symex_statet &src)
Definition: path_replay.h:24
void get_branches(const path_symex_step_reft history)
State of path-based symbolic simulator.
void path_replay(path_symex_step_reft history)
std::vector< bool > branchest
Definition: path_replay.h:33
path_symex_step_reft history