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 &);
63 void get_objects_r_lhs(const exprt &lhs, object_id_sett &);
64 
65 #endif // CPROVER_GOTO_INSTRUMENT_OBJECT_ID_H
dstringt
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:37
object_idt::object_idt
object_idt(const symbol_exprt &symbol_expr)
Definition: object_id.h:26
get_objects_w_lhs
void get_objects_w_lhs(const exprt &lhs, object_id_sett &)
object_idt::operator<
bool operator<(const object_idt &other) const
Definition: object_id.h:36
object_idt::object_idt
object_idt(const irep_idt &identifier)
Definition: object_id.h:31
exprt
Base class for all expressions.
Definition: expr.h:53
object_idt::get_id
const irep_idt & get_id() const
Definition: object_id.h:41
symbol_exprt
Expression to hold a symbol (variable)
Definition: std_expr.h:82
object_idt
Definition: object_id.h:22
symbol_exprt::get_identifier
const irep_idt & get_identifier() const
Definition: std_expr.h:111
operator<<
std::ostream & operator<<(std::ostream &out, const object_idt &object_id)
Definition: object_id.h:50
get_objects_r
void get_objects_r(const code_assignt &assign, object_id_sett &)
Definition: object_id.cpp:77
std_code.h
get_objects
void get_objects(const exprt &expr, object_id_sett &dest)
Definition: object_id.cpp:72
object_id_sett
std::set< object_idt > object_id_sett
Definition: object_id.h:57
object_idt::object_idt
object_idt()
Definition: object_id.h:24
object_idt::id
irep_idt id
Definition: object_id.h:47
get_objects_w
void get_objects_w(const code_assignt &assign, object_id_sett &)
Definition: object_id.cpp:83
code_assignt
A codet representing an assignment in the program.
Definition: std_code.h:295
get_objects_r_lhs
void get_objects_r_lhs(const exprt &lhs, object_id_sett &)
Definition: object_id.cpp:93
std_expr.h
API to expression classes.