CBMC
Loading...
Searching...
No Matches
object_id.h
Go to the documentation of this file.
1/*******************************************************************\
2
3Module: Object Identifiers
4
5Author: 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
20class code_assignt;
21
23{
24public:
26
27 explicit object_idt(const symbol_exprt &symbol_expr)
28 {
29 id=symbol_expr.get_identifier();
30 }
31
32 explicit object_idt(const irep_idt &identifier)
33 {
34 id=identifier;
35 }
36
37 bool operator<(const object_idt &other) const
38 {
39 return id<other.id;
40 }
41
42 const irep_idt &get_id() const
43 {
44 return id;
45 }
46
47protected:
49};
50
51inline std::ostream &operator<<(
52 std::ostream &out,
53 const object_idt &object_id)
54{
55 return out << object_id.get_id();
56}
57
58typedef std::set<object_idt> object_id_sett;
59
60void get_objects(const exprt &expr, object_id_sett &dest);
61void get_objects_r(const code_assignt &assign, object_id_sett &);
62void get_objects_w(const code_assignt &assign, object_id_sett &);
64void get_objects_r_lhs(const exprt &lhs, object_id_sett &);
65
66#endif // CPROVER_GOTO_INSTRUMENT_OBJECT_ID_H
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition ai.h:562
A goto_instruction_codet representing an assignment in the program.
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
irep_idt id
Definition object_id.h:48
object_idt(const irep_idt &identifier)
Definition object_id.h:32
const irep_idt & get_id() const
Definition object_id.h:42
bool operator<(const object_idt &other) const
Definition object_id.h:37
object_idt(const symbol_exprt &symbol_expr)
Definition object_id.h:27
Expression to hold a symbol (variable)
Definition std_expr.h:131
const irep_idt & get_identifier() const
Definition std_expr.h:160
std::set< object_idt > object_id_sett
Definition object_id.h:58
void get_objects_w(const code_assignt &assign, object_id_sett &)
Definition object_id.cpp:89
void get_objects_r(const code_assignt &assign, object_id_sett &)
Definition object_id.cpp:83
void get_objects_r_lhs(const exprt &lhs, object_id_sett &)
Definition object_id.cpp:99
void get_objects(const exprt &expr, object_id_sett &dest)
Definition object_id.cpp:78
std::ostream & operator<<(std::ostream &out, const object_idt &object_id)
Definition object_id.h:51
void get_objects_w_lhs(const exprt &lhs, object_id_sett &)
API to expression classes.