cprover
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 
46  void operator()(exprt &dest) const
47  {
48  rename(dest);
49  }
50 
51  void operator()(typet &dest) const
52  {
53  rename(dest);
54  }
55 
57  virtual ~rename_symbolt();
58 
61 
62 protected:
63  bool rename(exprt &dest) const;
64  bool rename(typet &dest) const;
65 
66  bool have_to_rename(const exprt &dest) const;
67  bool have_to_rename(const typet &type) const;
68 };
69 
70 #endif // CPROVER_UTIL_RENAME_SYMBOL_H
type_mapt type_map
Definition: rename_symbol.h:60
The type of an expression.
Definition: type.h:22
std::unordered_map< irep_idt, irep_idt > expr_mapt
Definition: rename_symbol.h:28
void insert_type(const irep_idt &old_id, const irep_idt &new_id)
Definition: rename_symbol.h:40
expr_mapt expr_map
Definition: rename_symbol.h:59
bool have_to_rename(const exprt &dest) const
void operator()(typet &dest) const
Definition: rename_symbol.h:51
std::unordered_map< irep_idt, irep_idt > type_mapt
Definition: rename_symbol.h:29
bool rename(exprt &dest) const
dstringt has one field, an unsigned integer no which is an index into a static table of strings...
Definition: dstring.h:33
void insert_expr(const irep_idt &old_id, const irep_idt &new_id)
Definition: rename_symbol.h:31
void operator()(exprt &dest) const
Definition: rename_symbol.h:46
Base class for all expressions.
Definition: expr.h:42
Expression to hold a symbol (variable)
Definition: std_expr.h:90
void insert(const class symbol_exprt &old_expr, const class symbol_exprt &new_expr)
virtual ~rename_symbolt()