CBMC
rename_symbol.h
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module:
4 
5 Author: Daniel Kroening, kroening@kroening.com
6 
7 \*******************************************************************/
8 
9 
10 #ifndef CPROVER_UTIL_RENAME_SYMBOL_H
11 #define CPROVER_UTIL_RENAME_SYMBOL_H
12 
13 //
14 // true: did nothing
15 // false: renamed something
16 //
17 
18 #include <unordered_map>
19 
20 #include "irep.h"
21 
22 class exprt;
23 class typet;
24 
26 {
27 public:
28  typedef std::unordered_map<irep_idt, irep_idt> expr_mapt;
29  typedef std::unordered_map<irep_idt, irep_idt> type_mapt;
30 
31  void insert_expr(const irep_idt &old_id,
32  const irep_idt &new_id)
33  {
34  expr_map.insert(std::pair<irep_idt, irep_idt>(old_id, new_id));
35  }
36 
37  void insert(const class symbol_exprt &old_expr,
38  const class symbol_exprt &new_expr);
39 
40  void insert_type(const irep_idt &old_id,
41  const irep_idt &new_id)
42  {
43  type_map.insert(std::pair<irep_idt, irep_idt>(old_id, new_id));
44  }
45 
48  bool operator()(exprt &dest) const
49  {
50  return rename(dest);
51  }
52 
55  bool operator()(typet &dest) const
56  {
57  return rename(dest);
58  }
59 
61  virtual ~rename_symbolt();
62 
65 
66 protected:
67  bool rename(exprt &dest) const;
68  bool rename(typet &dest) const;
69 
70  bool have_to_rename(const exprt &dest) const;
71  bool have_to_rename(const typet &type) const;
72 };
73 
74 #endif // CPROVER_UTIL_RENAME_SYMBOL_H
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:38
Base class for all expressions.
Definition: expr.h:56
void insert(const class symbol_exprt &old_expr, const class symbol_exprt &new_expr)
virtual ~rename_symbolt()
bool operator()(exprt &dest) const
Rename symbols in dest.
Definition: rename_symbol.h:48
void insert_type(const irep_idt &old_id, const irep_idt &new_id)
Definition: rename_symbol.h:40
std::unordered_map< irep_idt, irep_idt > type_mapt
Definition: rename_symbol.h:29
std::unordered_map< irep_idt, irep_idt > expr_mapt
Definition: rename_symbol.h:28
bool have_to_rename(const exprt &dest) const
expr_mapt expr_map
Definition: rename_symbol.h:63
bool rename(exprt &dest) const
type_mapt type_map
Definition: rename_symbol.h:64
void insert_expr(const irep_idt &old_id, const irep_idt &new_id)
Definition: rename_symbol.h:31
bool operator()(typet &dest) const
Rename symbols in dest.
Definition: rename_symbol.h:55
Expression to hold a symbol (variable)
Definition: std_expr.h:131
The type of an expression, extends irept.
Definition: type.h:29