cprover
object_id.h
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: Object Identifiers
4 
5 Author: Daniel Kroening, kroening@kroening.com
6 
7 \*******************************************************************/
8 
11 
12 #ifndef CPROVER_GOTO_INSTRUMENT_OBJECT_ID_H
13 #define CPROVER_GOTO_INSTRUMENT_OBJECT_ID_H
14 
15 #include <iosfwd>
16 #include <set>
17 
18 #include <util/std_expr.h>
19 #include <util/std_code.h>
20 
22 {
23 public:
24  object_idt() { }
25 
26  explicit object_idt(const symbol_exprt &symbol_expr)
27  {
28  id=symbol_expr.get_identifier();
29  }
30 
31  explicit object_idt(const irep_idt &identifier)
32  {
33  id=identifier;
34  }
35 
36  bool operator<(const object_idt &other) const
37  {
38  return id<other.id;
39  }
40 
41  const irep_idt &get_id() const
42  {
43  return id;
44  }
45 
46 protected:
48 };
49 
50 inline std::ostream &operator<<(
51  std::ostream &out,
52  const object_idt &object_id)
53 {
54  return out << object_id.get_id();
55 }
56 
57 typedef std::set<object_idt> object_id_sett;
58 
59 void get_objects(const exprt &expr, object_id_sett &dest);
60 void get_objects_r(const code_assignt &assign, object_id_sett &);
61 void get_objects_w(const code_assignt &assign, object_id_sett &);
62 void get_objects_w_lhs(const exprt &lhs, object_id_sett &);
63 void get_objects_r_lhs(const exprt &lhs, object_id_sett &);
64 
65 #endif // CPROVER_GOTO_INSTRUMENT_OBJECT_ID_H
void get_objects(const exprt &expr, object_id_sett &dest)
Definition: object_id.cpp:72
object_idt()
Definition: object_id.h:24
const irep_idt & get_identifier() const
Definition: std_expr.h:176
std::ostream & operator<<(std::ostream &out, const object_idt &object_id)
Definition: object_id.h:50
std::set< object_idt > object_id_sett
Definition: object_id.h:57
void get_objects_w(const code_assignt &assign, object_id_sett &)
Definition: object_id.cpp:83
irep_idt id
Definition: object_id.h:47
void get_objects_r(const code_assignt &assign, object_id_sett &)
Definition: object_id.cpp:77
API to expression classes.
void get_objects_w_lhs(const exprt &lhs, object_id_sett &)
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:35
object_idt(const irep_idt &identifier)
Definition: object_id.h:31
void get_objects_r_lhs(const exprt &lhs, object_id_sett &)
Definition: object_id.cpp:93
const irep_idt & get_id() const
Definition: object_id.h:41
Base class for all expressions.
Definition: expr.h:54
bool operator<(const object_idt &other) const
Definition: object_id.h:36
object_idt(const symbol_exprt &symbol_expr)
Definition: object_id.h:26
Expression to hold a symbol (variable)
Definition: std_expr.h:143
A codet representing an assignment in the program.
Definition: std_code.h:256