cprover
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
63 
64  // ANSI-C
68 
70  {
71  clear();
72  }
73 
75  void clear()
76  {
77  type.make_nil();
78  value.make_nil();
80 
82 
88  }
89 
90  void swap(symbolt &b);
91  void show(std::ostream &out) const;
92 
93  class symbol_exprt symbol_expr() const;
94 
95  bool is_shared() const
96  {
97  return !is_thread_local;
98  }
99 
100  bool is_function() const
101  {
102  return !is_type && !is_macro && type.id()==ID_code;
103  }
104 
107  bool is_compiled() const
108  {
109  return type.id() == ID_code && value == exprt(ID_compiled);
110  }
111 
115  {
116  PRECONDITION(type.id() == ID_code);
117  value = exprt(ID_compiled);
118  }
119 
121  bool is_well_formed() const;
122 
123  bool operator==(const symbolt &other) const;
124  bool operator!=(const symbolt &other) const;
125 };
126 
127 std::ostream &operator<<(std::ostream &out, const symbolt &symbol);
128 
132 class type_symbolt:public symbolt
133 {
134 public:
135  explicit type_symbolt(const typet &_type)
136  {
137  type=_type;
138  is_type=true;
139  }
140 };
141 
147 {
148 public:
150  {
151  is_lvalue=true;
152  is_state_var=true;
153  is_thread_local=true;
154  is_file_local=true;
155  is_auxiliary=true;
156  }
157 
160  {
161  this->name=name;
162  this->base_name=name;
163  this->type=type;
164  }
165 };
166 
171 {
172 public:
174  {
175  is_lvalue=true;
176  is_state_var=true;
177  is_thread_local=true;
178  is_file_local=true;
179  is_parameter=true;
180  }
181 };
182 
183 #endif // CPROVER_UTIL_SYMBOL_H
Internally generated symbol table entryThis is a symbol generated as part of translation to or modifi...
Definition: symbol.h:147
auxiliary_symbolt(const irep_idt &name, const typet &type)
Definition: symbol.h:158
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:37
bool empty() const
Definition: dstring.h:88
Base class for all expressions.
Definition: expr.h:54
exprt()
Definition: expr.h:59
const irep_idt & id() const
Definition: irep.h:407
void make_nil()
Definition: irep.h:465
Symbol table entry of function parameterThis is a symbol generated as part of type checking.
Definition: symbol.h:171
Expression to hold a symbol (variable)
Definition: std_expr.h:80
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
void clear()
Zero initialise a symbol object.
Definition: symbol.h:75
bool is_auxiliary
Definition: symbol.h:67
bool is_volatile
Definition: symbol.h:66
symbolt()
Definition: symbol.h:69
bool is_extern
Definition: symbol.h:66
const irep_idt & display_name() const
Return language specific display name if present.
Definition: symbol.h:55
bool is_macro
Definition: symbol.h:61
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:66
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:65
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:114
bool is_property
Definition: symbol.h:62
bool is_parameter
Definition: symbol.h:67
bool is_thread_local
Definition: symbol.h:65
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:107
bool is_state_var
Definition: symbol.h:62
class symbol_exprt symbol_expr() const
Produces a symbol_exprt for a symbol.
Definition: symbol.cpp:121
bool is_function() const
Definition: symbol.h:100
bool is_output
Definition: symbol.h:62
typet type
Type of symbol.
Definition: symbol.h:31
bool is_weak
Definition: symbol.h:67
irep_idt name
The unique identifier.
Definition: symbol.h:40
bool is_exported
Definition: symbol.h:61
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:95
bool is_lvalue
Definition: symbol.h:66
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:62
Symbol table entry describing a data typeThis is a symbol generated as part of type checking.
Definition: symbol.h:133
type_symbolt(const typet &_type)
Definition: symbol.h:135
The type of an expression, extends irept.
Definition: type.h:28
dstringt irep_idt
Definition: irep.h:37
#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