CBMC
replace_expr.cpp
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module:
4 
5 Author: Daniel Kroening, kroening@kroening.com
6 
7 \*******************************************************************/
8 
9 #include "replace_expr.h"
10 #include "expr_iterator.h"
11 
12 bool replace_expr(const exprt &what, const exprt &by, exprt &dest)
13 {
15  what.type() == by.type(),
16  "types to be replaced should match. old type:\n" + what.type().pretty() +
17  "\nnew type:\n" + by.type().pretty());
18 
19  bool no_change = true;
20 
21  for(auto it = dest.depth_begin(), itend = dest.depth_end();
22  it != itend;) // no ++it
23  {
24  if(*it == what)
25  {
26  it.mutate() = by;
27  no_change = false;
28  it.next_sibling_or_parent();
29  }
30  else
31  ++it;
32  }
33 
34  return no_change;
35 }
36 
37 bool replace_expr(const replace_mapt &what, exprt &dest)
38 {
39  bool no_change = true;
40 
41  for(auto it = dest.depth_begin(), itend = dest.depth_end();
42  it != itend;) // No ++it
43  {
44  replace_mapt::const_iterator findit = what.find(*it);
45  if(findit != what.end())
46  {
48  it->type() == findit->second.type(),
49  "types to be replaced should match. old type:\n" + it->type().pretty() +
50  "\nnew type:\n" + findit->second.type().pretty());
51 
52  it.mutate() = findit->second;
53  no_change = false;
54  it.next_sibling_or_parent();
55  }
56  else
57  ++it;
58  }
59 
60  return no_change;
61 }
Base class for all expressions.
Definition: expr.h:56
depth_iteratort depth_end()
Definition: expr.cpp:249
depth_iteratort depth_begin()
Definition: expr.cpp:247
typet & type()
Return the type of the expression.
Definition: expr.h:84
std::string pretty(unsigned indent=0, unsigned max_indent=0) const
Definition: irep.cpp:482
Forward depth-first search iterators These iterators' copy operations are expensive,...
bool replace_expr(const exprt &what, const exprt &by, exprt &dest)
std::unordered_map< exprt, exprt, irep_hash > replace_mapt
Definition: replace_expr.h:22
#define PRECONDITION_WITH_DIAGNOSTICS(CONDITION,...)
Definition: invariant.h:464