CBMC
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_SYMBOL_H
11 #define CPROVER_UTIL_SYMBOL_H
12 
17 
18 #include <iosfwd>
19 
20 #include "expr.h"
21 #include "invariant.h"
22 
27 class symbolt
28 {
29 public:
32 
35 
38 
41 
44 
47 
50 
53 
55  const irep_idt &display_name() const
56  {
58  }
59 
60  // global use
61  bool is_type = false;
62  bool is_macro = false;
63  bool is_exported = false;
64  bool is_input = false;
65  bool is_output = false;
66  bool is_state_var = false;
67  bool is_property = false;
68 
69  // ANSI-C
70  bool is_static_lifetime = false;
71  bool is_thread_local = false;
72  bool is_lvalue = false;
73  bool is_file_local = false;
74  bool is_extern = false;
75  bool is_volatile = false;
76  bool is_parameter = false;
77  bool is_auxiliary = false;
78  bool is_weak = false;
79 
81  : type(static_cast<const typet &>(get_nil_irep())),
82  value(static_cast<const exprt &>(get_nil_irep())),
84  {
85  }
86 
87  symbolt(const irep_idt &_name, typet _type, const irep_idt &_mode)
88  : type(std::move(_type)),
89  value(static_cast<const exprt &>(get_nil_irep())),
90  location(source_locationt::nil()),
91  name(_name),
92  mode(_mode)
93  {
94  }
95 
96  void swap(symbolt &b);
97  void show(std::ostream &out) const;
98 
99  class symbol_exprt symbol_expr() const;
100 
101  bool is_shared() const
102  {
103  return !is_thread_local;
104  }
105 
106  bool is_function() const
107  {
108  return !is_type && !is_macro && type.id()==ID_code;
109  }
110 
113  bool is_compiled() const
114  {
115  return type.id() == ID_code && value == exprt(ID_compiled);
116  }
117 
121  {
122  PRECONDITION(type.id() == ID_code);
123  value = exprt(ID_compiled);
124  }
125 
127  bool is_well_formed() const;
128 
129  bool operator==(const symbolt &other) const;
130  bool operator!=(const symbolt &other) const;
131 };
132 
133 std::ostream &operator<<(std::ostream &out, const symbolt &symbol);
134 
138 class type_symbolt:public symbolt
139 {
140 public:
141  type_symbolt(const irep_idt &_name, typet _type, const irep_idt &_mode)
142  : symbolt(_name, _type, _mode)
143  {
144  is_type = true;
145  }
146 };
147 
153 {
154 public:
156  {
157  is_lvalue=true;
158  is_state_var=true;
159  is_thread_local=true;
160  is_file_local=true;
161  is_auxiliary=true;
162  }
163 
165  : symbolt(name, type, mode)
166  {
167  is_lvalue = true;
168  is_state_var = true;
169  is_thread_local = true;
170  is_file_local = true;
171  is_auxiliary = true;
172  }
173 };
174 
179 {
180 public:
182  {
183  is_lvalue=true;
184  is_state_var=true;
185  is_thread_local=true;
186  is_file_local=true;
187  is_parameter=true;
188  }
189 };
190 
191 #endif // CPROVER_UTIL_SYMBOL_H
Internally generated symbol table entryThis is a symbol generated as part of translation to or modifi...
Definition: symbol.h:153
auxiliary_symbolt(const irep_idt &name, typet type, const irep_idt &mode)
Definition: symbol.h:164
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:38
bool empty() const
Definition: dstring.h:89
Base class for all expressions.
Definition: expr.h:56
exprt()
Definition: expr.h:61
const irep_idt & id() const
Definition: irep.h:384
Symbol table entry of function parameterThis is a symbol generated as part of type checking.
Definition: symbol.h:179
Expression to hold a symbol (variable)
Definition: std_expr.h:131
Symbol table entry.
Definition: symbol.h:28
irep_idt base_name
Base (non-scoped) name.
Definition: symbol.h:46
void swap(symbolt &b)
Swap values between two symbols.
Definition: symbol.cpp:85
bool is_auxiliary
Definition: symbol.h:77
bool is_volatile
Definition: symbol.h:75
symbolt()
Definition: symbol.h:80
bool is_extern
Definition: symbol.h:74
const irep_idt & display_name() const
Return language specific display name if present.
Definition: symbol.h:55
bool is_macro
Definition: symbol.h:62
bool operator==(const symbolt &other) const
Definition: symbol.cpp:202
void show(std::ostream &out) const
Dump the state of a symbol object to a given output stream.
Definition: symbol.cpp:19
bool is_file_local
Definition: symbol.h:73
bool is_well_formed() const
Check that a symbol is well formed.
Definition: symbol.cpp:128
irep_idt module
Name of module the symbol belongs to.
Definition: symbol.h:43
bool is_static_lifetime
Definition: symbol.h:70
symbolt(const irep_idt &_name, typet _type, const irep_idt &_mode)
Definition: symbol.h:87
void set_compiled()
Set the symbol's value to "compiled"; to be used once the code-typed value has been converted to a go...
Definition: symbol.h:120
bool is_property
Definition: symbol.h:67
bool is_parameter
Definition: symbol.h:76
bool is_thread_local
Definition: symbol.h:71
bool is_type
Definition: symbol.h:61
source_locationt location
Source code location of definition of symbol.
Definition: symbol.h:37
bool is_compiled() const
Returns true iff the the symbol's value has been compiled to a goto program.
Definition: symbol.h:113
bool is_state_var
Definition: symbol.h:66
class symbol_exprt symbol_expr() const
Produces a symbol_exprt for a symbol.
Definition: symbol.cpp:121
bool is_function() const
Definition: symbol.h:106
bool is_output
Definition: symbol.h:65
typet type
Type of symbol.
Definition: symbol.h:31
bool is_weak
Definition: symbol.h:78
irep_idt name
The unique identifier.
Definition: symbol.h:40
bool is_exported
Definition: symbol.h:63
irep_idt pretty_name
Language-specific display name.
Definition: symbol.h:52
bool operator!=(const symbolt &other) const
Definition: symbol.cpp:233
bool is_shared() const
Definition: symbol.h:101
bool is_lvalue
Definition: symbol.h:72
exprt value
Initial value of symbol.
Definition: symbol.h:34
irep_idt mode
Language mode.
Definition: symbol.h:49
bool is_input
Definition: symbol.h:64
Symbol table entry describing a data typeThis is a symbol generated as part of type checking.
Definition: symbol.h:139
type_symbolt(const irep_idt &_name, typet _type, const irep_idt &_mode)
Definition: symbol.h:141
The type of an expression, extends irept.
Definition: type.h:29
const irept & get_nil_irep()
Definition: irep.cpp:19
#define PRECONDITION(CONDITION)
Definition: invariant.h:463
std::ostream & operator<<(std::ostream &out, const symbolt &symbol)
Overload of stream operator to work with symbols.
Definition: symbol.cpp:76