cprover
path_symex_history.cpp
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: History of path-based symbolic simulator
4 
5 Author: Daniel Kroening, kroening@kroening.com
6 
7 \*******************************************************************/
8 
11 
12 #include "path_symex_history.h"
13 
14 #include <algorithm>
15 
17 
18 #include <langapi/language_util.h>
19 
20 void path_symex_stept::output(std::ostream &out) const
21 {
22  out << "PCs:";
23 
24 /*
25  for(pc_vectort::const_iterator p_it=s_it->pc_vector.begin();
26  p_it!=pc_vector.end();
27  p_it++)
28  out << " " << *p_it;
29  */
30  out << "\n";
31 
32  out << "Guard: " << from_expr(guard) << "\n";
33  out << "Full LHS: " << from_expr(full_lhs) << "\n";
34  out << "SSA LHS: " << from_expr(ssa_lhs) << "\n";
35  out << "SSA RHS: " << from_expr(ssa_rhs) << "\n";
36  out << "\n";
37 }
38 
40 {
41  if(ssa_rhs.is_not_nil())
42  dest << equal_exprt(ssa_lhs, ssa_rhs);
43 
44  if(guard.is_not_nil())
45  dest << guard;
46 }
47 
49  std::vector<path_symex_step_reft> &dest) const
50 {
51  dest.clear();
52 
53  path_symex_step_reft s=*this;
54  while(!s.is_nil())
55  {
56  dest.push_back(s);
57  --s;
58  }
59 
60  // the above goes backwards: now need to reverse
61  std::reverse(dest.begin(), dest.end());
62 }
History for path-based symbolic simulator.
bool is_not_nil() const
Definition: irep.h:104
void build_history(std::vector< path_symex_step_reft > &dest) const
std::string from_expr(const namespacet &ns, const irep_idt &identifier, const exprt &expr)
Decision Procedure Interface.
void convert(decision_proceduret &dest) const
equality
Definition: std_expr.h:1082
void output(std::ostream &) const